theory Propositions imports MLTT.Prelude Equivalence begin Definition isProp: ":= \<Prod>x y: A. x = y" where "A: U i" by typechk Definition isSet: ":=\<Prod>x y: A. \<Prod>p q: x = y. p = q" where "A: U i" by typechk Theorem isProp_Top: "isProp \<top>" unfolding isProp_def by (intros, elims, refl) Theorem isProp_Bot: "isProp \<bottom>" unfolding isProp_def by (intros, elim) end