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).