k_box.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.

Section P_Box.
  Variable T : Prop.
  Definition D_Box : Prop := forall A, (T -> A) -> A.
  Definition d_box (x : T) : D_Box := fun A k => k x.
  Definition d_out (d : D_Box) : T := d T (fun x => x).
  Definition d_f (d : D_Box) : D_Box := d_box (d_out d).

  Definition P_Box := {d : D_Box | d_f d = d}.
  Definition p_box (x : T) : P_Box := exist _ (d_box x) eq_refl.
  Definition p_out (p : P_Box) : T := d_out (fst p).
  Definition p_f (p : P_Box) : P_Box := p_box (p_out p).
End P_Box.

Definition sig_coe_through {T} {x y : T} {A} {B : forall (z : T), A z -> Prop}
  (p : x = y) H :
    exist (B y) (coe p A (proj1_sig H))
      (coe2 (J p) (fun z p => B z (coe p A (proj1_sig H))) (proj2_sig H)) =
    coe p (fun z => {a : A z | B z a}) H.
  apply (coe2 (J p)); destruct H; reflexivity.
Defined.
Section K_Eq.
  Variable T : Prop.
  Definition A : Prop := P_Box T.
  Definition f : A -> A := p_f T.
  Definition f_I a : C_Eq f (f a) := eq_refl.
  Definition f_J a : f_I (f a) = ap f (f_I a) := eq_refl.

  Definition K_Eq a := {
    c_I : C_Eq f a |
    ap (p_out _) c_I = eq_refl
  }.
  Definition k_refl a : K_Eq (f a) := exist _ eq_refl eq_refl.
  Definition k_ap {a} (k : K_Eq a) : K_Eq (f a) :=
    ap K_Eq (sym (fst k)) # k.
  Definition k_ind_w {a} (k : K_Eq a) (C : forall a, K_Eq a -> Prop)
    (H : forall c_J, C (f a) (exist _ (f_I a) c_J)) : C a k.
    destruct k as [c_I c_J].
    assert (f_I a = ap f c_I).
    unfold f, p_f.
    apply (coe (ap_ap (p_out T) (p_box T) c_I) (fun q => _ = q)).
    apply (coe (sym c_J)); reflexivity.
    refine (
      match c_ap_trunct_eq_c_f_trunct f_J c_I # H0 with
      | eq_refl => _
      end c_J
    ).
    apply (coe2 (c_f_ind f_I c_I)); exact H.
  Defined.
  Definition k_mod_spin {a} (k : K_Eq a)
    : exist K_Eq (f a) (k_ap k) = exist K_Eq a 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 k_ap_refl {a} (k : K_Eq a) : k_ap k = k_refl a.
    apply (k_ind_w k); clear k; intros c_J.
    unfold k_ap; apply (sig_ext (ap (ap (p_box _)) c_J)); simpl.
    assert (
      ap (fun c_I => ap (p_out T) c_I = eq_refl)
        (ap (ap (p_box T)) c_J) =
      ap (fun c_I => c_I = eq_refl)
        (ap (ap (p_out T)) (ap (ap (p_box T)) c_J))
    ).
    apply (coe2 (J c_J)); reflexivity.
    apply (coe (sym H) (fun p => p # c_J = eq_refl)); clear H.
    rewrite (ap_ap (ap (p_box T)) (ap (p_out T))).
    epose (H := fun (x : p_out T (f (f a)) = p_out T (f a)) =>
      ap_ap (p_box T) (p_out T) x @ ap_id x).
    apply (coe (sym (ap_funext H c_J))).
    unfold H, ap_ap; simpl.
    apply (coe (sym (trans_refl _))).
    apply (coe (sym (ap_id c_J))
      (fun p => ap (fun c_I => c_I = eq_refl) p # c_J = eq_refl)).
    apply (coe2 (J c_J)); reflexivity.
  Defined.
  Definition k_elim {a} (k : K_Eq a)
    : exist K_Eq (f a) (k_refl a) = exist K_Eq a k.
    apply (coe (k_mod_spin k) (fun x => _ = x)).
    apply (coe (k_ap_refl k)); reflexivity.
  Defined.
End K_Eq.