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?



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.