Library UniMath.Foundations.UnivalenceAxiom2

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.