Strict Propositions

[spitters]

They will be available in Coq and agda, and if I understand things well they are consistent with CTT.
Should we want them in redtt?
rocq-prover/rfcs#37

[jonsterling]

I think something along those lines is a reasonable idea; in RedPRL for instance, we considered many different universes with slightly different properties; one of the most useful ones was the "discrete types", which are roughly the types which are both Kan and satisfy equality reflection. There are a lot more types of that kind than you might at first expect!

I'd like to incorporate that, and also strict propositions at some point in the future.