proposition: Lemma propositionalUnivalenceUAH: propositionalUnivalenceStatement.
proof: Proof. unfold propositionalUnivalenceStatement; intros ? ? i j f g. apply weqtopathsUAH. simple refine (make_weq f (isweq_iso f g _ _)). - intro p. apply proofirrelevance, i. - intro q. apply proofirrelevance, j. Defined.
imports: UniMath.Foundations.PartB