(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(*****************************************************************************)
(*          Projet Coq - Calculus of Inductive Constructions V5.10           *)
(*****************************************************************************)
(*                                                                           *)
(*          InterChange Law                                                  *)
(*                                                                           *)
(*          Ge'rard Huet and Amokrane Saibi,  June 1994                      *)
(*                                                                           *)
(*****************************************************************************)

Require Export CatFunct. 

Set Implicit Arguments.
Unset Strict Implicit.

Section horz_comp.

Variables (A B C : Category) (F G : Functor A B) (F' G' : Functor B C)
  (T : NT F G) (T' : NT F' G').

Definition Ast (a : A) : (F o_F F') a --> (G o_F G') a :=
  T' (F a) o FMor G' (T a).

Lemma Ast_eq :
 forall a : A, FMor F' (T a) o T' (G a) =_S T' (F a) o FMor G' (T a).
Proof.
(* Goal: forall a : Ob A, @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) *)
intro a; apply NatCond.
Qed.

Lemma Ast_nt_law : NT_law Ast.
Proof.
(* Goal: @NT_law A C (@Comp_Functor A B C F F') (@Comp_Functor A B C G G') Ast *)
unfold NT_law, Ast, Comp_Functor in |- *.
(* Goal: forall (a b : Ob A) (f : Carrier (@Hom A a b)), @Equal (@Hom C (@FOb A C (@Build_Functor A C (@Comp_FOb A B C F F') (@Comp_FMap A B C F F') (@Comp_Functor_comp_law A B C F F') (@Comp_Functor_id_law A B C F F')) a) (@FOb A C (@Build_Functor A C (@Comp_FOb A B C G G') (@Comp_FMap A B C G G') (@Comp_Functor_comp_law A B C G G') (@Comp_Functor_id_law A B C G G')) b)) (@Comp C (@FOb A C (@Build_Functor A C (@Comp_FOb A B C F F') (@Comp_FMap A B C F F') (@Comp_Functor_comp_law A B C F F') (@Comp_Functor_id_law A B C F F')) a) (@FOb A C (@Build_Functor A C (@Comp_FOb A B C F F') (@Comp_FMap A B C F F') (@Comp_Functor_comp_law A B C F F') (@Comp_Functor_id_law A B C F F')) b) (@FOb A C (@Build_Functor A C (@Comp_FOb A B C G G') (@Comp_FMap A B C G G') (@Comp_Functor_comp_law A B C G G') (@Comp_Functor_id_law A B C G G')) b) (@FMor A C (@Build_Functor A C (@Comp_FOb A B C F F') (@Comp_FMap A B C F F') (@Comp_Functor_comp_law A B C F F') (@Comp_Functor_id_law A B C F F')) a b f) (@Comp C (@FOb B C F' (@FOb A B F b)) (@FOb B C G' (@FOb A B F b)) (@FOb B C G' (@FOb A B G b)) (@ApNT B C F' G' T' (@FOb A B F b)) (@FMor B C G' (@FOb A B F b) (@FOb A B G b) (@ApNT A B F G T b)))) (@Comp C (@FOb A C (@Build_Functor A C (@Comp_FOb A B C F F') (@Comp_FMap A B C F F') (@Comp_Functor_comp_law A B C F F') (@Comp_Functor_id_law A B C F F')) a) (@FOb A C (@Build_Functor A C (@Comp_FOb A B C G G') (@Comp_FMap A B C G G') (@Comp_Functor_comp_law A B C G G') (@Comp_Functor_id_law A B C G G')) a) (@FOb A C (@Build_Functor A C (@Comp_FOb A B C G G') (@Comp_FMap A B C G G') (@Comp_Functor_comp_law A B C G G') (@Comp_Functor_id_law A B C G G')) b) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor A C (@Build_Functor A C (@Comp_FOb A B C G G') (@Comp_FMap A B C G G') (@Comp_Functor_comp_law A B C G G') (@Comp_Functor_id_law A B C G G')) a b f)) *)
unfold FMor at 1 in |- *; simpl in |- *.
(* Goal: forall (a b : Ob A) (f : Carrier (@Hom A a b)), @Equal (@Hom C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' b)) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C F F' b) (@Comp_FOb A B C G G' b) (@Comp_FMor A B C F F' a b f) (@Comp C (@FOb B C F' (@FOb A B F b)) (@FOb B C G' (@FOb A B F b)) (@FOb B C G' (@FOb A B G b)) (@ApNT B C F' G' T' (@FOb A B F b)) (@FMor B C G' (@FOb A B F b) (@FOb A B G b) (@ApNT A B F G T b)))) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' a) (@Comp_FOb A B C G G' b) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor A C (@Build_Functor A C (@Comp_FOb A B C G G') (@Comp_FMap A B C G G') (@Comp_Functor_comp_law A B C G G') (@Comp_Functor_id_law A B C G G')) a b f)) *)
unfold FMor at 3 in |- *; simpl in |- *.
(* Goal: forall a : Ob A, @Equal_hom D (@FOb C D F'' (@Comp_FOb A B C F F' a)) (@FOb C D G'' (@Comp_FOb A B C G G' a)) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@ApNT C D F'' G'' T'' (@FOb B C F' (@FOb A B F a))) (@FMor C D G'' (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))))) (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@ApNT C D F'' G'' T'' (@FOb B C F' (@FOb A B F a))) (@FMor C D G'' (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)))) (@Comp_FMor B C D G' G'' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) *)
unfold Comp_FMor in |- *.
(* Goal: forall (a b : Ob A) (f : Carrier (@Hom A a b)), @Equal (@Hom C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' b)) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C F F' b) (@Comp_FOb A B C G G' b) (@FMor B C F' (@FOb A B F a) (@FOb A B F b) (@FMor A B F a b f)) (@Comp C (@FOb B C F' (@FOb A B F b)) (@FOb B C G' (@FOb A B F b)) (@FOb B C G' (@FOb A B G b)) (@ApNT B C F' G' T' (@FOb A B F b)) (@FMor B C G' (@FOb A B F b) (@FOb A B G b) (@ApNT A B F G T b)))) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' a) (@Comp_FOb A B C G G' b) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
intros a b f.
(* Goal: @Equal (@Hom C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' b)) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C F F' b) (@Comp_FOb A B C G G' b) (@FMor B C F' (@FOb A B F a) (@FOb A B F b) (@FMor A B F a b f)) (@Comp C (@FOb B C F' (@FOb A B F b)) (@FOb B C G' (@FOb A B F b)) (@FOb B C G' (@FOb A B G b)) (@ApNT B C F' G' T' (@FOb A B F b)) (@FMor B C G' (@FOb A B F b) (@FOb A B G b) (@ApNT A B F G T b)))) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' a) (@Comp_FOb A B C G G' b) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* *) apply Trans with ((FMor F' (T a) o T' (G a)) o FMor G' (FMor G f)).
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C F F' b) (@Comp_FOb A B C G G' b) (@FMor B C F' (@FOb A B F a) (@FOb A B F b) (@FMor A B F a b f)) (@Comp C (@FOb B C F' (@FOb A B F b)) (@FOb B C G' (@FOb A B F b)) (@FOb B C G' (@FOb A B G b)) (@ApNT B C F' G' T' (@FOb A B F b)) (@FMor B C G' (@FOb A B F b) (@FOb A B G b) (@ApNT A B F G T b)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' a) (@Comp_FOb A B C G G' b) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* *) apply Trans with (FMor F' (FMor F f) o FMor F' (T b) o T' (G b)).
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C F F' b) (@Comp_FOb A B C G G' b) (@FMor B C F' (@FOb A B F a) (@FOb A B F b) (@FMor A B F a b f)) (@Comp C (@FOb B C F' (@FOb A B F b)) (@FOb B C G' (@FOb A B F b)) (@FOb B C G' (@FOb A B G b)) (@ApNT B C F' G' T' (@FOb A B F b)) (@FMor B C G' (@FOb A B F b) (@FOb A B G b) (@ApNT A B F G T b)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B F b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B F b) (@FMor A B F a b f)) (@Comp C (@FOb B C F' (@FOb A B F b)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F b) (@FOb A B G b) (@ApNT A B F G T b)) (@ApNT B C F' G' T' (@FOb A B G b)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B F b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B F b) (@FMor A B F a b f)) (@Comp C (@FOb B C F' (@FOb A B F b)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F b) (@FOb A B G b) (@ApNT A B F G T b)) (@ApNT B C F' G' T' (@FOb A B G b)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' a) (@Comp_FOb A B C G G' b) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
apply Comp_l; apply Sym; apply (Ast_eq b).
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B F b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B F b) (@FMor A B F a b f)) (@Comp C (@FOb B C F' (@FOb A B F b)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F b) (@FOb A B G b) (@ApNT A B F G T b)) (@ApNT B C F' G' T' (@FOb A B G b)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' a) (@Comp_FOb A B C G G' b) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* *) apply Trans with (FMor F' (T a) o FMor F' (FMor G f) o T' (G b)).
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B F b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B F b) (@FMor A B F a b f)) (@Comp C (@FOb B C F' (@FOb A B F b)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F b) (@FOb A B G b) (@ApNT A B F G T b)) (@ApNT B C F' G' T' (@FOb A B G b)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f)) (@ApNT B C F' G' T' (@FOb A B G b)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f)) (@ApNT B C F' G' T' (@FOb A B G b)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' a) (@Comp_FOb A B C G G' b) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* *) apply Trans with ((FMor F' (FMor F f) o FMor F' (T b)) o T' (G b)).
(* Goal: @Equal (@Hom D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a)))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@ApNT C D F'' G'' T'' (@FOb B C F' (@FOb A B F a))) (@Comp D (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@FMor C D G'' (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a))) (@FMor C D G'' (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@ApNT C D F'' G'' T'' (@FOb B C F' (@FOb A B F a))) (@FMor C D G'' (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)))) (@FMor C D G'' (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)))) *)
apply Ass.
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B F b)) (@FOb B C F' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B F b) (@FMor A B F a b f)) (@FMor B C F' (@FOb A B F b) (@FOb A B G b) (@ApNT A B F G T b))) (@ApNT B C F' G' T' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f)) (@ApNT B C F' G' T' (@FOb A B G b)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f)) (@ApNT B C F' G' T' (@FOb A B G b)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' a) (@Comp_FOb A B C G G' b) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* *) apply Trans with ((FMor F' (T a) o FMor F' (FMor G f)) o T' (G b)).
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' a) (@Comp_FOb A B C G G' b) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
apply Comp_r.
(* commutation du diagramme de gauche par fonctorialite' de F'
   et Naturalite' de T (p.18) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B F b)) (@FOb B C F' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B F b) (@FMor A B F a b f)) (@FMor B C F' (@FOb A B F b) (@FOb A B G b) (@ApNT A B F G T b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) (@ApNT B C F' G' T' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f)) (@ApNT B C F' G' T' (@FOb A B G b)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f)) (@ApNT B C F' G' T' (@FOb A B G b)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' a) (@Comp_FOb A B C G G' b) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* *) apply Trans with (FMor F' (FMor F f o T b)).
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B F b)) (@FOb B C F' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B F b) (@FMor A B F a b f)) (@FMor B C F' (@FOb A B F b) (@FOb A B G b) (@ApNT A B F G T b))) (@FMor B C F' (@FOb A B F a) (@FOb A B G b) (@Comp B (@FOb A B F a) (@FOb A B F b) (@FOb A B G b) (@FMor A B F a b f) (@ApNT A B F G T b))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G b))) (@FMor B C F' (@FOb A B F a) (@FOb A B G b) (@Comp B (@FOb A B F a) (@FOb A B F b) (@FOb A B G b) (@FMor A B F a b f) (@ApNT A B F G T b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) (@ApNT B C F' G' T' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f)) (@ApNT B C F' G' T' (@FOb A B G b)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f)) (@ApNT B C F' G' T' (@FOb A B G b)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' a) (@Comp_FOb A B C G G' b) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
apply FComp1.
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G b))) (@FMor B C F' (@FOb A B F a) (@FOb A B G b) (@Comp B (@FOb A B F a) (@FOb A B F b) (@FOb A B G b) (@FMor A B F a b f) (@ApNT A B F G T b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) (@ApNT B C F' G' T' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f)) (@ApNT B C F' G' T' (@FOb A B G b)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f)) (@ApNT B C F' G' T' (@FOb A B G b)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' a) (@Comp_FOb A B C G G' b) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* *) apply Trans with (FMor F' (T a o FMor G f)).
(* Fonctorialite' de F' *)
(* T Naturelle *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G b))) (@FMor B C F' (@FOb A B F a) (@FOb A B G b) (@Comp B (@FOb A B F a) (@FOb A B F b) (@FOb A B G b) (@FMor A B F a b f) (@ApNT A B F G T b))) (@FMor B C F' (@FOb A B F a) (@FOb A B G b) (@Comp B (@FOb A B F a) (@FOb A B G a) (@FOb A B G b) (@ApNT A B F G T a) (@FMor A B G a b f))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G b))) (@FMor B C F' (@FOb A B F a) (@FOb A B G b) (@Comp B (@FOb A B F a) (@FOb A B G a) (@FOb A B G b) (@ApNT A B F G T a) (@FMor A B G a b f))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) (@ApNT B C F' G' T' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f)) (@ApNT B C F' G' T' (@FOb A B G b)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f)) (@ApNT B C F' G' T' (@FOb A B G b)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' a) (@Comp_FOb A B C G G' b) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
apply FPres; apply NatCond.
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G b))) (@FMor B C F' (@FOb A B F a) (@FOb A B G b) (@Comp B (@FOb A B F a) (@FOb A B G a) (@FOb A B G b) (@ApNT A B F G T a) (@FMor A B G a b f))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) (@ApNT B C F' G' T' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f)) (@ApNT B C F' G' T' (@FOb A B G b)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f)) (@ApNT B C F' G' T' (@FOb A B G b)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' a) (@Comp_FOb A B C G G' b) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
apply FComp.
(* Goal: @Equal (@Hom C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@ApNT B C G' H' U' (@FOb A B F a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a))) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C G' H' U' (@FOb A B F a)) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C G' H' U' (@FOb A B F a)) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a))))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@FMor B C H' (@FOb A B F a) (@FOb A B H a) (@Comp B (@FOb A B F a) (@FOb A B G a) (@FOb A B H a) (@ApNT A B F G T a) (@ApNT A B G H U a)))) *)
apply Ass1.
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f)) (@ApNT B C F' G' T' (@FOb A B G b)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' a) (@Comp_FOb A B C G G' b) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* *) apply Trans with (FMor F' (T a) o T' (G a) o FMor G' (FMor G f)).
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f)) (@ApNT B C F' G' T' (@FOb A B G b)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@ApNT B C F' G' T' (@FOb A B G a)) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@ApNT B C F' G' T' (@FOb A B G a)) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' a) (@Comp_FOb A B C G G' b) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
apply Comp_l; apply NatCond.
(* Goal: @Equal (@Hom D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a)))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@ApNT C D F'' G'' T'' (@FOb B C F' (@FOb A B F a))) (@Comp D (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@FMor C D G'' (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a))) (@FMor C D G'' (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@ApNT C D F'' G'' T'' (@FOb B C F' (@FOb A B F a))) (@FMor C D G'' (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)))) (@FMor C D G'' (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)))) *)
apply Ass.
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' a) (@Comp_FOb A B C G G' b) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
apply Comp_r.
(* Goal: @Equal (@Hom C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) *)
apply (Ast_eq a).
Qed.

Canonical Structure CompH_NT := Build_NT Ast_nt_law.

End horz_comp.

Infix "o_NTh" := CompH_NT (at level 20, right associativity).

Section interchangelaw.

Variables (A B C : Category) (F G H : Functor A B) (F' G' H' : Functor B C).
Variables (T : NT F G) (T' : NT F' G') (U : NT G H) (U' : NT G' H').

Lemma InterChange_law :
 (T o_NTh T') o_NTv U o_NTh U' =_NT (T o_NTv U) o_NTh T' o_NTv U'.
Proof.
(* Goal: @Equal_NT A C (@Comp_Functor A B C F F') (@Comp_Functor A B C H H') (@CompV_NT A C (@Comp_Functor A B C F F') (@Comp_Functor A B C G G') (@Comp_Functor A B C H H') (@CompH_NT A B C F G F' G' T T') (@CompH_NT A B C G H G' H' U U')) (@CompH_NT A B C F H F' H' (@CompV_NT A B F G H T U) (@CompV_NT B C F' G' H' T' U')) *)
unfold Equal_NT in |- *; intro a; simpl in |- *.
(* Goal: @Equal (@Hom C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C H H' a)) (@Comp_tau A C (@Comp_Functor A B C F F') (@Comp_Functor A B C G G') (@Comp_Functor A B C H H') (@CompH_NT A B C F G F' G' T T') (@CompH_NT A B C G H G' H' U U') a) (@Ast A B C F H F' H' (@CompV_NT A B F G H T U) (@CompV_NT B C F' G' H' T' U') a) *)
unfold CompH_NT, Comp_Functor in |- *; simpl in |- *.
(* Goal: @Equal (@Hom C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C H H' a)) (@Comp_tau A C (@Build_Functor A C (@Comp_FOb A B C F F') (@Comp_FMap A B C F F') (@Comp_Functor_comp_law A B C F F') (@Comp_Functor_id_law A B C F F')) (@Build_Functor A C (@Comp_FOb A B C G G') (@Comp_FMap A B C G G') (@Comp_Functor_comp_law A B C G G') (@Comp_Functor_id_law A B C G G')) (@Build_Functor A C (@Comp_FOb A B C H H') (@Comp_FMap A B C H H') (@Comp_Functor_comp_law A B C H H') (@Comp_Functor_id_law A B C H H')) (@Build_NT A C (@Build_Functor A C (@Comp_FOb A B C F F') (@Comp_FMap A B C F F') (@Comp_Functor_comp_law A B C F F') (@Comp_Functor_id_law A B C F F')) (@Build_Functor A C (@Comp_FOb A B C G G') (@Comp_FMap A B C G G') (@Comp_Functor_comp_law A B C G G') (@Comp_Functor_id_law A B C G G')) (@Ast A B C F G F' G' T T') (@Ast_nt_law A B C F G F' G' T T')) (@Build_NT A C (@Build_Functor A C (@Comp_FOb A B C G G') (@Comp_FMap A B C G G') (@Comp_Functor_comp_law A B C G G') (@Comp_Functor_id_law A B C G G')) (@Build_Functor A C (@Comp_FOb A B C H H') (@Comp_FMap A B C H H') (@Comp_Functor_comp_law A B C H H') (@Comp_Functor_id_law A B C H H')) (@Ast A B C G H G' H' U U') (@Ast_nt_law A B C G H G' H' U U')) a) (@Ast A B C F H F' H' (@CompV_NT A B F G H T U) (@CompV_NT B C F' G' H' T' U') a) *)
unfold Ast, Comp_tau in |- *; simpl in |- *.
(* Goal: @Equal (@Hom C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C H H' a)) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' a) (@Comp_FOb A B C H H' a) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@Comp C (@FOb B C G' (@FOb A B G a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C G' H' U' (@FOb A B G a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp_tau B C F' G' H' T' U' (@FOb A B F a)) (@FMor B C H' (@FOb A B F a) (@FOb A B H a) (@Comp_tau A B F G H T U a))) *)
unfold Comp_tau in |- *.
(* *) apply
       Trans with ((T' (F a) o U' (F a)) o FMor H' (T a) o FMor H' (U a)).
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' a) (@Comp_FOb A B C H H' a) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@Comp C (@FOb B C G' (@FOb A B G a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C G' H' U' (@FOb A B G a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@FMor B C H' (@FOb A B F a) (@FOb A B H a) (@Comp B (@FOb A B F a) (@FOb A B G a) (@FOb A B H a) (@ApNT A B F G T a) (@ApNT A B G H U a)))) *)
(* *) apply Trans with (T' (F a) o FMor G' (T a) o U' (G a) o FMor H' (U a)).
(* Goal: @Equal (@Hom C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@ApNT B C G' H' U' (@FOb A B F a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a))) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C G' H' U' (@FOb A B F a)) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C G' H' U' (@FOb A B F a)) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a))))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@FMor B C H' (@FOb A B F a) (@FOb A B H a) (@Comp B (@FOb A B F a) (@FOb A B G a) (@FOb A B H a) (@ApNT A B F G T a) (@ApNT A B G H U a)))) *)
apply Ass1.
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C G' (@FOb A B G a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C G' H' U' (@FOb A B G a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a))))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@FMor B C H' (@FOb A B F a) (@FOb A B H a) (@Comp B (@FOb A B F a) (@FOb A B G a) (@FOb A B H a) (@ApNT A B F G T a) (@ApNT A B G H U a)))) *)
(* *) apply Trans with (T' (F a) o U' (F a) o FMor H' (T a) o FMor H' (U a)).
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C G' (@FOb A B G a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C G' H' U' (@FOb A B G a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a))))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C G' H' U' (@FOb A B F a)) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a))))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C G' H' U' (@FOb A B F a)) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a))))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@FMor B C H' (@FOb A B F a) (@FOb A B H a) (@Comp B (@FOb A B F a) (@FOb A B G a) (@FOb A B H a) (@ApNT A B F G T a) (@ApNT A B G H U a)))) *)
apply Comp_l.
(* Goal: @Equal (@Hom C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C G' (@FOb A B G a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C G' H' U' (@FOb A B G a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C G' H' U' (@FOb A B F a)) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C G' H' U' (@FOb A B F a)) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a))))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@FMor B C H' (@FOb A B F a) (@FOb A B H a) (@Comp B (@FOb A B F a) (@FOb A B G a) (@FOb A B H a) (@ApNT A B F G T a) (@ApNT A B G H U a)))) *)
(* *) apply Trans with ((FMor G' (T a) o U' (G a)) o FMor H' (U a)).
(* Goal: @Equal (@Hom D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a)))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@ApNT C D F'' G'' T'' (@FOb B C F' (@FOb A B F a))) (@Comp D (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@FMor C D G'' (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a))) (@FMor C D G'' (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@ApNT C D F'' G'' T'' (@FOb B C F' (@FOb A B F a))) (@FMor C D G'' (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)))) (@FMor C D G'' (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)))) *)
apply Ass.
(* Goal: @Equal (@Hom C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C H' (@FOb A B G a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C G' H' U' (@FOb A B G a))) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a))) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C G' H' U' (@FOb A B F a)) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C G' H' U' (@FOb A B F a)) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a))))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@FMor B C H' (@FOb A B F a) (@FOb A B H a) (@Comp B (@FOb A B F a) (@FOb A B G a) (@FOb A B H a) (@ApNT A B F G T a) (@ApNT A B G H U a)))) *)
(* *) apply Trans with ((U' (F a) o FMor H' (T a)) o FMor H' (U a)).
(* Goal: @Equal (@Hom C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C H' (@FOb A B G a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C G' H' U' (@FOb A B G a))) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a))) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@ApNT B C G' H' U' (@FOb A B F a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a))) *)
(* Goal: @Equal (@Hom C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@ApNT B C G' H' U' (@FOb A B F a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a))) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C G' H' U' (@FOb A B F a)) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C G' H' U' (@FOb A B F a)) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a))))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@FMor B C H' (@FOb A B F a) (@FOb A B H a) (@Comp B (@FOb A B F a) (@FOb A B G a) (@FOb A B H a) (@ApNT A B F G T a) (@ApNT A B G H U a)))) *)
apply Comp_r; apply NatCond.
(* Goal: @Equal (@Hom C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@ApNT B C G' H' U' (@FOb A B F a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a))) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C G' H' U' (@FOb A B F a)) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@Comp C (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@ApNT B C G' H' U' (@FOb A B F a)) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a))))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@Comp C (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B G a)) (@FOb B C H' (@FOb A B H a)) (@FMor B C H' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C H' (@FOb A B G a) (@FOb A B H a) (@ApNT A B G H U a)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@FOb B C H' (@FOb A B H a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C H' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@ApNT B C G' H' U' (@FOb A B F a))) (@FMor B C H' (@FOb A B F a) (@FOb A B H a) (@Comp B (@FOb A B F a) (@FOb A B G a) (@FOb A B H a) (@ApNT A B F G T a) (@ApNT A B G H U a)))) *)
apply Ass1.
(* Goal: @Equal (@Hom D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a)))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@ApNT C D F'' G'' T'' (@FOb B C F' (@FOb A B F a))) (@Comp D (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@FMor C D G'' (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a))) (@FMor C D G'' (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@ApNT C D F'' G'' T'' (@FOb B C F' (@FOb A B F a))) (@FMor C D G'' (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)))) (@FMor C D G'' (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)))) *)
apply Ass.
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B F b)) (@FOb B C F' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B F b) (@FMor A B F a b f)) (@FMor B C F' (@FOb A B F b) (@FOb A B G b) (@ApNT A B F G T b))) (@FMor B C F' (@FOb A B F a) (@FOb A B G b) (@Comp B (@FOb A B F a) (@FOb A B F b) (@FOb A B G b) (@FMor A B F a b f) (@ApNT A B F G T b))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G b))) (@FMor B C F' (@FOb A B F a) (@FOb A B G b) (@Comp B (@FOb A B F a) (@FOb A B F b) (@FOb A B G b) (@FMor A B F a b f) (@ApNT A B F G T b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) (@ApNT B C F' G' T' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f)) (@ApNT B C F' G' T' (@FOb A B G b)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f)) (@ApNT B C F' G' T' (@FOb A B G b)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' a) (@Comp_FOb A B C G G' b) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
apply Comp_l; apply FComp1.
Qed.
                                           
End interchangelaw.


(* o_NTh is associative *)

Definition EqualH_NT (C D : Category) (F G F' G' : Functor C D) 
  (T : NT F G) (T' : NT F' G') := forall a : C, T a =_H T' a.

Infix "=_NTH" := EqualH_NT (at level 70).

Section assoc_horz_comp.

Variables (A B C D : Category) (F G : Functor A B) 
  (F' G' : Functor B C) (F'' G'' : Functor C D).
Variables (T : NT F G) (T' : NT F' G') (T'' : NT F'' G'').

Lemma CompH_NT_assoc : (T o_NTh T') o_NTh T'' =_NTH T o_NTh T' o_NTh T''.
Proof.
(* Goal: @EqualH_NT A D (@Comp_Functor A C D (@Comp_Functor A B C F F') F'') (@Comp_Functor A C D (@Comp_Functor A B C G G') G'') (@Comp_Functor A B D F (@Comp_Functor B C D F' F'')) (@Comp_Functor A B D G (@Comp_Functor B C D G' G'')) (@CompH_NT A C D (@Comp_Functor A B C F F') (@Comp_Functor A B C G G') F'' G'' (@CompH_NT A B C F G F' G' T T') T'') (@CompH_NT A B D F G (@Comp_Functor B C D F' F'') (@Comp_Functor B C D G' G'') T (@CompH_NT B C D F' G' F'' G'' T' T'')) *)
unfold EqualH_NT, CompH_NT in |- *; simpl in |- *.
(* Goal: forall a : Ob A, @Equal_hom D (@Comp_FOb A C D (@Comp_Functor A B C F F') F'' a) (@Comp_FOb A C D (@Comp_Functor A B C G G') G'' a) (@Ast A C D (@Comp_Functor A B C F F') (@Comp_Functor A B C G G') F'' G'' (@Build_NT A C (@Comp_Functor A B C F F') (@Comp_Functor A B C G G') (@Ast A B C F G F' G' T T') (@Ast_nt_law A B C F G F' G' T T')) T'' a) (@Comp_FOb B C D F' F'' (@FOb A B F a)) (@Comp_FOb B C D G' G'' (@FOb A B G a)) (@Ast A B D F G (@Comp_Functor B C D F' F'') (@Comp_Functor B C D G' G'') T (@Build_NT B D (@Comp_Functor B C D F' F'') (@Comp_Functor B C D G' G'') (@Ast B C D F' G' F'' G'' T' T'') (@Ast_nt_law B C D F' G' F'' G'' T' T'')) a) *)
unfold Ast in |- *; simpl in |- *.
(* Goal: forall a : Ob A, @Equal_hom D (@Comp_FOb A C D (@Comp_Functor A B C F F') F'' a) (@Comp_FOb A C D (@Comp_Functor A B C G G') G'' a) (@Comp D (@FOb C D F'' (@Comp_FOb A B C F F' a)) (@FOb C D G'' (@Comp_FOb A B C F F' a)) (@FOb C D G'' (@Comp_FOb A B C G G' a)) (@ApNT C D F'' G'' T'' (@Comp_FOb A B C F F' a)) (@FMor C D G'' (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' a) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))))) (@Comp_FOb B C D F' F'' (@FOb A B F a)) (@Comp_FOb B C D G' G'' (@FOb A B G a)) (@Comp D (@Comp_FOb B C D F' F'' (@FOb A B F a)) (@Comp_FOb B C D G' G'' (@FOb A B F a)) (@Comp_FOb B C D G' G'' (@FOb A B G a)) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@ApNT C D F'' G'' T'' (@FOb B C F' (@FOb A B F a))) (@FMor C D G'' (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)))) (@FMor B D (@Comp_Functor B C D G' G'') (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) *)
unfold Comp_FOb in |- *.
(* Goal: forall a : Ob A, @Equal_hom D (@FOb C D F'' (@FOb A C (@Comp_Functor A B C F F') a)) (@FOb C D G'' (@FOb A C (@Comp_Functor A B C G G') a)) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@ApNT C D F'' G'' T'' (@FOb B C F' (@FOb A B F a))) (@FMor C D G'' (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))))) (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@ApNT C D F'' G'' T'' (@FOb B C F' (@FOb A B F a))) (@FMor C D G'' (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)))) (@FMor B D (@Comp_Functor B C D G' G'') (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) *)
unfold FMor at 4 in |- *; simpl in |- *.
(* Goal: forall a : Ob A, @Equal_hom D (@FOb C D F'' (@Comp_FOb A B C F F' a)) (@FOb C D G'' (@Comp_FOb A B C G G' a)) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@ApNT C D F'' G'' T'' (@FOb B C F' (@FOb A B F a))) (@FMor C D G'' (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))))) (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@ApNT C D F'' G'' T'' (@FOb B C F' (@FOb A B F a))) (@FMor C D G'' (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)))) (@Comp_FMor B C D G' G'' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) *)
unfold Comp_FMor in |- *.
(* Goal: forall a : Ob A, @Equal_hom D (@FOb C D F'' (@Comp_FOb A B C F F' a)) (@FOb C D G'' (@Comp_FOb A B C G G' a)) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@ApNT C D F'' G'' T'' (@FOb B C F' (@FOb A B F a))) (@FMor C D G'' (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))))) (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@ApNT C D F'' G'' T'' (@FOb B C F' (@FOb A B F a))) (@FMor C D G'' (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)))) (@FMor C D G'' (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)))) *)
intro a.
(* Goal: @Equal_hom D (@FOb C D F'' (@Comp_FOb A B C F F' a)) (@FOb C D G'' (@Comp_FOb A B C G G' a)) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@ApNT C D F'' G'' T'' (@FOb B C F' (@FOb A B F a))) (@FMor C D G'' (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))))) (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@ApNT C D F'' G'' T'' (@FOb B C F' (@FOb A B F a))) (@FMor C D G'' (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)))) (@FMor C D G'' (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)))) *)
apply Build_Equal_hom.
(* *) apply
       Trans
        with
          (T'' (F' (F a)) o FMor G'' (T' (F a)) o FMor G'' (FMor G' (T a))).
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G b))) (@FMor B C F' (@FOb A B F a) (@FOb A B G b) (@Comp B (@FOb A B F a) (@FOb A B G a) (@FOb A B G b) (@ApNT A B F G T a) (@FMor A B G a b f))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) (@ApNT B C F' G' T' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f)) (@ApNT B C F' G' T' (@FOb A B G b)))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@Comp C (@FOb B C F' (@FOb A B G a)) (@FOb B C F' (@FOb A B G b)) (@FOb B C G' (@FOb A B G b)) (@FMor B C F' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f)) (@ApNT B C F' G' T' (@FOb A B G b)))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
(* Goal: @Equal (@Hom C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G b))) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FOb B C G' (@FOb A B G b)) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C F' (@FOb A B G a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C F' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)) (@ApNT B C F' G' T' (@FOb A B G a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) (@Comp C (@Comp_FOb A B C F F' a) (@Comp_FOb A B C G G' a) (@Comp_FOb A B C G G' b) (@Comp C (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@ApNT B C F' G' T' (@FOb A B F a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))) (@FMor B C G' (@FOb A B G a) (@FOb A B G b) (@FMor A B G a b f))) *)
apply Comp_l; apply FComp.
(* Goal: @Equal (@Hom D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a)))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@ApNT C D F'' G'' T'' (@FOb B C F' (@FOb A B F a))) (@Comp D (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@FMor C D G'' (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a))) (@FMor C D G'' (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a))))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B G a))) (@Comp D (@FOb C D F'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C F' (@FOb A B F a))) (@FOb C D G'' (@FOb B C G' (@FOb A B F a))) (@ApNT C D F'' G'' T'' (@FOb B C F' (@FOb A B F a))) (@FMor C D G'' (@FOb B C F' (@FOb A B F a)) (@FOb B C G' (@FOb A B F a)) (@ApNT B C F' G' T' (@FOb A B F a)))) (@FMor C D G'' (@FOb B C G' (@FOb A B F a)) (@FOb B C G' (@FOb A B G a)) (@FMor B C G' (@FOb A B F a) (@FOb A B G a) (@ApNT A B F G T a)))) *)
apply Ass.
Qed.

End assoc_horz_comp.

