bool_by_j.v

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.

Definition C_Bool : Prop := 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) : Prop :=
  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 : Prop := {c_b : C_Bool | I_Bool c_b}.
Definition w_true : W_Bool := exist _ c_true i_true.
Definition w_false : W_Bool := exist _ c_false i_false.

Definition c_next (c_b : C_Bool) : C_Bool :=
  proj1_sig (c_b W_Bool w_true w_false).
Definition c_next_i (c_b : C_Bool) : I_Bool (c_next c_b) :=
  proj2_sig (c_b W_Bool w_true w_false).

Definition Bool : Prop := {c_b : C_Bool | c_next c_b = c_b}.
Definition true : Bool := exist _ c_true eq_refl.
Definition false : Bool := exist _ c_false eq_refl.

Definition true_next_eq {c_b : C_Bool}
  (w : c_true = c_b) : c_true = c_b.
  assert (c_next c_b = c_b).
  exact (
    match w in (_ = c_b) return (c_next c_b = c_b)
    with
    | eq_refl => eq_refl
    end
  ).
  revert w H.
  apply (c_next_i c_b).
  intros w H; exact H.
  intros w H; exact w.
Defined.
  Definition false_next_eq {c_b : C_Bool}
  (w : c_false = c_b) : c_false = c_b.
  assert (c_next c_b = c_b).
  exact (
    match w in (_ = c_b) return (c_next c_b = c_b)
    with
    | eq_refl => eq_refl
    end
  ).
  revert w H.
  apply (c_next_i c_b).
  intros w H; exact w.
  intros w H; exact H.
Defined.
Definition true_eq w : true = exist _ c_true w.
  apply (sig_ext true (exist _ _ _) w).
  unfold eq_rect; simpl.
  exact (
    match w in (_ = c_b) return true_next_eq w = w with
    | eq_refl => eq_refl
    end
  ).
Defined.
Definition false_eq w : false = exist _ c_false w.
  apply (sig_ext false (exist _ _ _) w).
  unfold eq_rect; simpl.
  refine (
    match w in (_ = c_b) return false_next_eq w = w with
    | eq_refl => eq_refl
    end
  ).
Defined.

Definition ind (b : Bool) : forall P : Bool -> Prop, P true -> P false -> P b.
  intros P t f; destruct b as [c_b w]; simpl in *.
  refine (
    match w with
    | eq_refl => _
    end w
  ); clear w.
  apply (c_next_i c_b); intros w.
  rewrite <- (true_eq w); exact t.
  rewrite <- (false_eq w); exact f.
Defined.

🔥

Interesting...