4
$\begingroup$

What are some examples of existence proofs in Coq/Agda etc., where the constructed natural number is useful from mathematical point of view, but it's non-obvious from the proof what it should be? I am aware of the Brunerie number in homotopical versions of type theory, but as far as I know, this doesn't really compute or takes far too long in current implementations of Cubical Type Theory. Are there any interesting applications in Agda/Coq etc. with K, which compute and weren't done by hand on paper? Are there any interesting numbers in Cubical Agda, which were computed?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.