better_than_agda.v

Set Universe Polymorphism.
Set Definitional UIP.

Inductive eqP (A : Type) (x : A) : A -> SProp :=
  | eqP_refl : eqP A x x.

Definition C_Bool : Type := forall A, A -> A -> A.
Definition c_true : C_Bool := fun A x y => x.
Definition c_false : C_Bool := fun A x y => y.

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

Record Bool : Type := {
  c_b : C_Bool;
  i_b : I_Bool c_b;
  w : c_b SProp
    (forall H : eqP _ c_b c_true,
      eqP _ i_true match H with
      | eqP_refl _ _ => i_b
      end)
    (forall H : eqP _ c_b c_false,
      eqP _ i_false match H with
      | eqP_refl _ _ => i_b
      end)
}.

Definition true : Bool :=
  {|
    c_b := c_true;
    i_b := i_true;
    w := fun H => eqP_refl _ _
  |}.
Definition false : Bool :=
  {|
    c_b := c_false;
    i_b := i_false;
    w := fun H => eqP_refl _ _
  |}.

Lemma ind b : forall P : Bool -> Type, P true -> P false -> P b.
  intros P x y.
  destruct b as [c_b i_b w].
  refine (i_b (fun i_c_b =>
    forall (eq : eqP _ c_b i_c_b) w,
    P {|
      c_b := i_c_b;
      i_b := 
        match eq with
        | eqP_refl _ _ => i_b
        end;
      w := w;
    |}
  ) _ _ (eqP_refl _ _) w).
  clear w; intros eq w; unfold true, c_true in *; simpl in *.
  destruct (w (eqP_refl _ _)).
  exact x.
  clear w; intros eq w; unfold false, c_false in *; simpl in *.
  destruct (w (eqP_refl _ _)).
  exact y.
Defined.