bool_by_j_pure_pred.v

Inductive t_eq {A} (x : A) : A -> Type :=
  | t_refl : t_eq x x.
Definition coe {A} {x y : A} (C : A -> Type) (p : t_eq x y) (H : C x) : C y :=
  match p in (t_eq _ z) return C z with | t_refl _ => H end.
Definition sym {A} {x y : A} (p : t_eq x y) : t_eq y x :=
  coe (fun z => t_eq z x) p (t_refl x).
Definition ap {A B x y} (f : A -> B) (H : t_eq x y) : t_eq (f x) (f y) :=
  coe (fun z => t_eq (f x) (f z)) H (t_refl (f x)).
Definition coe_inj {A} {x y : A} (C : A -> Type)
  (p : t_eq x y) {H1 H2} (H : t_eq (coe C p H1) (coe C p H2)) : t_eq H1 H2.
  destruct p; exact H.
Defined.

Lemma sig_ext {A B} (p q : {x : A & B x})
  (H1 : t_eq (projT1 p) (projT1 q))
  (H2 : t_eq (coe B H1 (projT2 p)) (projT2 q)) : t_eq p q.
  destruct p, q; cbn in *.
  destruct H1, H2; cbn in *.
  reflexivity.
Defined.

Definition C_False : Type := forall A, A.
Definition C_Unit : Type := forall A, A -> A.
Definition c_unit : C_Unit := fun A x => x.

Definition C_Either (A B : Type) : Type :=
  forall (C : Type), (A -> C) -> (B -> C) -> C.
Definition c_inl {A B} (a : A) : C_Either A B :=
  fun C f g => f a.
Definition c_inr {A B} (b : B) : C_Either A B :=
  fun C f g => g b.

Definition I_Either A B (c_e : C_Either A B) : Type :=
  forall (P : C_Either A B -> Type),
    (forall a, P (c_inl a)) ->
    (forall b, P (c_inr b)) ->
    P c_e.
Definition i_inl A B (a : A) : I_Either A B (c_inl a) :=
  fun P f g => f a.
Definition i_inr A B (b : B) : I_Either A B (c_inr b) :=
  fun P f g => g b.

Definition W_Either A B : Type :=
  {c_e : C_Either A B & I_Either A B c_e}.
Definition w_inl A B (a : A) : W_Either A B :=
  existT _ (c_inl a) (i_inl A B a).
Definition w_inr A B (b : B) : W_Either A B :=
  existT _ (c_inr b) (i_inr A B b).

Definition Dec_f A (f : A -> A) : Type :=
  forall x y, W_Either (t_eq (f x) (f y)) (t_eq (f x) (f y) -> C_False).
Definition f_dec_eq {A f} (f_dec : Dec_f A f)
  x y (H1 : t_eq (f x) (f y)) : t_eq (f x) (f y).
  apply (projT1 (f_dec x y)); intros H2.
  apply (projT1 (f_dec x x)); intros H3.
  exact (coe (fun z => t_eq (f x) z) H2 (sym H3)).
  apply (H3 (t_refl _)).
  apply (H2 H1).
Defined.
Definition f_dec_eq_refl {A f} (f_dec : Dec_f A f)
  x (H1 : t_eq (f x) (f x)) : t_eq (f_dec_eq f_dec x x H1) (t_refl _).
  unfold f_dec_eq; apply (projT2 (f_dec x x)).
  intros H2; unfold c_inl; destruct H2; reflexivity.
  intros H2; apply (H2 (t_refl _)).
Defined.
Definition f_dec_uip {A f} (f_dec : Dec_f A f)
  x y (H1 H2 : t_eq x y) : t_eq (ap f H1) (ap f H2).
  destruct H2; cbn.
  destruct (f_dec_eq_refl f_dec x (ap f H1)).
  destruct H1.
  exact (sym (f_dec_eq_refl f_dec x (t_refl _))).
Defined.
Definition fix_f {A f} (x : A) (p : t_eq (f x) x) :
    t_eq (existT (fun x => t_eq (f x) x) (f x) (ap f p)) (existT _ x p).
  apply (sig_ext (existT _ _ _) (existT _ _ _) p); cbn.
  apply (coe_inj (fun z => t_eq (f z) x) (sym p)).
  refine (match p with | t_refl _ => _ end); cbn.
  refine (match p with | t_refl _ => _ end); cbn.
  reflexivity.
Defined.

Definition fix_I {A f} (f_dec : Dec_f A f)
  (f_I : forall x, t_eq (f (f x)) (f x)) (x : A) (p : t_eq (f x) x) :
    t_eq (existT (fun x => t_eq (f x) x) (f x) (f_I x)) (existT _ x p).
  destruct (fix_f (f x) (f_I x)).
  destruct (fix_f x p), (fix_f (f x) (ap f p)).
  destruct (f_dec_uip f_dec (f (f x)) (f x) (f_I x) (ap f p)).
  reflexivity.
Defined.

(* bool *)
(* specific instances *)

Definition C_Bool : Type := forall A, A -> A -> A.
Definition c_true : C_Bool := fun A t f => t.
Definition c_false : C_Bool := fun A t f => f.

Definition I_Bool (c_b : C_Bool) : Type :=
  forall P, P c_true -> P c_false -> P c_b.
Definition i_true : I_Bool c_true := fun P t f => t.
Definition i_false : I_Bool c_false := fun P t f => f.

Definition W_Bool : Type := {c_b : C_Bool & I_Bool c_b}.
Definition w_true : W_Bool := existT _ c_true i_true.
Definition w_false : W_Bool := existT _ c_false i_false.

Definition H_Bool : Type := forall A, A -> A -> A.
Definition h_true : H_Bool := fun A t f => t.
Definition h_false : H_Bool := fun A t f => f.

(* axioms usage starts here *)
Axiom lift_c_bool : C_Bool -> H_Bool.
Axiom lift_c_true : t_eq (lift_c_bool c_true) h_true.
Axiom lift_c_false : t_eq (lift_c_bool c_false) h_false.

Definition c_to_w (c_b : C_Bool) : W_Bool :=
  lift_c_bool c_b _ w_true w_false.
Definition c_next (c_b : C_Bool) : C_Bool :=
  projT1 (c_to_w c_b).
Definition c_next_ind c_b : I_Bool (c_next c_b) :=
  projT2 (c_to_w c_b).
Definition c_next_I c_b : t_eq (c_next (c_next c_b)) (c_next c_b).
  apply (c_next_ind c_b); clear c_b.
  unfold c_next, c_to_w; rewrite lift_c_true; reflexivity.
  unfold c_next, c_to_w; rewrite lift_c_false; reflexivity.
Defined.
(* axioms usage ends here *)

Definition c_true_neq_c_false : t_eq c_true c_false -> C_False :=
  fun H1 => @coe C_Bool _ _ (fun c_b => c_b Type C_Unit C_False) H1 c_unit.

Definition c_next_dec : Dec_f C_Bool c_next.
  intros l_c_b r_c_b.
  apply (c_next_ind l_c_b); apply (c_next_ind r_c_b).
  apply w_inl; reflexivity.
  apply w_inr; intros H; exact (c_true_neq_c_false H).
  apply w_inr; intros H; exact (c_true_neq_c_false (sym H)).
  apply w_inl; reflexivity.
Defined.

Definition Bool : Type := { c_b : C_Bool & t_eq (c_next c_b) c_b }.
Definition true : Bool := existT _ (c_next c_true) (c_next_I c_true).
Definition false : Bool := existT _ (c_next c_false) (c_next_I c_false).

Definition next (b : Bool) : Bool :=
  existT _ (c_next (projT1 b)) (c_next_I (projT1 b)).
Definition ind_next b : forall P, P true -> P false -> P (next b).
  intros P t f; destruct b as [c_b H1]; unfold next; cbn; destruct H1.
  apply (c_next_ind c_b); auto.
Defined.
Definition mod_next b : t_eq (next b) b.
  destruct b as [c_b H1]; unfold next; cbn.
  apply (fix_I c_next_dec c_next_I).
Defined.
Definition ind b : forall P, P true -> P false -> P b.
  destruct (mod_next b); exact (ind_next b).
Defined.