Require Import overture pext inhab.

Section Interval.
  Definition interval := inhab bool.
  Let i0 : interval := tr false.
  Let i1 : interval := tr true.

  Lemma I_path {A : Type} (f : interval -> A) : f i0 = f i1.
  Proof. congr f. exact: trP. Qed.

  Program Definition path_I {A : Type} {x y : A} (p : x = y) : interval -> A :=
    inhab_rec (fun b => if b then y else x) _.
  Next Obligation. by destruct x0, y0. Qed.

  Definition fext {A : Type} {B : A -> Type} (f g : forall x, B x) :
    (forall x, f x = g x) -> f = g := fun p => I_path (fun i x => path_I (p x) i).
End Interval.

Lemma xi_ext {A} {B C : A -> Type} (p : forall x : A, B x = C x) :
  (forall x, B x) = (forall x, C x).
Proof. have: B = C by exact: fext. by move->. Qed.

Lemma xi_extP {A} {B C : A -> Prop} (p : forall x : A, B x = C x) :
  (forall x, B x) = (forall x, C x).
Proof. have: B = C by exact: fext. by move->. Qed.

Lemma xi_extS {A} {B C : A -> Set} (p : forall x : A, B x = C x) :
  (forall x, B x) = (forall x, C x).
Proof. have: B = C by exact: fext. by move->. Qed.

Ltac fext := nointr repeat (
  match goal with
    [ |- ?x = ?y ] =>
     (apply: fext ||
     apply: xi_extP ||
     apply: xi_extS ||
     apply: xi_ext); intro
  end).

Lemma prod_is_prop A (P : A -> hprop) : is_prop (forall x, P x).
Proof. move=> p q. apply: fext => x. exact: hpropP. Qed.

Canonical Structure prod_hprop A (P : A -> hprop) :=
  mk_hprop (iprod P) (@prod_is_prop A P).

Canonical Structure fun_hprop A (B : hprop) :=
  mk_hprop (A -> B) (@prod_is_prop A (fun _ => B)).

Definition pairb {T} (x y : T) (b : bool) : T := if b then x else y.

Lemma pairb_fun {X Y} (f : X -> Y) x y :
  f \o pairb x y = pairb (f x) (f y).
Proof. by fext=> -[]. Qed.

Section EquivalencePaths.
  Variables (A B : Type).
  Implicit Types (f : A -> B).

  Lemma is_equiv_prop f :
    is_prop (is_equiv f).
  Proof.
    move=> [g1 h1 h2] [g2 h3 h4]. have e: g1 = g2. apply: fext => x.
      by rewrite -{1}[x]h4 h1. destruct e. f_equal; exact: pi.
  Qed.

  Canonical Structure is_equiv_hprop f := mk_hprop (is_equiv f) (@is_equiv_prop f).

  Lemma equiv_eq (f g : A <~> B) :
    f = g :> (A -> B) -> f = g.
  Proof.
    move: f g => [f hf] [g hg] /= eqn. destruct eqn. f_equal. exact: hpropP.
  Qed.
End EquivalencePaths.

Section TruncationMappingProperty.
  Variables (A B : Type).

  Definition constant (f : A -> B) := forall x y, f x = f y.

  Program Definition inhab_map (f : inhab A -> B) : { f : A -> B | constant f } :=
    exist _ (f \o tr) _.
  Next Obligation. move=> x y /=. congr f. exact: trP. Qed.

  Definition map_inhab (p : { f : A -> B | constant f }) : inhab A -> B :=
    inhab_rec p.1 p.2.

  Lemma inhab_map_sect (f : inhab A -> B) : map_inhab (inhab_map f) = f.
  Proof. fext. exact: inhab_ind. Qed.

  Lemma inhab_map_retr (p : { f : A -> B | constant f }) :
    inhab_map (map_inhab p) = p.
  Proof. exact: sig_eq. Qed.

  Definition inhab_map_is_equiv : is_equiv inhab_map :=
    mk_is_equiv map_inhab inhab_map_sect inhab_map_retr.

  Canonical inhab_map_equiv := mk_equiv inhab_map inhab_map_is_equiv.
End TruncationMappingProperty.