Library UniMath.Foundations.UnivalenceAxiom2
proofs that the statements of the axioms are propositions
Require Import UniMath.Foundations.PartD.
Lemma isaprop_univalenceStatement : isaprop univalenceStatement.
Proof.
unfold univalenceStatement.
apply impred_isaprop; intro X;
apply impred_isaprop; intro Y.
apply isapropisweq.
Defined.
Lemma isaprop_funextemptyStatement : isaprop funextemptyStatement.
Proof.
unfold funextemptyStatement.
apply impred_isaprop; intro X;
apply impred_isaprop; intro f;
apply impred_isaprop; intro g.
generalize g; clear g.
generalize f; clear f.
change (isaset (X → ∅)).
apply impred_isaset; intro x.
apply isasetempty.
Defined.
Lemma isaprop_isweqtoforallpathsStatement : isaprop isweqtoforallpathsStatement.
Proof.
unfold isweqtoforallpathsStatement.
apply impred_isaprop; intro T;
apply impred_isaprop; intro P;
apply impred_isaprop; intro f;
apply impred_isaprop; intro g.
apply isapropisweq.
Defined.
Lemma isaprop_propositionalUnivalenceStatement : isaprop propositionalUnivalenceStatement.
Proof.
unfold propositionalUnivalenceStatement.
apply impred_isaprop; intro P;
apply impred_isaprop; intro Q;
apply impred_isaprop; intro i;
apply impred_isaprop; intro j;
apply impred_isaprop; intros _;
apply impred_isaprop; intros _.
apply (isofhlevelweqb 1 (univalence P Q)).
fold isaprop.
apply isapropweqtoprop.
exact j.
Defined.
Lemma isaprop_funcontrStatement : isaprop funcontrStatement.
Proof.
unfold funcontrStatement.
apply impred_isaprop; intro X;
apply impred_isaprop; intro P;
apply impred_isaprop; intros _.
apply isapropiscontr.
Defined.
Lemma isaprop_funextcontrStatement : isaprop funextcontrStatement.
Proof.
unfold funextcontrStatement.
apply impred_isaprop; intro T;
apply impred_isaprop; intro P;
apply impred_isaprop; intro g.
apply isapropiscontr.
Defined.