booleans_by_univalence.v

(*
  Everything here is really ugly as I didn't clean it,
    some bits come from the Coq-HoTT library.

  The main idea is that given funext and any
    h-set with multiple provably distinct elements.

  Univalence is only used to prove s_true_neq_s_false

  Then by funext you can get the induction principle to contract.

  Then you pair the h-set and the induction principle is contractible.
  
  Then to prove anything about the pair you can prove only about the fst.

  Structure:

  S_Bool, a set truncated boolean
  I_Bool, the induction principle for S_Bool
  T_Bool, a witness for I_Bool
  J_Bool, a contractible pair with the induction principle
  Bool, S_Bool and J_Bool
*)

Definition sig_fst {A B} {p q : {x : A | B x}} (H : p = q)
  : proj1_sig p = proj1_sig q :=
  eq_rect _ (fun z => proj1_sig p = proj1_sig z) eq_refl _ H.

Definition sig_snd {A B} {p q : {x : A | B x}} (H : p = q)
  : eq_rect _ B (proj2_sig p) _ (sig_fst H) = proj2_sig q :=
  match H with
  | eq_refl => eq_refl
  end.
Lemma sig_ext {A B} (p q : {x : A | B x})
  (H1 : proj1_sig p = proj1_sig q)
  (H2 : eq_rect _ B (proj2_sig p) _ H1 = proj2_sig q)
  : p = q.
  destruct p, q; simpl in *.
  destruct H1, H2; simpl in *.
  reflexivity.
Defined.
Lemma sig_eq_is_sig_ext {A B} {l r : {x : A | B x}}
  (p : l = r) : p = sig_ext l r (sig_fst p) (sig_snd p).
  destruct p, l; reflexivity.
Defined.
Lemma sig_eq_ext_refl {A B} {l : {x : A | B x}}
  (p : l = l) (H1 : sig_fst p = eq_refl)
  (H2 :
    match H1 in (_ = f_p) return
      eq_rect _ B (proj2_sig l) _ f_p = proj2_sig l
    with
    | eq_refl => sig_snd p
    end = eq_refl)
  : p = eq_refl.
  rewrite (sig_eq_is_sig_ext p).
  rewrite (sig_eq_is_sig_ext eq_refl).
  (* TODO: this is ugly *)
  eassert (_ = sig_snd eq_refl).
  exact H2.
  destruct H; clear H2.
  simpl.
  destruct H1.
  reflexivity.
Defined.
Lemma sig_eq_ext {A B} {l r : {x : A | B x}}
  (p q : l = r) (H1 : sig_fst p = sig_fst q)
  (H2 :
    match H1 in (_ = f_p) return
      eq_rect _ B (proj2_sig l) _ f_p = proj2_sig r
    with
    | eq_refl => sig_snd p
    end = sig_snd q) : p = q.
  destruct q.
  exact (sig_eq_ext_refl p H1 H2).
Defined.

(* univalence bits *)
Definition Sect {A B : Prop} (s : A -> B) (r : B -> A) : Prop :=
  forall x : A, r (s x) = x.
Definition ap {A B : Prop} (f : A -> B)
  {x y : A} (p : x = y) : f x = f y
  := match p with | eq_refl => eq_refl end.
Record IsEquiv {A B : Prop} (f : A -> B) : Prop := equiv_intro {
  equiv_inv : B -> A;
  eisretr : Sect equiv_inv f;
  eissect : Sect f equiv_inv;
  eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
}.
Record Equiv A B : Prop := {
  equiv_fun : A -> B;
  equiv_isequiv : IsEquiv equiv_fun;
}.
Lemma id_equiv {A : Prop} : Equiv A A.
  exists (fun x => x).
  exists (fun x => x) (fun x => eq_refl) (fun x => eq_refl).
  intros x; reflexivity.
Defined.
Definition equiv_path {A B : Prop} (p : A = B) : Equiv A B := 
  match p with
  | eq_refl => id_equiv
  end.

Axiom Univalence : forall (A B : Prop), IsEquiv (@equiv_path A B).

(* funext *)
Axiom functional_extensionality_dep_inner : forall {A} {B : A -> Type},
  forall (f g : forall x : A, B x),
  (forall x, f x = g x) -> f = g.
Definition functional_extensionality_dep
  {A} {B : A -> Type}
  (f g : forall x : A, B x)
  (H : forall x, f x = g x) : f = g
:= eq_trans (eq_sym (functional_extensionality_dep_inner f f (fun _ => eq_refl)))
     (functional_extensionality_dep_inner f g H).

Lemma functional_extensionality_dep_refl {A B} f
: @functional_extensionality_dep A B f f (fun _ => eq_refl) = eq_refl.
  unfold functional_extensionality_dep.
  destruct functional_extensionality_dep_inner; reflexivity.
Defined.

Lemma fun_elim {A B} {l r : forall (x : A), B x}
  (p : l = r) : forall x, l x = r x.
  intros x; destruct p; reflexivity.
Defined.
Lemma fun_eq_is_fun_ext {A B} {l r : forall (x : A), B x}
  (p : l = r) : functional_extensionality_dep l r (fun_elim p) = p.
  refine (
    match p in (_ = f) return
      functional_extensionality_dep l _ (fun_elim p) = p
    with
    | eq_refl => _
    end
  ).
  apply functional_extensionality_dep_refl.
Defined.
Lemma fun_eq_ext {A B} {l r : forall (x : A), B x}
  (p q : l = r) (h : forall x, fun_elim p x = fun_elim q x) : p = q.
  destruct (fun_eq_is_fun_ext p).
  destruct (fun_eq_is_fun_ext q).
  assert (fun_elim p = fun_elim q).
  apply functional_extensionality_dep; intros x.
  exact (h x).
  rewrite H; reflexivity.
Defined.

Lemma pair_ext {P R : Prop}
  (l r : (P * R) : Prop) (H1 : fst l = fst r)
  (H2 : snd l = snd r) : l = r.
  destruct l, r.
  simpl in *.
  destruct H1, H2; reflexivity.
Defined.

(* h-level *)
Definition IsContr (A : Type) :=
  {x | forall y : A, x = y}.
Definition IsProp (A : Type) :=
  forall x y : A, x = y.
Definition IsSet (A : Type) :=
  forall x y : A, IsProp (x = y).

Lemma IsContr_IsProp {A : Prop} (A_is_contr : IsContr A) : IsProp A.
  intros x y; destruct A_is_contr as [center H].
  destruct (H x), (H y); reflexivity.
Defined.

(* h-props *)
Lemma h_prop_eq_contr {A : Prop} (A_is_prop : IsProp A)
  (x : A) : IsContr (x = x).
  exists (
    match A_is_prop x x in (_ = z) return (z = x) with
    | eq_refl => A_is_prop x x
    end
  ).
  intros H.
  destruct H.
  destruct (A_is_prop x x).
  reflexivity.
Defined.

Lemma h_prop_eq_prop {A : Prop} (A_is_prop : IsProp A)
  (x y : A) : IsProp (x = y).
  intros p q; destruct p.
  destruct (h_prop_eq_contr A_is_prop x) as [center H].
  destruct (H eq_refl); exact (H q).
Defined.
Lemma h_prop_eq_eq_prop {A : Prop} (A_is_prop : IsProp A)
  (x y : A) (p q : x = y) : IsProp (p = q).
  intros l r; destruct p, l.
  apply (
    h_prop_eq_prop
      (h_prop_eq_prop A_is_prop x x)
      eq_refl eq_refl).
Defined.  

Lemma equiv_h_prop_t_eq_contr {A : Prop}
  (A_is_prop : IsProp A) : IsContr (Equiv A A).
  exists id_equiv; intros r.

  assert (forall (f : A -> A), (fun x => x) = f).
  intros f; apply functional_extensionality_dep.
  intros x; apply A_is_prop.

  unfold id_equiv.
  destruct r as [r_in [r_inv r_is_retr r_is_sect r_is_adj]].
  destruct (H r_in), (H r_inv); clear H.
  
  assert (forall (p : forall (x : A), x = x), (fun _ => eq_refl) = p).
  intros p; apply functional_extensionality_dep; intros x.
  apply (h_prop_eq_prop A_is_prop x x).

  destruct (H r_is_retr), (H r_is_sect); clear H.

  assert ((fun x => eq_refl) = r_is_adj).
  apply functional_extensionality_dep; intros x.
  apply (h_prop_eq_eq_prop A_is_prop x x eq_refl eq_refl).
  
  destruct H; reflexivity.
Defined.

Lemma h_prop_t_eq_contr {A : Prop} (A_is_prop : IsProp A) : IsContr (A = A).
  assert ((A = A) = Equiv A A).
  (* only usage of univalence *)
  apply (equiv_inv _ (Univalence (A = A) (Equiv A A))).
  exists equiv_path; apply Univalence.
  rewrite H; apply equiv_h_prop_t_eq_contr; exact A_is_prop.
Defined.

Definition False : Prop := forall A, A.
Lemma False_IsProp : IsProp False.
  intros x y; apply x.
Defined.
Lemma False_eq_IsContr : IsContr (False = False).
  exact (h_prop_t_eq_contr False_IsProp).
Defined.

Definition Unit : Prop :=
  {x : (forall A : Prop, A -> A) | (fun A x => x) = x}.
Definition unit : Unit := exist _ (fun A x => x) eq_refl.
Lemma Unit_IsProp : IsProp Unit.
  intros x y; destruct x as [x_l x_h]; destruct y as [y_l y_h].
  destruct x_h, y_h; reflexivity.
Defined.
Lemma Unit_eq_IsContr : IsContr (Unit = Unit).
  exact (h_prop_t_eq_contr Unit_IsProp).
Defined.

Lemma Unit_neq_False (H : Unit = False) : False.
  destruct H; exact unit.
Defined.

Definition S_Bool : Type :=
  forall (A : Type) (t : A) (f : A),
    IsContr (t = t) -> IsContr (f = f) -> A.
Definition s_true : S_Bool := fun A t f s_t s_f => t.
Definition s_false : S_Bool := fun A t f s_t s_f => f.
Lemma s_true_eq_prop : IsProp (s_true = s_true).
  intros p q.
  apply (fun_eq_ext _ _); intros A.
  apply (fun_eq_ext _ _); intros t.
  apply (fun_eq_ext _ _); intros f.
  apply (fun_eq_ext _ _); intros s_t.
  apply (fun_eq_ext _ _); intros s_f.
  apply (IsContr_IsProp s_t).
Defined.
Lemma s_false_eq_prop : IsProp (s_false = s_false).
  intros p q.
  apply (fun_eq_ext _ _); intros A.
  apply (fun_eq_ext _ _); intros t.
  apply (fun_eq_ext _ _); intros f.
  apply (fun_eq_ext _ _); intros s_t.
  apply (fun_eq_ext _ _); intros s_f.
  apply (IsContr_IsProp s_f).
Defined.
Lemma s_true_neq_s_false (H : s_true = s_false) : False.
  exact (
    match H in (_ = s_b) return
      s_b Prop Unit False Unit_eq_IsContr False_eq_IsContr
    with
    | eq_refl => unit
    end
  ).
Defined.

Definition I_Bool (s_b : S_Bool) : Prop :=
  forall (P : S_Bool -> Prop) (t : P s_true) (f : P s_false), P s_b.
Definition i_true : I_Bool s_true := fun P t f => t.
Definition i_false : I_Bool s_false := fun P t f => f.

Definition T_Bool {s_b} (i_b : I_Bool s_b) : Prop :=
  ((forall H : (s_true = s_b),
    match H in (_ = r) return (I_Bool r) with
    | eq_refl => i_true
    end = i_b) * 
  (forall H : (s_false = s_b),
    match H in (_ = r) return (I_Bool r) with
    | eq_refl => i_false
    end = i_b)).
Definition t_true : T_Bool i_true.
  split.
  intros H; destruct (s_true_eq_prop eq_refl H); reflexivity.
  intros H; apply (s_true_neq_s_false (eq_sym H)).
Defined.
Definition t_false : T_Bool i_false.
  split.
  intros H; apply (s_true_neq_s_false H).
  intros H; destruct (s_false_eq_prop eq_refl H); reflexivity.
Defined.

Definition J_Bool (s_b : S_Bool) : Prop :=
  {i_b : I_Bool s_b | T_Bool i_b}.
Definition j_true : J_Bool s_true := exist _ i_true t_true.
Definition j_false : J_Bool s_false := exist _ i_false t_false.

Lemma j_true_contr : IsContr (J_Bool s_true).
  exists j_true; intros j_b.
  unfold j_true; destruct j_b as [i_b [h_t h_f]].
  apply (sig_ext j_true (exist _ i_b (h_t, h_f)) (h_t eq_refl)).
  apply pair_ext; simpl.
  -
    apply functional_extensionality_dep; intros H.
    destruct (s_true_eq_prop eq_refl H).
    destruct (h_t eq_refl); simpl.
    assert (eq_refl = s_true_eq_prop eq_refl eq_refl).
    apply (h_prop_eq_prop s_true_eq_prop eq_refl eq_refl).
    destruct H; reflexivity.
  -
    apply functional_extensionality_dep; intros H.
    apply (s_true_neq_s_false (eq_sym H)).
Defined.
Lemma j_true_prop : IsProp (J_Bool s_true).
  exact (IsContr_IsProp (j_true_contr)).
Defined.

Lemma j_false_contr : IsContr (J_Bool s_false).
  exists j_false; intros j_b.
  unfold j_false; destruct j_b as [i_b [h_t h_f]].
  apply (sig_ext j_false (exist _ i_b (h_t, h_f)) (h_f eq_refl)).
  apply pair_ext; simpl.
  -
    apply functional_extensionality_dep; intros H.
    apply (s_true_neq_s_false H).
  -
    apply functional_extensionality_dep; intros H.
    destruct (s_false_eq_prop eq_refl H).
    destruct (h_f eq_refl); simpl.
    assert (eq_refl = s_false_eq_prop eq_refl eq_refl).
    apply (h_prop_eq_prop s_false_eq_prop eq_refl eq_refl).
    destruct H; reflexivity.
Defined.
Lemma j_false_prop : IsProp (J_Bool s_false).
  exact (IsContr_IsProp (j_false_contr)).
Defined.

Definition Bool : Prop := exists (s_b : S_Bool), J_Bool s_b.
Definition true : Bool := ex_intro _ s_true j_true.
Definition false : Bool := ex_intro _ s_false j_false.

Lemma ind (b : Bool) : forall P : Bool -> Prop, P true -> P false -> P b.
  destruct b as [b_p j_b].
  refine (proj1_sig j_b
    (fun b_p => forall j_b,
      forall P, _ -> _ -> P (ex_intro _ b_p j_b))
    _ _ j_b); clear.
  intros j_b P t f; destruct (j_true_prop j_true j_b); exact t.
  intros j_b P t f; destruct (j_false_prop j_false j_b); exact f.
Defined.

Lemma ind_t : ind true = (fun P t f => t).
  simpl; unfold i_true.
  assert (eq_refl = j_true_prop j_true j_true).
  apply (h_prop_eq_prop j_true_prop).
  destruct H; reflexivity.
Defined.
Lemma ind_f : ind false = (fun P t f => f).
  simpl; unfold i_false.
  assert (eq_refl = j_false_prop j_false j_false).
  apply (h_prop_eq_prop j_false_prop).
  destruct H; reflexivity.
Defined.

Lemma bool_h_set : IsSet Bool.
  intros x y p q; destruct p.
  revert q; apply (ind x); intros q.
  epose (
    match q as p in (_ = b) return
      ind b
        (fun b => true = b -> true = b)
        (fun h => eq_refl) (fun h => h) p = p
    with
    | eq_refl => _
    end
  ).
  rewrite ind_t in e; exact e.
  epose (
    match q as p in (_ = b) return
      ind b
        (fun b => false = b -> false = b)
        (fun h => h) (fun h => eq_refl) p = p
    with
    | eq_refl => _
    end
  ).
  rewrite ind_f in e; exact e.
  Unshelve.
  rewrite ind_t; reflexivity.
  rewrite ind_f; reflexivity.
Defined.