either_by_j.v

Definition id {A : Prop} (x : A) : A := x.
Definition J1 {A} {x y : A} (p : x = y)
  (C : forall y : A, x = y -> Prop) (H : C x eq_refl) : C y p :=
  match p as q in (_ = z) return C z q with | eq_refl => H end.
Definition J {A} {x y : A} (p : x = y) :
  exist (fun y => x = y) x eq_refl = exist (fun y => x = y) y p.
  apply (J1 p); reflexivity.
Defined.
Definition coe {A} {x y : A} (p : x = y) (C : A -> Prop) (H : C x) : C y :=
  J1 p (fun z _ => C z) H.
Definition coe2 {A B x_a x_b y_a y_b} (p : exist B x_a x_b = exist B y_a y_b)
  (C : forall (a : A), B a -> Prop) (H : C x_a x_b)
  : C y_a y_b := coe p (fun '(exist _ f s) => C f s) H.

Definition cast {A B : Prop} (p : A = B) (a : A) : B :=
  coe p (fun T => T) a.
Notation "p # x" := (cast p x)
  (at level 60, right associativity).
Definition sym {A} {x y : A} (p : x = y) : y = x :=
  coe p (fun z => z = x) (eq_refl x).
Definition ap {A B x y} (f : A -> B) (H : x = y) : f x = f y :=
  coe H (fun z => f x = f z) (eq_refl (f x)).
Definition ap2 {T A} {B : A -> Prop} {l_a l_b r_a r_b} (f : forall a, B a -> T)
  (p : exist B l_a l_b = exist B r_a r_b) : f l_a l_b = f r_a r_b :=
  ap (fun '(exist _ x_a x_b) => f x_a x_b) p.
(* Definition ap_B_is_eq {A x y} {L R : A -> Prop}
  (p : x = y) : ap (fun a => L a = R a) p = ap (fun a => L a = R a) p. *)

Definition ap_sym {A B x y} (f : A -> B) (p : x = y)
  : ap f (sym p) = sym (ap f p).
  apply (coe2 (J p)); reflexivity.
Defined.
Definition ap_ap {A B C x y} (f : A -> B) (g : B -> C)
  (p : x = y) : ap g (ap f p) = ap (fun x => g (f x)) p.
  apply (coe2 (J p)); reflexivity.
Defined.
(* Definition ap_eq_f_to_ap {A B x y} {f : A -> B} (p : x = y) :
  ap (fun z => f x = f z) p = ap (fun z => f x = f z) p.
  epose (ap (fun z => f x = f z) p).
  epose (ap (ap f)).
  simpl in *.
  apply (coe2 (J p)); simpl.
  apply (coe2 (J (f_eq_g x))); reflexivity. *)
Definition apD {A B x y} (f : forall (x : A), B x)
  (p : x = y) : ap B p # (f x) = f y :=
  coe2 (J p) (fun z p => ap B p # (f x) = f z) eq_refl.
Definition trans {A} {x y z : A} (p : x = y) (q : y = z) : x = z :=
  coe q (fun y => x = y) p.
Notation "p @ q" := (trans p q)
  (at level 40, left associativity).
Definition trans_assoc {A} {w x y z : A} (p : w = x) (q : x = y) (r : y = z)
  : p @ q @ r = p @ (q @ r).
  apply (coe2 (J r)); simpl; reflexivity.
Defined.
Definition trans_sym {A} {x y : A} (p : x = y) : eq_refl = sym p @ p.
  apply (coe2 (J p)); simpl; reflexivity.
Defined.
Definition trans_ap {A} (f : A -> A) {x y z} (p : x = y) (q : y = z) 
  : ap f p @ ap f q = ap f (p @ q).
  apply (coe2 (J q)); simpl; reflexivity.
Defined.
Definition trans_refl {A} {x y : A} (p : x = y) : eq_refl @ p = p.
  apply (coe2 (J p)); simpl; reflexivity.
Defined.
Definition coe_inj {A} {x y : A} (C : A -> Prop)
  (p : x = y) {H1 H2} (H : coe p C H1 = coe p C H2) : H1 = H2.
  revert H1 H2 H; apply (coe2 (J p)); intros H1 H2 H; exact H.
Defined.

Definition ap_id {A : Prop} {x y : A} (p : x = y) : ap id p = p.
  apply (coe2 (J p)); reflexivity.
Defined.
Definition ap_funext {A B x y} {f g : A -> B} (f_eq_g : forall a, f a = g a)
  (p : x = y) : ap f p = f_eq_g x @ (ap g p) @ (sym (f_eq_g y)).
  apply (coe2 (J p)); simpl.
  apply (coe2 (J (f_eq_g x))).
  reflexivity.
Defined.

Definition fst {A} {B : A -> Prop} (p : sig B) : A := proj1_sig p.
Definition snd {A} {B : A -> Prop} (p : sig B) : B (fst p) := proj2_sig p.
Lemma sig_ext {A} {B : A -> Prop} {l_a l_b r_a r_b}
  (p_a : l_a = r_a) (p_b : ap B p_a # l_b = r_b)
  : exist B l_a l_b = exist B r_a r_b.
  apply (coe (ap (fun x_b => exist B r_a x_b) p_b)).
  exact (ap2 (fun x_a p_x => exist B x_a (ap B p_x # l_b)) (J p_a)).
Defined.
Definition sig_ext_ap_fst {A} {B : A -> Prop} {l_a l_b r_a r_b}
  (p_a : l_a = r_a) (p_b : ap B p_a # l_b = r_b)
  : ap fst (sig_ext p_a p_b) = p_a.
  unfold sig_ext.
  (* TODO: ugly *)
  apply (coe2 (J p_b)); simpl.
  apply (coe2 (J p_a)); simpl.
  reflexivity.
Defined.

Definition C_Eq {A : Prop} f (a : A) := f a = a.
Definition coe_c_eq {A f} {x y} (p : x = y) (q : @C_Eq A f x)
    : sym (ap f p) @ q @ p = coe p (C_Eq f) q.
  apply (coe2 (J p)); simpl.
  exact (trans_refl q).
Defined.
Lemma sig_c_eq_ext {A : Prop} (f : A -> A) {l_a l_b r_a r_b}
  (p_a : l_a = r_a) (p_b : sym (ap f p_a) @ l_b @ p_a = r_b)
  : exist (C_Eq f) l_a l_b = exist (C_Eq f) r_a r_b.
  apply (sig_ext p_a).
  apply (coe p_b (fun p => _ = p)).
  apply (coe2 (J p_a)); simpl.
  exact (sym (trans_refl l_b)).
Defined.
Definition c_ind {A f a} (c : @C_Eq A f a)
  : exist (C_Eq f) (f a) (ap f c) = exist (C_Eq f) a c.
  apply (sig_c_eq_ext f c).
  apply (coe (trans_sym (ap f c)) (fun p => p @ _ = _)).
  exact (trans_refl c).
Defined.

Lemma sig_c_eq_snd {A : Prop} (f : A -> A) {l_a l_b r_a r_b}
  (p : exist (C_Eq f) l_a l_b = exist (C_Eq f) r_a r_b)
  : sym (ap f (ap fst p)) @ l_b @ (ap fst p) = r_b.
  apply (coe (apD snd p) (fun p => _ = p)); clear; simpl.
  refine (match p with | eq_refl => _ end); simpl.
  exact (trans_refl l_b).
Defined.

Section C_Eq_F.
  Variable A : Prop.
  Variable f : A -> A.
  Variable f_I : forall a, C_Eq f (f a).
  Variable f_J : forall a, f_I (f a) = ap f (f_I a).
  (* Variable f_J : forall a,
    coe (f_I a) (C_Eq f) (f_I (f a)) = f_I a. *)

  Definition c_f {x y} (c : f x = y) : C_Eq f y :=
    sym (ap f c) @ f_I x @ c.
  Definition c_f_ind {x y} (c : f x = y) :
    exist (C_Eq f) (f x) (f_I x) = exist (C_Eq f) y (c_f c) :=
    sig_c_eq_ext f c eq_refl.
  Definition c_f_I {x y} (c : f x = y) : C_Eq c_f (c_f c).
    apply (coe2 (c_f_ind c)).
    unfold C_Eq, c_f; apply (coe (sym (f_J x))).
    apply (coe (trans_sym (ap f (f_I x)))).
    exact (trans_refl (f_I x)).
  Defined.
  Definition c_ap_c_f_eq_f_I {x y} (c : f x = y) :
    f_I y = ap f (c_f c).
    apply (coe2 (c_f_ind c)).
    exact (f_J x).
  Defined.
  Definition c_f_J {x y} (c : f x = y) :
    ap f (c_f c) = c_f (ap f c).
    unfold c_f.
    apply (coe (trans_ap f _ _)).
    apply (coe (trans_ap f _ _)).
    (* TODO: this is lazy *)
    apply (coe2 (J c)).
    apply (coe (f_J x)).
    reflexivity.
  Defined.
  (* TODO: this one is weird here *)
  Definition c_ap_trunct_eq_c_f_trunct {a} (c : C_Eq f a)
    : (f_I a = ap f c) = (c_f c = c).
    apply (coe (c_ind c) (fun '(exist _ q q_I) => (_ = ap f c) = _)).
    apply (coe (c_f_J c)); apply (coe (c_ap_c_f_eq_f_I c)); reflexivity.
  Defined.
End C_Eq_F.
Arguments c_f {A f} f_I {x y} c.
Arguments c_f_ind {A f} f_I {x y} c.
Arguments c_f_I {A f f_I} f_J {x y} c.
Arguments c_ap_c_f_eq_f_I {A f f_I} f_J {x y} c.
Arguments c_f_J {A f f_I} f_J {x y} c.
Arguments c_ap_trunct_eq_c_f_trunct {A f f_I} f_J {a} c.

Definition split_coe_l {A : Prop} {f} {l r : A} (p : f l = r) (q : f (f l) = f l) :
  coe p (fun x => f r = x) (coe p (fun x => f x = f l) q) =
    coe p (fun a => f a = a) q.
  apply (coe2 (J p)); reflexivity.
Defined.
Definition split_coe_r {A : Prop} {f} {l r : A} (p : f l = r) (q : f r = r) :
  coe (sym p) (fun x => f (f l) = x)
    (coe (sym p) (fun x => f x = r) q) =
  coe (sym p) (fun a => f a = a) q.
  revert q; apply (coe2 (J p)); intros q; reflexivity.
Defined.
Definition coe_sym_refl_l {A : Prop} {C : A -> Prop} {x y : A}
  (p : x = y) : eq_refl = coe (sym p) (fun z => x = z) p.
  apply (coe2 (J p)); reflexivity.
Defined.

Section Either.
  Definition C_Either (A B : Prop) : Prop := forall (C : Prop),
    (A -> C) -> (B -> C) -> C.
  Definition c_left {A B} a : C_Either A B := fun C l r => l a.
  Definition c_right {A B} b : C_Either A B := fun C l r => r b.

  (* this can be done by encoding the booleans first *)
  Definition P_Either A B : Prop :=
    exists (b : bool), if b then A else B : Prop.
  Definition p_left {A B} a : P_Either A B :=
    (ex_intro _ true a).
  Definition p_right {A B} b : P_Either A B :=
    (ex_intro _ false b).
  Definition p_ind {A B} (p : P_Either A B)
    (C : P_Either A B -> Prop)
      (l : forall a, C (p_left a))
      (r : forall b, C (p_right b)) : C p.
    destruct p as [b x]; destruct b.
    apply l.
    apply r.
  Defined.

  Definition c_out {A B} (c : C_Either A B) : P_Either A B :=
    c (P_Either A B) p_left p_right.
  Definition c_box {A B} (p : P_Either A B) : C_Either A B.
    apply (p_ind p (fun p => C_Either A B)).
    apply c_left; exact x.
    apply c_right; exact x.
  Defined.

  Definition c_next {A B} (c : C_Either A B) := c_box (c_out c).
  Definition c_next_ind {A B} (c : C_Either A B)
    (C : C_Either A B -> Prop)
      (l : forall a, C (c_left a))
      (r : forall b, C (c_right b)) : C (c_next c).
    unfold c_next; apply (p_ind (c_out c)); auto.
  Defined.
  Definition c_next_I {A B} (c : C_Either A B)
    : c_next (c_next c) = c_next c.
    apply (c_next_ind c (C_Eq c_next)); intros x; reflexivity.
  Defined.
  Definition c_next_J {A B} (c : C_Either A B)
    : c_next_I (c_next c) = ap c_next (c_next_I c).
    unfold c_next_I, c_next, c_next_ind.
    apply (p_ind (c_out c)); auto.
  Defined.

  Definition c_out_I {A B} (c : C_Either A B)
    : c_out (c_next c) = c_out c.
    unfold c_next; destruct (c_out c) as [b x].
    destruct b; auto.
  Defined.
  Definition c_out_box {A B} (p : P_Either A B)
    : c_out (c_box p) = p.
    destruct p as [b x]; destruct b; auto.
  Defined.
  
  Definition K_Eq {A B} (c : C_Either A B) : Prop := {
    c_I : C_Eq c_next c |
    ap c_out c_I = c_out_I c
  }.
  Definition k_refl {A B} (c : C_Either A B) : K_Eq (c_next c).
    apply (c_next_ind c).
    intros a; exists eq_refl; reflexivity.
    intros b; exists eq_refl; reflexivity.
  Defined.
  Definition k_ap {A B c} (k : @K_Eq A B c) : K_Eq (c_next c) :=
    ap K_Eq (sym (fst k)) # k.
  Definition k_ind_w {A B c} (k : @K_Eq A B c)
      (C : forall c, K_Eq c -> Prop)
    (H : forall c_J, C (c_next c) (exist _ (c_next_I c) c_J)) : C c k.
    destruct k as [c_I c_J].
    assert (c_next_I c = ap c_next c_I) as H0.
    apply (coe (ap_ap c_out c_box c_I) (fun q => _ = q)).
    apply (coe (sym c_J)); apply (coe c_I); apply (c_next_ind c); auto.
    refine (coe (c_ap_trunct_eq_c_f_trunct c_next_J c_I # H0)
      (fun c_I => forall c_J, C c _) _ c_J); clear H0 c_J.
    apply (coe2 (c_f_ind c_next_I c_I)); exact H.
  Defined.
  Definition k_mod_spin {A B c} (k : @K_Eq A B c)
    : exist K_Eq (c_next c) (k_ap k) = exist K_Eq c k.
    apply (sig_ext (proj1_sig k)); unfold k_ap.
    exact (coe2 (J (proj1_sig k)) (fun z q => forall k, ap K_Eq q #
      ap K_Eq (sym q) # k = k) (fun k => eq_refl) k).
  Defined.
  Definition ap_f_out_l {A B} {x y r} (p : x = y) (f : A -> B) :
    ap (fun z => z = r) (ap f p) = ap (fun z => f z = r) p.
    apply (coe2 (J p)); reflexivity.
  Defined.

  Definition ap_out_box_is_id {A B} {x y} (p : x = y) :
    ap (fun z => @c_out A B (c_box z)) p =
      c_out_box x @ p @ sym (c_out_box y).
    apply (coe (ap_id p) (fun q =>
      ap (fun p => c_out (c_box p)) p = _ @ q @ _)).
    exact (ap_funext c_out_box p).
  Defined.
  Definition k_ap_refl {A B c} (k : @K_Eq A B c) : k_ap k = k_refl c.
    refine (coe (proj1_sig k) (fun c => _) _ k); clear k; intros k.
    apply (k_ind_w k); clear k; apply (c_next_ind c); clear c.
    -
      (* duplicated just because I'm lazy *)
      intros a c_J; unfold k_ap; simpl.
      apply (sig_ext (ap (ap c_box) c_J)); simpl.
      apply (coe (ap_f_out_l (ap (ap c_box) c_J) (ap c_out))).
      apply (coe (sym (ap_ap (ap c_box) (ap c_out) c_J))).
      apply (coe (sym (ap_funext (ap_ap c_box c_out) c_J))).
      unfold ap_ap; simpl; rewrite (trans_refl _).
      enough (c_J = ap (ap (fun x => c_out (c_box x))) c_J) as H.
      apply (coe H (fun q_J => ap (fun z => z = c_out_I _) q_J # _ = _)).
      apply (coe2 (J c_J) (fun q_I q_J =>
        ap (fun z => z = _) q_J # q_J = eq_refl)); reflexivity.
      apply (coe (sym (ap_funext ap_out_box_is_id c_J))); cbn.
      rewrite trans_refl.
      apply (coe (sym (ap_funext trans_refl c_J))
        (fun q_J => _ = q_J)); cbn; rewrite trans_refl.
      exact (sym (ap_id c_J)).
    -
      intros a c_J; unfold k_ap; simpl.
      apply (sig_ext (ap (ap c_box) c_J)); simpl.
      apply (coe (ap_f_out_l (ap (ap c_box) c_J) (ap c_out))).
      apply (coe (sym (ap_ap (ap c_box) (ap c_out) c_J))).
      apply (coe (sym (ap_funext (ap_ap c_box c_out) c_J))).
      unfold ap_ap; simpl; rewrite (trans_refl _).
      enough (c_J = ap (ap (fun x => c_out (c_box x))) c_J) as H.
      apply (coe H (fun q_J => ap (fun z => z = c_out_I _) q_J # _ = _)).
      apply (coe2 (J c_J) (fun q_I q_J =>
        ap (fun z => z = _) q_J # q_J = eq_refl)); reflexivity.
      apply (coe (sym (ap_funext ap_out_box_is_id c_J))); cbn.
      rewrite trans_refl.
      apply (coe (sym (ap_funext trans_refl c_J))
        (fun q_J => _ = q_J)); cbn; rewrite trans_refl.
      exact (sym (ap_id c_J)).
  Defined.
  Definition k_elim {A B c} (k : @K_Eq A B c)
    : exist K_Eq (c_next c) (k_refl c) = exist K_Eq c k.
    apply (coe (k_mod_spin k) (fun x => _ = x)).
    apply (coe (k_ap_refl k)); reflexivity.
  Defined.

  Definition Either (A B : Prop) : Prop := {c : C_Either A B | K_Eq c}.
  Definition left {A B} (a : A) : Either A B :=
    exist K_Eq (c_left a) (k_refl (c_left a)).
  Definition right {A B} (b : B) : Either A B :=
    exist K_Eq (c_right b) (k_refl (c_right b)).

  Definition ind {A B} (e : Either A B) (C : Either A B -> Prop)
    (l : forall a, C (left a)) (r : forall b, C (right b)) : C e.
    destruct e as [c k]; simpl.
    apply (coe2 (k_elim k)); apply (coe (proj1_sig k)); clear k.
    apply (c_next_ind c); auto.
  Defined.
End Either.