Library UniMath.Foundations.UnivalenceAxiom2

proofs that the statements of the axioms are propositions

Require Import UniMath.Foundations.PartD.

Lemma isaprop_univalenceStatement : isaprop univalenceStatement.
Show proof.

  unfold univalenceStatement.
  apply impred_isaprop; intro X;
  apply impred_isaprop; intro Y.
  apply isapropisweq.

Lemma isaprop_funextemptyStatement : isaprop funextemptyStatement.
Show 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.

Lemma isaprop_isweqtoforallpathsStatement : isaprop isweqtoforallpathsStatement.
Show 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.

Lemma isaprop_propositionalUnivalenceStatement : isaprop propositionalUnivalenceStatement.
Show 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.

Lemma isaprop_funcontrStatement : isaprop funcontrStatement.
Show proof.

  unfold funcontrStatement.
  apply impred_isaprop; intro X;
  apply impred_isaprop; intro P;
  apply impred_isaprop; intros _.
  apply isapropiscontr.

Lemma isaprop_funextcontrStatement : isaprop funextcontrStatement.
Show proof.

  unfold funextcontrStatement.
  apply impred_isaprop; intro T;
  apply impred_isaprop; intro P;
  apply impred_isaprop; intro g.
  apply isapropiscontr.