From 512664cc10d6616ddcd840eedbf1d15ef9259fc0 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 10 Jul 2024 08:46:47 +0200 Subject: [PATCH] Using proof irrelevance --- theories/HoTT_additions.v | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/theories/HoTT_additions.v b/theories/HoTT_additions.v index 02df3b0..1cd7801 100644 --- a/theories/HoTT_additions.v +++ b/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. \ No newline at end of file