I've seen elaboration-zoo, pi-forall, Mini-TT, etc., all kinds of demonstrations of dependent type elaboration. However, none of them support Prop.

I am interested in the following specific type checking problem about Prop. I have read somewhere in TaPL saying that for Prop, one cannot simply eliminate it to Type. I understand semantically why, but I am having trouble finding an elegant way to algorithmize it. I (together with some friends) came up with the following naive attempts, all seem stupid and ugly:

  • Add a boolean parameter to inherit/synthesize, the two directions of type checking, representing whether we are allowed to eliminate from Prop here in the term. We also add it to the patterns' type checker.
  • Everywhere I see an elimination from a proposition, I check the context type and make sure it's also a proposition. We do the same for patterns.

I think both seem very inefficient. Is there some code examples I can look at? I conjecture that there must be some clever ways...

  • $\begingroup$ What kind of language are you looking at? I guess Agda-style clausal definitions? If you work with eliminators/pattern-matching, it's easy: decide in advance which inductive types are allowed to be eliminated in which universes (ie what is usually called subsingleton elimination), and when you encounter an eliminator/match, infer the universe of the return predicate, and check that it is allowed for the type you are eliminating/matching on. $\endgroup$ Nov 17, 2022 at 9:22
  • $\begingroup$ @MevenLennon-Bertrand yes Agda style $\endgroup$
    – ice1000
    Nov 17, 2022 at 13:01


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.