Using proof irrelevance

theories/HoTT_additions.v

@@ -16,7 +16,6 @@ From Coq Require Import ssreflect ssrfun ssrbool.
 Set Universe Polymorphism.
 Unset Universe Minimization ToSet.
 
-
 (* Definition equiv_forall_sigma {A : Type} {P : A -> Type} {Q : forall a, P a -> Type} : *)
 (*   (forall a (b : P a), Q a b) <~> forall x : { a : A | P a }, Q x.1 x.2. *)
 (* Proof. *)
@@ -223,6 +222,10 @@ Lemma moveR_pM {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) :
   r = q @ p^ -> r @ p = q.
 Proof. by case: _ / p q r. Defined.
 
+Lemma transport1@{i j} {A : Type@{i}} (P : A -> Type@{j})
+    {x : A} (u : P x) : transport P 1 u = u.
+Proof. done. Defined.
+
 Lemma transport_pp@{i j} {A : Type@{i}} (P : A -> Type@{j})
     {x y z : A} (p : x = y) (q : y = z) (u : P x) :
   transport P (p @ q) u = transport P q (transport P p u).
@@ -255,3 +258,9 @@ Reserved Notation "m +2+ n" (at level 50, left associativity).
 Reserved Infix "mod" (at level 40, no associativity).
 Reserved Notation "p ~ 1" (at level 7, left associativity, format "p '~' '1'").
 Reserved Notation "p ~ 0" (at level 7, left associativity, format "p '~' '0'").
+
+Definition Prop_irrelevance_type := forall (P : Prop) (p q : P), p = q.
+Definition Prop_ext_type := forall (P Q : Prop), (P <-> Q) -> P = Q.
+
+Axiom Prop_irrelevance : Prop_irrelevance_type.
+Axiom Prop_ext : Prop_ext_type.