semantics.base.pext
Propositional Extensionality
Require Import overture.
Require Import Coq.Logic.PropExtensionality.
Lemma pext {P Q : Prop} :
(P -> Q) -> (Q -> P) -> P = Q.
Proof.
move=> pq qp. exact: propositional_extensionality.
Qed.
Lemma pi {P : Prop} (p q : P) : p = q.
Proof.
have e: P = True by exact: pext. move: p q. by rewrite e => -[] [].
Qed.
Canonical Structure hprop_prop (P : Prop) := mk_hprop P pi.
Definition K {A : Type} {a : A} (P : a = a -> Type) (h : P erefl)
(p : a = a) : P p := match pi erefl p with erefl => h end.
(*Lemma K_refl {A} {a : A} (P : a = a -> Type) (h : P erefl) :
K h erefl = h.
Proof.
rewrite/K. move: (pi _ _). exact: K.
Qed.*)
Lemma sigT_injective (A : Type) (P : A -> Type) (a : A) (p q : P a) :
(a; p) = (a; q) -> p = q.
Proof.
move=> e. move/sigT_eq_pr2: (e) => /=. move: e..1 => /=. exact: K.
Qed.
Lemma sig_eq (A : Type) (P : A -> Prop) (p q : sig P) :
p.1 = q.1 -> p = q.
Proof. destruct p,q => /= E. destruct E. f_equal. exact: pi. Qed.
Lemma sig_is_hprop (A : hprop) (P : A -> Prop) : is_prop (sig P).
Proof. move=> a b. apply: sig_eq. exact: hpropP. Qed.
Canonical Structure sig_hprop (A : hprop) (P : A -> Prop) :=
mk_hprop (sig P) (@sig_is_hprop A P).
Require Import Coq.Logic.PropExtensionality.
Lemma pext {P Q : Prop} :
(P -> Q) -> (Q -> P) -> P = Q.
Proof.
move=> pq qp. exact: propositional_extensionality.
Qed.
Lemma pi {P : Prop} (p q : P) : p = q.
Proof.
have e: P = True by exact: pext. move: p q. by rewrite e => -[] [].
Qed.
Canonical Structure hprop_prop (P : Prop) := mk_hprop P pi.
Definition K {A : Type} {a : A} (P : a = a -> Type) (h : P erefl)
(p : a = a) : P p := match pi erefl p with erefl => h end.
(*Lemma K_refl {A} {a : A} (P : a = a -> Type) (h : P erefl) :
K h erefl = h.
Proof.
rewrite/K. move: (pi _ _). exact: K.
Qed.*)
Lemma sigT_injective (A : Type) (P : A -> Type) (a : A) (p q : P a) :
(a; p) = (a; q) -> p = q.
Proof.
move=> e. move/sigT_eq_pr2: (e) => /=. move: e..1 => /=. exact: K.
Qed.
Lemma sig_eq (A : Type) (P : A -> Prop) (p q : sig P) :
p.1 = q.1 -> p = q.
Proof. destruct p,q => /= E. destruct E. f_equal. exact: pi. Qed.
Lemma sig_is_hprop (A : hprop) (P : A -> Prop) : is_prop (sig P).
Proof. move=> a b. apply: sig_eq. exact: hpropP. Qed.
Canonical Structure sig_hprop (A : hprop) (P : A -> Prop) :=
mk_hprop (sig P) (@sig_is_hprop A P).