https://proofassistants.stackexchange.com/questions/3841/assistance-using-destruct-on-an-equality-proof-for-functors/3843

F.v

(* https://proofassistants.stackexchange.com/questions/3841/assistance-using-destruct-on-an-equality-proof-for-functors/3843 *)

(* Proof of associativity of functor composition without UIP *)

(* 1. Intuition: treat equality as a proper algebraic structure:
      think of it as a category (aka. the discrete category), not an equivalence relation. *)
(* 1a. An equality between morphisms, f = g, becomes the existence of a morphism between f and g. *)
(* 1b. In the definition of a category, homsets are thus categories.
       The resulting structure is known as a 2-category. https://ncatlab.org/nlab/show/2-category
       You can kepp applying the same generalization to the morphism category, resulting
       in the concepts of n-category and infinity-category. https://ncatlab.org/nlab/show/infinity-category *)
(* 2. In the definition of Functor_Composition, we need to prove
      AF G (AF F (o f g)) = o (AF G (AF F f)) (AF G (AF F g)).
      Reinterpret that as constructing a "=-morphism" (morphism in the discrete category)
      between those two "B-morphisms" (where B is the category containing f and g). *)
(* 2a. Instead of "rewrite", use categorical constructs in the "=" category:
       - eq_trans : x = y -> y = z -> x = z   (composition of morphisms, aka. transitivity)
       - f_equal : forall (f : A -> B) (x y : A), x = y -> f x = f y   (functions are endofunctors in "=")
         especially the specialization to the functor mapping
         f_equal (AF F) : f = g -> AF F f = AF F g
       (also of course, eq_refl : x = x)
       Their equations can be found via "Search eq_trans" and "Search f_equal".
*)
(* 3. In the proof of associativity of Functor_Composition, equalities between equalities can now
      be reasoned about as equalities between morphism.
      It's just category theory in the discrete category. *)

Definition Function_Extensionality := forall (A:Type) (B: A -> Type) (f g: (forall (a:A),B a)), (forall a: A, f a = g a) -> f = g.

Record  Category_By_Hom_Types := {
object_type                 :  Type;
morphism_type               : object_type -> object_type -> Type;
identity_morphism           : forall (A: object_type), (morphism_type A A);
morphism_composition        : forall (X Y Z: object_type) (g : (morphism_type Y Z)) (f : (morphism_type X Y)), (morphism_type X Z);
composition_associator      : forall (W X Y Z: object_type) (h : (morphism_type Y Z)) (g : (morphism_type X Y)) (f : (morphism_type W X)), morphism_composition _ _ _ h (morphism_composition _ _ _ g f) = (morphism_composition _ _ _ (morphism_composition _ _ _ h g) f);
identity_morphism_left_unitor : forall (X Y: object_type) (f: (morphism_type X Y)), morphism_composition _ _ _ (identity_morphism Y) f = f;
identity_morphism_right_unitor : forall (X Y: object_type) (f: (morphism_type X Y)), morphism_composition _ _ _ f (identity_morphism X) = f;
}.

(* Shorthands for Categories *)
Notation CHT := Category_By_Hom_Types.
Notation O := object_type.
Notation A := morphism_type.
Notation o := ( morphism_composition _ _ _ _ ).
Notation i := identity_morphism.
Notation i_left_unit := (identity_morphism_left_unitor).
Notation i_right_unit := (identity_morphism_right_unitor).
Notation o_assoc := composition_associator.

Record Functor_By_Hom_Types (C D : Category_By_Hom_Types) := {
map_of_objects : O C -> O D;
map_of_morphisms                    : forall (X Y: O C), (A C X Y) -> (A D ( map_of_objects X) (map_of_objects Y));
functor_commutes_with_composition   : forall (X Y Z: O C) (g: (A C Y Z)) (f: (A C X Y)), map_of_morphisms _ _ (o g f) = o (map_of_morphisms _ _  g) (map_of_morphisms _ _  f);
functor_commutes_with_identity      : forall (X: O C), map_of_morphisms _ _  (i C X) = (i D (map_of_objects X));
}.

(* Shorthands for Functors *)
Notation FHT := Functor_By_Hom_Types.
Notation OF := (map_of_objects _ _).
Notation AF F := (map_of_morphisms _ _ F _ _).
Notation comm_F := (functor_commutes_with_composition _ _).
Notation unit_F := (functor_commutes_with_identity _ _).

Lemma Functor_Composition : forall (B C D : CHT) (G: (FHT C D)) (F: (FHT B C)) ,(FHT B D).
Proof.
intros B C D G F.
unshelve econstructor.
- exact (fun X => OF G (OF F X)).
- exact (fun X Y f => AF G (AF F f)).
- cbn. intros.
  transitivity (AF G (o (AF F g) (AF F f))).
  + apply (f_equal (AF G)). apply (comm_F F).
  + apply (comm_F G).
- cbn. intros.
  transitivity (AF G (i C (OF F X))).
  + apply (f_equal (AF G)). apply (unit_F F).
  + apply (unit_F G).
Defined.

Notation oFunctor := (Functor_Composition _ _ _).

Parameter function_extensionality : Function_Extensionality.

Lemma Functor_Composition_Assoc : forall (B C D E : CHT) (H : FHT D E) (G : FHT C D) (F : FHT B C),
  oFunctor H (oFunctor G F) = oFunctor (oFunctor H G) F.
Proof.
  intros. unfold oFunctor; cbn. f_equal.
  - do 5 (apply function_extensionality; intros).
    (* With some simplified notations, this is an equality between morphisms (in the discrete category):
         o (EF H (o (EF G (comm_F F)) (comm_F G))) (comm_F H)
       = o (EF (oFunctor H G) (comm_F F)) (o (EF G (comm_F F)) (comm_F H))
       where o = eq_trans, EF K = f_equal (AF K)
       Proof by functoriality of EF ("eq_trans_map_distr")
       and associativity of o ("eq_trans_assoc").
       *)
    apply (eq_trans (f_equal (fun e => eq_trans e _) (eq_trans_map_distr (AF H) _ _))).
    apply (eq_trans (eq_sym (eq_trans_assoc _ _ _))).
    f_equal. apply f_equal_compose.
  - apply function_extensionality; intros.
    (* same as above, with unit_F instead of comm_F *)
    apply (eq_trans (f_equal (fun e => eq_trans e _) (eq_trans_map_distr (AF H) _ _))).
    apply (eq_trans (eq_sym (eq_trans_assoc _ _ _))).
    f_equal. apply f_equal_compose.
Defined.