(** * Functoriality of the comma category construction *)
Require Import Functor.Core NaturalTransformation.Core.
Require Import Functor.Composition.Core NaturalTransformation.Composition.Core.
Require Import NaturalTransformation.Composition.Laws.
Require Import Functor.Paths.
Require Import Category.Strict.
Require Comma.Core.
Local Set Warnings "-notation-overridden". (* work around bug #5567, https://coq.inria.fr/bugs/show_bug.cgi?id=5567, notation-overridden,parsing should not trigger for only printing notations *)
Import Comma.Core.
Local Set Warnings "notation-overridden".
Import Functor.Identity.FunctorIdentityNotations NaturalTransformation.Identity.NaturalTransformationIdentityNotations.
Require Import HoTT.Tactics PathGroupoids Types.Forall.

Set Implicit Arguments.
Generalizable All Variables.
Local Open Scope morphism_scope.
Local Open Scope category_scope.

(** The comma category construction is functorial in its category
    arguments.  We really should be using ∏ (dependent product) here,
    but I'm lazy, and will instead expand it out. *)

Local Ltac helper_t fwd_tac bak_tac fin :=
  repeat
    first [ fin
          | rewrite <- ?Category.Core.associativity;
            progress repeat first [ bak_tac
                                  | apply ap10; apply ap ]
          | rewrite -> ?Category.Core.associativity;
            progress repeat first [ fwd_tac
                                  | apply ap ]
          | rewrite <- !composition_of ].

Local Tactic Notation "helper" tactic(fin) constr(hyp_fwd) constr(hyp_bak) :=
  let H := fresh in
  let H' := fresh in
  pose proof hyp_fwd as H;
    pose proof hyp_bak as H';
    simpl in *;
    helper_t ltac:(rewrite -> H) ltac:(rewrite <- H') fin.

Local Ltac functorial_helper_t unfold_lem :=
  repeat (apply path_forall || intro); simpl;
  rewrite !transport_forall_constant; simpl;
  transport_path_forall_hammer; simpl;
  apply CommaCategory.path_morphism; simpl;
  unfold unfold_lem; simpl;
  repeat match goal with
           | _ => exact idpath
           | [ |- context[CommaCategory.g (transport ?P ?p ?z)] ]
             => simpl rewrite (@ap_transport _ P _ _ _ p (fun _ => @CommaCategory.g _ _ _ _ _ _ _) z)
           | [ |- context[CommaCategory.h (transport ?P ?p ?z)] ]
             => simpl rewrite (@ap_transport _ P _ _ _ p (fun _ => @CommaCategory.h _ _ _ _ _ _ _) z)
           | [ |- context[transport (fun y => ?f (?g y) ?z)] ]
             => simpl rewrite (fun a b => @transport_compose _ _ a b (fun y => f y z) g)
           | [ |- context[transport (fun y => ?f (?g y))] ]
             => simpl rewrite (fun a b => @transport_compose _ _ a b (fun y => f y) g)
           | _ => rewrite !CommaCategory.ap_a_path_object'; simpl
           | _ => rewrite !CommaCategory.ap_b_path_object'; simpl
         end.

Section functorial.
  Section single_source.
    Variables A B C : PreCategory.
    Variable S : Functor A C.
    Variable T : Functor B C.

    Section morphism_of.
      Variables A' B' C' : PreCategory.
      Variable S' : Functor A' C'.
      Variable T' : Functor B' C'.

      Variable AF : Functor A A'.
      Variable BF : Functor B B'.
      Variable CF : Functor C C'.

      Variable TA : NaturalTransformation (S' o AF) (CF o S).
      Variable TB : NaturalTransformation (CF o T) (T' o BF).

      Definition functorial_morphism_of_object_of : (S / T) -> (S' / T')
        := fun x => CommaCategory.Build_object
                      S' T'
                      (AF (CommaCategory.a x))
                      (BF (CommaCategory.b x))
                      (TB (CommaCategory.b x) o CF _1 (CommaCategory.f x) o TA (CommaCategory.a x)).

      Definition functorial_morphism_of_morphism_of
                 s d (m : morphism (S / T) s d)
      : morphism (S' / T') (functorial_morphism_of_object_of s) (functorial_morphism_of_object_of d).
A, B, C: PreCategory
S: Functor A C
T: Functor B C
A', B', C': PreCategory
S': Functor A' C'
T': Functor B' C'
AF: Functor A A'
BF: Functor B B'
CF: Functor C C'
TA: NaturalTransformation (S' o AF) (CF o S)
TB: NaturalTransformation (CF o T) (T' o BF)
s, d: S / T
m: morphism (S / T) s d
morphism (S' / T') (functorial_morphism_of_object_of s)
  (functorial_morphism_of_object_of d)
      Proof.
A, B, C: PreCategory
S: Functor A C
T: Functor B C
A', B', C': PreCategory
S': Functor A' C'
T': Functor B' C'
AF: Functor A A'
BF: Functor B B'
CF: Functor C C'
TA: NaturalTransformation (S' o AF) (CF o S)
TB: NaturalTransformation (CF o T) (T' o BF)
s, d: S / T
m: morphism (S / T) s d
morphism (S' / T') (functorial_morphism_of_object_of s)
  (functorial_morphism_of_object_of d)
        simpl in *.
A, B, C: PreCategory
S: Functor A C
T: Functor B C
A', B', C': PreCategory
S': Functor A' C'
T': Functor B' C'
AF: Functor A A'
BF: Functor B B'
CF: Functor C C'
TA: NaturalTransformation (S' o AF) (CF o S)
TB: NaturalTransformation (CF o T) (T' o BF)
s, d: CommaCategory.object S T
m: CommaCategory.morphism s d
CommaCategory.morphism (functorial_morphism_of_object_of s)
  (functorial_morphism_of_object_of d)
        refine (CommaCategory.Build_morphism
                  (functorial_morphism_of_object_of s)
                  (functorial_morphism_of_object_of d)
                  (AF _1 (CommaCategory.g m))
                  (BF _1 (CommaCategory.h m))
                  _).
A, B, C: PreCategory
S: Functor A C
T: Functor B C
A', B', C': PreCategory
S': Functor A' C'
T': Functor B' C'
AF: Functor A A'
BF: Functor B B'
CF: Functor C C'
TA: NaturalTransformation (S' o AF) (CF o S)
TB: NaturalTransformation (CF o T) (T' o BF)
s, d: CommaCategory.object S T
m: CommaCategory.morphism s d
T' _1 (BF _1 (CommaCategory.h m))
o CommaCategory.f (functorial_morphism_of_object_of s) =
CommaCategory.f (functorial_morphism_of_object_of d)
o S' _1 (AF _1 (CommaCategory.g m))
        unfold functorial_morphism_of_object_of; simpl.
A, B, C: PreCategory
S: Functor A C
T: Functor B C
A', B', C': PreCategory
S': Functor A' C'
T': Functor B' C'
AF: Functor A A'
BF: Functor B B'
CF: Functor C C'
TA: NaturalTransformation (S' o AF) (CF o S)
TB: NaturalTransformation (CF o T) (T' o BF)
s, d: CommaCategory.object S T
m: CommaCategory.morphism s d
T' _1 (BF _1 (CommaCategory.h m))
o (TB (CommaCategory.b s) o CF _1 (CommaCategory.f s)
   o TA (CommaCategory.a s)) =
TB (CommaCategory.b d) o CF _1 (CommaCategory.f d) o TA (CommaCategory.a d)
o S' _1 (AF _1 (CommaCategory.g m))
        clear.
A, B, C: PreCategory
S: Functor A C
T: Functor B C
A', B', C': PreCategory
S': Functor A' C'
T': Functor B' C'
AF: Functor A A'
BF: Functor B B'
CF: Functor C C'
TA: NaturalTransformation (S' o AF) (CF o S)
TB: NaturalTransformation (CF o T) (T' o BF)
s, d: CommaCategory.object S T
m: CommaCategory.morphism s d
T' _1 (BF _1 (CommaCategory.h m))
o (TB (CommaCategory.b s) o CF _1 (CommaCategory.f s)
   o TA (CommaCategory.a s)) =
TB (CommaCategory.b d) o CF _1 (CommaCategory.f d) o TA (CommaCategory.a d)
o S' _1 (AF _1 (CommaCategory.g m))
        abstract helper (exact (CommaCategory.p m)) (commutes TA) (commutes TB).
      Defined.

      Definition functorial_morphism_of : Functor (S / T) (S' / T').
A, B, C: PreCategory
S: Functor A C
T: Functor B C
A', B', C': PreCategory
S': Functor A' C'
T': Functor B' C'
AF: Functor A A'
BF: Functor B B'
CF: Functor C C'
TA: NaturalTransformation (S' o AF) (CF o S)
TB: NaturalTransformation (CF o T) (T' o BF)
Functor (S / T) (S' / T')
      Proof.
A, B, C: PreCategory
S: Functor A C
T: Functor B C
A', B', C': PreCategory
S': Functor A' C'
T': Functor B' C'
AF: Functor A A'
BF: Functor B B'
CF: Functor C C'
TA: NaturalTransformation (S' o AF) (CF o S)
TB: NaturalTransformation (CF o T) (T' o BF)
Functor (S / T) (S' / T')
        refine (Build_Functor
                  (S / T) (S' / T')
                  functorial_morphism_of_object_of
                  functorial_morphism_of_morphism_of
                  _
                  _);
        abstract (
            intros;
            apply CommaCategory.path_morphism; simpl;
            auto with functor
          ).
      Defined.
    End morphism_of.

    Section identity_of.
      Definition functorial_identity_of_helper x
      : @functorial_morphism_of_object_of _ _ _ S T 1 1 1 1 1 x = x.
A, B, C: PreCategory
S: Functor A C
T: Functor B C
x: S / T
functorial_morphism_of_object_of 1 1 x = x
      Proof.
A, B, C: PreCategory
S: Functor A C
T: Functor B C
x: S / T
functorial_morphism_of_object_of 1 1 x = x
        let A := match goal with |- ?A = ?B => constr:(A) end in
        let B := match goal with |- ?A = ?B => constr:(B) end in
        refine (@CommaCategory.path_object' _ _ _ _ _ A B 1%path 1%path _).
A, B, C: PreCategory
S: Functor A C
T: Functor B C
x: S / T
transport
  (fun X : A => morphism C (S _0 X)%object (T _0 (CommaCategory.b x))%object)
  1
  (transport
     (fun Y : B =>
      morphism C
        (S _0 (CommaCategory.a (functorial_morphism_of_object_of 1 1 x)))%object
        (T _0 Y)%object)
     1 (CommaCategory.f (functorial_morphism_of_object_of 1 1 x))) =
CommaCategory.f x
        exact (Category.Core.right_identity _ _ _ _ @ Category.Core.left_identity _ _ _ _)%path.
      Defined.

      Definition functorial_identity_of `{Funext}
      : @functorial_morphism_of
          _ _ _ S T
          1 1 1 1 1
        = 1%functor.
A, B, C: PreCategory
S: Functor A C
T: Functor B C
H: Funext
functorial_morphism_of 1 1 = 1%functor
      Proof.
A, B, C: PreCategory
S: Functor A C
T: Functor B C
H: Funext
functorial_morphism_of 1 1 = 1%functor
        path_functor; simpl.
A, B, C: PreCategory
S: Functor A C
T: Functor B C
H: Funext
{HO : functorial_morphism_of_object_of 1 1 = idmap &
transport
  (fun GO : CommaCategory.object S T -> CommaCategory.object S T =>
   forall s d : CommaCategory.object S T,
   CommaCategory.morphism s d -> CommaCategory.morphism (GO s) (GO d))
  HO (functorial_morphism_of_morphism_of 1 1) =
(fun s d : CommaCategory.object S T => idmap)}
        exists (path_forall _ _ functorial_identity_of_helper).
A, B, C: PreCategory
S: Functor A C
T: Functor B C
H: Funext
transport
  (fun GO : CommaCategory.object S T -> CommaCategory.object S T =>
   forall s d : CommaCategory.object S T,
   CommaCategory.morphism s d -> CommaCategory.morphism (GO s) (GO d))
  (path_forall (functorial_morphism_of_object_of 1 1) idmap
     functorial_identity_of_helper)
  (functorial_morphism_of_morphism_of 1 1) =
(fun s d : CommaCategory.object S T => idmap)
        simpl.
A, B, C: PreCategory
S: Functor A C
T: Functor B C
H: Funext
transport
  (fun GO : CommaCategory.object S T -> CommaCategory.object S T =>
   forall s d : CommaCategory.object S T,
   CommaCategory.morphism s d -> CommaCategory.morphism (GO s) (GO d))
  (path_forall (functorial_morphism_of_object_of 1 1) idmap
     functorial_identity_of_helper)
  (functorial_morphism_of_morphism_of 1 1) =
(fun s d : CommaCategory.object S T => idmap)
        functorial_helper_t functorial_identity_of_helper.
      Qed.
    End identity_of.
  End single_source.

  Section composition_of.
    Variables A B C : PreCategory.
    Variable S : Functor A C.
    Variable T : Functor B C.

    Variables A' B' C' : PreCategory.
    Variable S' : Functor A' C'.
    Variable T' : Functor B' C'.

    Variables A'' B'' C'' : PreCategory.
    Variable S'' : Functor A'' C''.
    Variable T'' : Functor B'' C''.

    Variable AF : Functor A A'.
    Variable BF : Functor B B'.
    Variable CF : Functor C C'.

    Variable TA : NaturalTransformation (S' o AF) (CF o S).
    Variable TB : NaturalTransformation (CF o T) (T' o BF).

    Variable AF' : Functor A' A''.
    Variable BF' : Functor B' B''.
    Variable CF' : Functor C' C''.

    Variable TA' : NaturalTransformation (S'' o AF') (CF' o S').
    Variable TB' : NaturalTransformation (CF' o T') (T'' o BF').

    Let AF'' := (AF' o AF)%functor.
    Let BF'' := (BF' o BF)%functor.
    Let CF'' := (CF' o CF)%functor.

    Let TA'' : NaturalTransformation (S'' o AF'') (CF'' o S)
      := ((associator_2 _ _ _)
            o (CF' oL TA)
            o (associator_1 _ _ _)
            o (TA' oR AF)
            o associator_2 _ _ _)%natural_transformation.
    Let TB'' : NaturalTransformation (CF'' o T) (T'' o BF'')
      := ((associator_1 _ _ _)
            o (TB' oR BF)
            o (associator_2 _ _ _)
            o (CF' oL TB)
            o associator_1 _ _ _)%natural_transformation.

    Definition functorial_composition_of_helper x
    : (functorial_morphism_of TA' TB' o functorial_morphism_of TA TB)%functor x
      = functorial_morphism_of TA'' TB'' x.
A, B, C: PreCategory
S: Functor A C
T: Functor B C
A', B', C': PreCategory
S': Functor A' C'
T': Functor B' C'
A'', B'', C'': PreCategory
S'': Functor A'' C''
T'': Functor B'' C''
AF: Functor A A'
BF: Functor B B'
CF: Functor C C'
TA: NaturalTransformation (S' o AF) (CF o S)
TB: NaturalTransformation (CF o T) (T' o BF)
AF': Functor A' A''
BF': Functor B' B''
CF': Functor C' C''
TA': NaturalTransformation (S'' o AF') (CF' o S')
TB': NaturalTransformation (CF' o T') (T'' o BF')
AF'':= (AF' o AF)%functor: Functor A A''
BF'':= (BF' o BF)%functor: Functor B B''
CF'':= (CF' o CF)%functor: Functor C C''
TA'':= (associator_2 CF' CF S o (CF' oL TA) o associator_1 CF' S' AF o (TA' oR AF)
 o associator_2 S'' AF' AF)%natural_transformation: NaturalTransformation (S'' o AF'') (CF'' o S)
TB'':= (associator_1 T'' BF' BF o (TB' oR BF) o associator_2 CF' T' BF o (CF' oL TB)
 o associator_1 CF' CF T)%natural_transformation: NaturalTransformation (CF'' o T) (T'' o BF'')
x: S / T
((functorial_morphism_of TA' TB' o functorial_morphism_of TA TB) _0 x)%object =
((functorial_morphism_of TA'' TB'') _0 x)%object
    Proof.
A, B, C: PreCategory
S: Functor A C
T: Functor B C
A', B', C': PreCategory
S': Functor A' C'
T': Functor B' C'
A'', B'', C'': PreCategory
S'': Functor A'' C''
T'': Functor B'' C''
AF: Functor A A'
BF: Functor B B'
CF: Functor C C'
TA: NaturalTransformation (S' o AF) (CF o S)
TB: NaturalTransformation (CF o T) (T' o BF)
AF': Functor A' A''
BF': Functor B' B''
CF': Functor C' C''
TA': NaturalTransformation (S'' o AF') (CF' o S')
TB': NaturalTransformation (CF' o T') (T'' o BF')
AF'':= (AF' o AF)%functor: Functor A A''
BF'':= (BF' o BF)%functor: Functor B B''
CF'':= (CF' o CF)%functor: Functor C C''
TA'':= (associator_2 CF' CF S o (CF' oL TA) o associator_1 CF' S' AF o (TA' oR AF)
 o associator_2 S'' AF' AF)%natural_transformation: NaturalTransformation (S'' o AF'') (CF'' o S)
TB'':= (associator_1 T'' BF' BF o (TB' oR BF) o associator_2 CF' T' BF o (CF' oL TB)
 o associator_1 CF' CF T)%natural_transformation: NaturalTransformation (CF'' o T) (T'' o BF'')
x: S / T
((functorial_morphism_of TA' TB' o functorial_morphism_of TA TB) _0 x)%object =
((functorial_morphism_of TA'' TB'') _0 x)%object
      let A := match goal with |- ?A = ?B => constr:(A) end in
      let B := match goal with |- ?A = ?B => constr:(B) end in
      refine (@CommaCategory.path_object' _ _ _ _ _ A B 1%path 1%path _).
A, B, C: PreCategory
S: Functor A C
T: Functor B C
A', B', C': PreCategory
S': Functor A' C'
T': Functor B' C'
A'', B'', C'': PreCategory
S'': Functor A'' C''
T'': Functor B'' C''
AF: Functor A A'
BF: Functor B B'
CF: Functor C C'
TA: NaturalTransformation (S' o AF) (CF o S)
TB: NaturalTransformation (CF o T) (T' o BF)
AF': Functor A' A''
BF': Functor B' B''
CF': Functor C' C''
TA': NaturalTransformation (S'' o AF') (CF' o S')
TB': NaturalTransformation (CF' o T') (T'' o BF')
AF'':= (AF' o AF)%functor: Functor A A''
BF'':= (BF' o BF)%functor: Functor B B''
CF'':= (CF' o CF)%functor: Functor C C''
TA'':= (associator_2 CF' CF S o (CF' oL TA) o associator_1 CF' S' AF o (TA' oR AF)
 o associator_2 S'' AF' AF)%natural_transformation: NaturalTransformation (S'' o AF'') (CF'' o S)
TB'':= (associator_1 T'' BF' BF o (TB' oR BF) o associator_2 CF' T' BF o (CF' oL TB)
 o associator_1 CF' CF T)%natural_transformation: NaturalTransformation (CF'' o T) (T'' o BF'')
x: S / T
transport
  (fun X : A'' =>
   morphism C'' (S'' _0 X)%object
     (T'' _0 (CommaCategory.b ((functorial_morphism_of TA'' TB'') _0 x)))%object)
  1
  (transport
     (fun Y : B'' =>
      morphism C''
        (S''
         _0 (CommaCategory.a
               ((functorial_morphism_of TA' TB'
                 o functorial_morphism_of TA TB)
                _0 x)))%object
        (T'' _0 Y)%object)
     1
     (CommaCategory.f
        ((functorial_morphism_of TA' TB' o functorial_morphism_of TA TB) _0 x)%object)) =
CommaCategory.f ((functorial_morphism_of TA'' TB'') _0 x)%object
      subst AF'' BF'' CF'' TA'' TB''.
A, B, C: PreCategory
S: Functor A C
T: Functor B C
A', B', C': PreCategory
S': Functor A' C'
T': Functor B' C'
A'', B'', C'': PreCategory
S'': Functor A'' C''
T'': Functor B'' C''
AF: Functor A A'
BF: Functor B B'
CF: Functor C C'
TA: NaturalTransformation (S' o AF) (CF o S)
TB: NaturalTransformation (CF o T) (T' o BF)
AF': Functor A' A''
BF': Functor B' B''
CF': Functor C' C''
TA': NaturalTransformation (S'' o AF') (CF' o S')
TB': NaturalTransformation (CF' o T') (T'' o BF')
x: S / T
transport
  (fun X : A'' =>
   morphism C'' (S'' _0 X)%object
     (T''
      _0 (CommaCategory.b
            ((functorial_morphism_of
                (associator_2 CF' CF S o (CF' oL TA) o associator_1 CF' S' AF
                 o (TA' oR AF) o associator_2 S'' AF' AF)
                (associator_1 T'' BF' BF o (TB' oR BF)
                 o associator_2 CF' T' BF o (CF' oL TB)
                 o associator_1 CF' CF T))
             _0 x)))%object)
  1
  (transport
     (fun Y : B'' =>
      morphism C''
        (S''
         _0 (CommaCategory.a
               ((functorial_morphism_of TA' TB'
                 o functorial_morphism_of TA TB)
                _0 x)))%object
        (T'' _0 Y)%object)
     1
     (CommaCategory.f
        ((functorial_morphism_of TA' TB' o functorial_morphism_of TA TB) _0 x)%object)) =
CommaCategory.f
  ((functorial_morphism_of
      (associator_2 CF' CF S o (CF' oL TA) o associator_1 CF' S' AF
       o (TA' oR AF) o associator_2 S'' AF' AF)
      (associator_1 T'' BF' BF o (TB' oR BF) o associator_2 CF' T' BF
       o (CF' oL TB) o associator_1 CF' CF T))
   _0 x)%object
      simpl in *.
A, B, C: PreCategory
S: Functor A C
T: Functor B C
A', B', C': PreCategory
S': Functor A' C'
T': Functor B' C'
A'', B'', C'': PreCategory
S'': Functor A'' C''
T'': Functor B'' C''
AF: Functor A A'
BF: Functor B B'
CF: Functor C C'
TA: NaturalTransformation (S' o AF) (CF o S)
TB: NaturalTransformation (CF o T) (T' o BF)
AF': Functor A' A''
BF': Functor B' B''
CF': Functor C' C''
TA': NaturalTransformation (S'' o AF') (CF' o S')
TB': NaturalTransformation (CF' o T') (T'' o BF')
x: CommaCategory.object S T
TB' (BF _0 (CommaCategory.b x))%object
o CF'
  _1 (TB (CommaCategory.b x) o CF _1 (CommaCategory.f x)
      o TA (CommaCategory.a x))
o TA' (AF _0 (CommaCategory.a x))%object =
1 o TB' (BF _0 (CommaCategory.b x))%object o 1
o CF' _1 (TB (CommaCategory.b x)) o 1 o CF' _1 (CF _1 (CommaCategory.f x))
o (1 o CF' _1 (TA (CommaCategory.a x)) o 1
   o TA' (AF _0 (CommaCategory.a x))%object o 1)
      abstract (
          autorewrite with morphism; simpl;
          helper (exact idpath) (commutes TA') (commutes TB')
        ).
    Defined.

    Definition functorial_composition_of `{Funext}
    : (functorial_morphism_of TA' TB' o functorial_morphism_of TA TB)%functor
      = functorial_morphism_of TA'' TB''.
A, B, C: PreCategory
S: Functor A C
T: Functor B C
A', B', C': PreCategory
S': Functor A' C'
T': Functor B' C'
A'', B'', C'': PreCategory
S'': Functor A'' C''
T'': Functor B'' C''
AF: Functor A A'
BF: Functor B B'
CF: Functor C C'
TA: NaturalTransformation (S' o AF) (CF o S)
TB: NaturalTransformation (CF o T) (T' o BF)
AF': Functor A' A''
BF': Functor B' B''
CF': Functor C' C''
TA': NaturalTransformation (S'' o AF') (CF' o S')
TB': NaturalTransformation (CF' o T') (T'' o BF')
AF'':= (AF' o AF)%functor: Functor A A''
BF'':= (BF' o BF)%functor: Functor B B''
CF'':= (CF' o CF)%functor: Functor C C''
TA'':= (associator_2 CF' CF S o (CF' oL TA) o associator_1 CF' S' AF o (TA' oR AF)
 o associator_2 S'' AF' AF)%natural_transformation: NaturalTransformation (S'' o AF'') (CF'' o S)
TB'':= (associator_1 T'' BF' BF o (TB' oR BF) o associator_2 CF' T' BF o (CF' oL TB)
 o associator_1 CF' CF T)%natural_transformation: NaturalTransformation (CF'' o T) (T'' o BF'')
H: Funext
(functorial_morphism_of TA' TB' o functorial_morphism_of TA TB)%functor =
functorial_morphism_of TA'' TB''
    Proof.
A, B, C: PreCategory
S: Functor A C
T: Functor B C
A', B', C': PreCategory
S': Functor A' C'
T': Functor B' C'
A'', B'', C'': PreCategory
S'': Functor A'' C''
T'': Functor B'' C''
AF: Functor A A'
BF: Functor B B'
CF: Functor C C'
TA: NaturalTransformation (S' o AF) (CF o S)
TB: NaturalTransformation (CF o T) (T' o BF)
AF': Functor A' A''
BF': Functor B' B''
CF': Functor C' C''
TA': NaturalTransformation (S'' o AF') (CF' o S')
TB': NaturalTransformation (CF' o T') (T'' o BF')
AF'':= (AF' o AF)%functor: Functor A A''
BF'':= (BF' o BF)%functor: Functor B B''
CF'':= (CF' o CF)%functor: Functor C C''
TA'':= (associator_2 CF' CF S o (CF' oL TA) o associator_1 CF' S' AF o (TA' oR AF)
 o associator_2 S'' AF' AF)%natural_transformation: NaturalTransformation (S'' o AF'') (CF'' o S)
TB'':= (associator_1 T'' BF' BF o (TB' oR BF) o associator_2 CF' T' BF o (CF' oL TB)
 o associator_1 CF' CF T)%natural_transformation: NaturalTransformation (CF'' o T) (T'' o BF'')
H: Funext
(functorial_morphism_of TA' TB' o functorial_morphism_of TA TB)%functor =
functorial_morphism_of TA'' TB''
      path_functor; simpl.
A, B, C: PreCategory
S: Functor A C
T: Functor B C
A', B', C': PreCategory
S': Functor A' C'
T': Functor B' C'
A'', B'', C'': PreCategory
S'': Functor A'' C''
T'': Functor B'' C''
AF: Functor A A'
BF: Functor B B'
CF: Functor C C'
TA: NaturalTransformation (S' o AF) (CF o S)
TB: NaturalTransformation (CF o T) (T' o BF)
AF': Functor A' A''
BF': Functor B' B''
CF': Functor C' C''
TA': NaturalTransformation (S'' o AF') (CF' o S')
TB': NaturalTransformation (CF' o T') (T'' o BF')
AF'':= (AF' o AF)%functor: Functor A A''
BF'':= (BF' o BF)%functor: Functor B B''
CF'':= (CF' o CF)%functor: Functor C C''
TA'':= (associator_2 CF' CF S o (CF' oL TA) o associator_1 CF' S' AF o (TA' oR AF)
 o associator_2 S'' AF' AF)%natural_transformation: NaturalTransformation (S'' o AF'') (CF'' o S)
TB'':= (associator_1 T'' BF' BF o (TB' oR BF) o associator_2 CF' T' BF o (CF' oL TB)
 o associator_1 CF' CF T)%natural_transformation: NaturalTransformation (CF'' o T) (T'' o BF'')
H: Funext
{HO
: (fun c : CommaCategory.object S T =>
   functorial_morphism_of_object_of TA' TB'
     (functorial_morphism_of_object_of TA TB c)) =
  functorial_morphism_of_object_of TA'' TB''
&
transport
  (fun GO : CommaCategory.object S T -> CommaCategory.object S'' T'' =>
   forall s d : CommaCategory.object S T,
   CommaCategory.morphism s d -> CommaCategory.morphism (GO s) (GO d))
  HO
  (fun (s d : CommaCategory.object S T) (m : CommaCategory.morphism s d) =>
   functorial_morphism_of_morphism_of TA' TB'
     (functorial_morphism_of_morphism_of TA TB m)) =
functorial_morphism_of_morphism_of TA'' TB''}
      exists (path_forall _ _ functorial_composition_of_helper).
A, B, C: PreCategory
S: Functor A C
T: Functor B C
A', B', C': PreCategory
S': Functor A' C'
T': Functor B' C'
A'', B'', C'': PreCategory
S'': Functor A'' C''
T'': Functor B'' C''
AF: Functor A A'
BF: Functor B B'
CF: Functor C C'
TA: NaturalTransformation (S' o AF) (CF o S)
TB: NaturalTransformation (CF o T) (T' o BF)
AF': Functor A' A''
BF': Functor B' B''
CF': Functor C' C''
TA': NaturalTransformation (S'' o AF') (CF' o S')
TB': NaturalTransformation (CF' o T') (T'' o BF')
AF'':= (AF' o AF)%functor: Functor A A''
BF'':= (BF' o BF)%functor: Functor B B''
CF'':= (CF' o CF)%functor: Functor C C''
TA'':= (associator_2 CF' CF S o (CF' oL TA) o associator_1 CF' S' AF o (TA' oR AF)
 o associator_2 S'' AF' AF)%natural_transformation: NaturalTransformation (S'' o AF'') (CF'' o S)
TB'':= (associator_1 T'' BF' BF o (TB' oR BF) o associator_2 CF' T' BF o (CF' oL TB)
 o associator_1 CF' CF T)%natural_transformation: NaturalTransformation (CF'' o T) (T'' o BF'')
H: Funext
transport
  (fun GO : CommaCategory.object S T -> CommaCategory.object S'' T'' =>
   forall s d : CommaCategory.object S T,
   CommaCategory.morphism s d -> CommaCategory.morphism (GO s) (GO d))
  (path_forall
     (functorial_morphism_of TA' TB' o functorial_morphism_of TA TB)%functor
     (functorial_morphism_of TA'' TB'') functorial_composition_of_helper)
  (fun (s d : CommaCategory.object S T) (m : CommaCategory.morphism s d) =>
   functorial_morphism_of_morphism_of TA' TB'
     (functorial_morphism_of_morphism_of TA TB m)) =
functorial_morphism_of_morphism_of TA'' TB''
      functorial_helper_t functorial_composition_of_helper.
    Qed.
  End composition_of.
End functorial.