(* 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           *)
(*****************************************************************************)
(*                                                                           *)
(*          The Functor Category                                             *)
(*                                                                           *)
(*          Amokrane Saibi,  May 1994                                        *)
(*                                                                           *)
(*****************************************************************************)


Require Export Ntransformation.
Require Export Category_dup2.

Set Implicit Arguments.
Unset Strict Implicit.

(* Functor Category *)

Section cat_functor.

Variable C D : Category.

 Section compnt.

 Variables (F G H : Functor C D) (T : NT F G) (T' : NT G H).

 Definition Comp_tau (a : C) := T a o T' a.

 Lemma Comp_tau_nt_law : NT_law Comp_tau.
 Proof.
(* Goal: @NT_law C D F H Comp_tau *)
 unfold Comp_tau in |- *; unfold NT_law in |- *.
(* Goal: forall (a b : Ob C) (f : Carrier (@Hom C a b)), @Equal (@Hom D (@FOb C D F a) (@FOb C D H b)) (@Comp D (@FOb C D F a) (@FOb C D F b) (@FOb C D H b) (@FMor C D F a b f) (@Comp D (@FOb C D F b) (@FOb C D G b) (@FOb C D H b) (@ApNT C D F G T b) (@ApNT C D G H T' b))) (@Comp D (@FOb C D F a) (@FOb C D H a) (@FOb C D H b) (@Comp D (@FOb C D F a) (@FOb C D G a) (@FOb C D H a) (@ApNT C D F G T a) (@ApNT C D G H T' a)) (@FMor C D H a b f)) *)
 intros a b f.
 (* F(f)o((tauFG b)o(tauGH b)) = ((tauFG a)o(tauGH a))oH(f) *)
(* Goal: @Equal (@Hom D (@FOb C D F a) (@FOb C D H b)) (@Comp D (@FOb C D F a) (@FOb C D F b) (@FOb C D H b) (@FMor C D F a b f) (@Comp D (@FOb C D F b) (@FOb C D G b) (@FOb C D H b) (@ApNT C D F G T b) (@ApNT C D G H T' b))) (@Comp D (@FOb C D F a) (@FOb C D H a) (@FOb C D H b) (@Comp D (@FOb C D F a) (@FOb C D G a) (@FOb C D H a) (@ApNT C D F G T a) (@ApNT C D G H T' a)) (@FMor C D H a b f)) *)
 (* *) apply Trans with ((FMor F f o T b) o T' b).
 (* F(f)o((T b)o(T' b)) = (F(f)o(T b))o(T' b) *)
(* Goal: @Equal (@Hom D (@FOb C D a x) (@FOb C D f x)) (@Comp D (@FOb C D a x) (@FOb C D b x) (@FOb C D f x) (@ApNT C D a b T1 x) (@Comp D (@FOb C D b x) (@FOb C D c x) (@FOb C D f x) (@ApNT C D b c T2 x) (@ApNT C D c f T3 x))) (@Comp D (@FOb C D a x) (@FOb C D c x) (@FOb C D f x) (@Comp D (@FOb C D a x) (@FOb C D b x) (@FOb C D c x) (@ApNT C D a b T1 x) (@ApNT C D b c T2 x)) (@ApNT C D c f T3 x)) *)
 apply Ass.
 (* (F(f)o(T' b))o(T' b) = ((T a)o(T' a))oH(f) *) 
(* Goal: @Equal (@Hom D (@FOb C D F a) (@FOb C D H b)) (@Comp D (@FOb C D F a) (@FOb C D G b) (@FOb C D H b) (@Comp D (@FOb C D F a) (@FOb C D F b) (@FOb C D G b) (@FMor C D F a b f) (@ApNT C D F G T b)) (@ApNT C D G H T' b)) (@Comp D (@FOb C D F a) (@FOb C D H a) (@FOb C D H b) (@Comp D (@FOb C D F a) (@FOb C D G a) (@FOb C D H a) (@ApNT C D F G T a) (@ApNT C D G H T' a)) (@FMor C D H a b f)) *)
 (* *) apply Trans with ((T a o FMor G f) o T' b).        
 (* (F(f)o(T' b))o(T' b) = ((T a)oG(f))o(T' b) *) 
(* Goal: @Equal (@Hom D (@FOb C D F a) (@FOb C D H b)) (@Comp D (@FOb C D F a) (@FOb C D G b) (@FOb C D H b) (@Comp D (@FOb C D F a) (@FOb C D F b) (@FOb C D G b) (@FMor C D F a b f) (@ApNT C D F G T b)) (@ApNT C D G H T' b)) (@Comp D (@FOb C D F a) (@FOb C D G b) (@FOb C D H b) (@Comp D (@FOb C D F a) (@FOb C D G a) (@FOb C D G b) (@ApNT C D F G T a) (@FMor C D G a b f)) (@ApNT C D G H T' b)) *)
(* Goal: @Equal (@Hom D (@FOb C D F a) (@FOb C D H b)) (@Comp D (@FOb C D F a) (@FOb C D G b) (@FOb C D H b) (@Comp D (@FOb C D F a) (@FOb C D G a) (@FOb C D G b) (@ApNT C D F G T a) (@FMor C D G a b f)) (@ApNT C D G H T' b)) (@Comp D (@FOb C D F a) (@FOb C D H a) (@FOb C D H b) (@Comp D (@FOb C D F a) (@FOb C D G a) (@FOb C D H a) (@ApNT C D F G T a) (@ApNT C D G H T' a)) (@FMor C D H a b f)) *)
 apply Comp_r; apply NatCond.
 (*  ((T a)oG(f))o(T' b) = ((T a)o(T' a))oH(f) *) 
(* Goal: @Equal (@Hom D (@FOb C D F a) (@FOb C D H b)) (@Comp D (@FOb C D F a) (@FOb C D G b) (@FOb C D H b) (@Comp D (@FOb C D F a) (@FOb C D G a) (@FOb C D G b) (@ApNT C D F G T a) (@FMor C D G a b f)) (@ApNT C D G H T' b)) (@Comp D (@FOb C D F a) (@FOb C D H a) (@FOb C D H b) (@Comp D (@FOb C D F a) (@FOb C D G a) (@FOb C D H a) (@ApNT C D F G T a) (@ApNT C D G H T' a)) (@FMor C D H a b f)) *)
 (* *) apply Trans with (T a o FMor G f o T' b).        
 (* ((T a)oG(f))o(T' b) = (T a)o(G(f)o(T' b)) *)
(* Goal: @Equal (@Hom D (@FOb C D F a) (@FOb C D H b)) (@Comp D (@FOb C D F a) (@FOb C D G b) (@FOb C D H b) (@Comp D (@FOb C D F a) (@FOb C D G a) (@FOb C D G b) (@ApNT C D F G T a) (@FMor C D G a b f)) (@ApNT C D G H T' b)) (@Comp D (@FOb C D F a) (@FOb C D G a) (@FOb C D H b) (@ApNT C D F G T a) (@Comp D (@FOb C D G a) (@FOb C D G b) (@FOb C D H b) (@FMor C D G a b f) (@ApNT C D G H T' b))) *)
(* Goal: @Equal (@Hom D (@FOb C D F a) (@FOb C D H b)) (@Comp D (@FOb C D F a) (@FOb C D G a) (@FOb C D H b) (@ApNT C D F G T a) (@Comp D (@FOb C D G a) (@FOb C D G b) (@FOb C D H b) (@FMor C D G a b f) (@ApNT C D G H T' b))) (@Comp D (@FOb C D F a) (@FOb C D H a) (@FOb C D H b) (@Comp D (@FOb C D F a) (@FOb C D G a) (@FOb C D H a) (@ApNT C D F G T a) (@ApNT C D G H T' a)) (@FMor C D H a b f)) *)
 apply Ass1.
 (* (T a)o(G(f)o(T' b)) = ((T a)o(T' a))oH(f) *) 
(* Goal: @Equal (@Hom D (@FOb C D F a) (@FOb C D H b)) (@Comp D (@FOb C D F a) (@FOb C D G a) (@FOb C D H b) (@ApNT C D F G T a) (@Comp D (@FOb C D G a) (@FOb C D G b) (@FOb C D H b) (@FMor C D G a b f) (@ApNT C D G H T' b))) (@Comp D (@FOb C D F a) (@FOb C D H a) (@FOb C D H b) (@Comp D (@FOb C D F a) (@FOb C D G a) (@FOb C D H a) (@ApNT C D F G T a) (@ApNT C D G H T' a)) (@FMor C D H a b f)) *)
 (* *) apply Trans with (T a o T' a o FMor H f).
 (* (T a)o(G(f)o(T' b)) = (T a)o((T' a)oH(f)) *)
 (* G(f)o(T' b) = (T' a)oH(f) *)
(* Goal: @Equal (@Hom D (@FOb C D F a) (@FOb C D H b)) (@Comp D (@FOb C D F a) (@FOb C D G a) (@FOb C D H b) (@ApNT C D F G T a) (@Comp D (@FOb C D G a) (@FOb C D G b) (@FOb C D H b) (@FMor C D G a b f) (@ApNT C D G H T' b))) (@Comp D (@FOb C D F a) (@FOb C D G a) (@FOb C D H b) (@ApNT C D F G T a) (@Comp D (@FOb C D G a) (@FOb C D H a) (@FOb C D H b) (@ApNT C D G H T' a) (@FMor C D H a b f))) *)
(* Goal: @Equal (@Hom D (@FOb C D F a) (@FOb C D H b)) (@Comp D (@FOb C D F a) (@FOb C D G a) (@FOb C D H b) (@ApNT C D F G T a) (@Comp D (@FOb C D G a) (@FOb C D H a) (@FOb C D H b) (@ApNT C D G H T' a) (@FMor C D H a b f))) (@Comp D (@FOb C D F a) (@FOb C D H a) (@FOb C D H b) (@Comp D (@FOb C D F a) (@FOb C D G a) (@FOb C D H a) (@ApNT C D F G T a) (@ApNT C D G H T' a)) (@FMor C D H a b f)) *)
 apply Comp_l; apply NatCond.
 (* (T a)o(G(f)o(T' b)) = ((T a)o(G(f))o(T' b) *)
(* Goal: @Equal (@Hom D (@FOb C D a x) (@FOb C D f x)) (@Comp D (@FOb C D a x) (@FOb C D b x) (@FOb C D f x) (@ApNT C D a b T1 x) (@Comp D (@FOb C D b x) (@FOb C D c x) (@FOb C D f x) (@ApNT C D b c T2 x) (@ApNT C D c f T3 x))) (@Comp D (@FOb C D a x) (@FOb C D c x) (@FOb C D f x) (@Comp D (@FOb C D a x) (@FOb C D b x) (@FOb C D c x) (@ApNT C D a b T1 x) (@ApNT C D b c T2 x)) (@ApNT C D c f T3 x)) *)
 apply Ass.
 Qed.

 Canonical Structure CompV_NT : NT_setoid F H := Comp_tau_nt_law.

 End compnt.

Lemma CompV_NT_congl : Congl_law'' CompV_NT.  
Proof.
(* Goal: @Congl_law'' (Functor C D) (@NT_setoid C D) CompV_NT *)
unfold Congl_law'' in |- *; simpl in |- *.
(* Goal: @Equal_NT C D a f (@CompV_NT a b f T1 (@CompV_NT b c f T2 T3)) (@CompV_NT a c f (@CompV_NT a b c T1 T2) T3) *)
unfold Equal_NT, CompV_NT in |- *; simpl in |- *.
(* Goal: forall (a b c : Functor C D) (f g : @NT C D a b) (h : @NT C D b c) (_ : forall a0 : Ob C, @Equal (@Hom D (@FOb C D a a0) (@FOb C D b a0)) (@ApNT C D a b f a0) (@ApNT C D a b g a0)) (a0 : Ob C), @Equal (@Hom D (@FOb C D a a0) (@FOb C D c a0)) (@Comp_tau a b c f h a0) (@Comp_tau a b c g h a0) *)
intros F G H T1 T2 T3 eqT1_T2 a; unfold Comp_tau in |- *.
(* Goal: @Equal (@Hom D (@FOb C D F a) (@FOb C D H a)) (@Comp D (@FOb C D F a) (@FOb C D G a) (@FOb C D H a) (@ApNT C D F G T3 a) (@ApNT C D G H T1 a)) (@Comp D (@FOb C D F a) (@FOb C D G a) (@FOb C D H a) (@ApNT C D F G T3 a) (@ApNT C D G H T2 a)) *)
apply Comp_l; apply eqT1_T2.
Qed.

Lemma CompV_NT_congr : Congr_law'' CompV_NT.  
Proof.
(* Goal: @Congr_law'' (Functor C D) (@NT_setoid C D) CompV_NT *)
unfold Congr_law'' in |- *; simpl in |- *.
(* Goal: @Equal_NT C D a f (@CompV_NT a b f T1 (@CompV_NT b c f T2 T3)) (@CompV_NT a c f (@CompV_NT a b c T1 T2) T3) *)
unfold Equal_NT, CompV_NT in |- *; simpl in |- *.
(* Goal: forall (a b c : Functor C D) (f g : @NT C D a b) (h : @NT C D b c) (_ : forall a0 : Ob C, @Equal (@Hom D (@FOb C D a a0) (@FOb C D b a0)) (@ApNT C D a b f a0) (@ApNT C D a b g a0)) (a0 : Ob C), @Equal (@Hom D (@FOb C D a a0) (@FOb C D c a0)) (@Comp_tau a b c f h a0) (@Comp_tau a b c g h a0) *)
intros F G H T1 T2 T3 eqT1_T2 a; unfold Comp_tau in |- *.  
(* Goal: @Equal (@Hom D (@FOb C D F a) (@FOb C D H a)) (@Comp D (@FOb C D F a) (@FOb C D G a) (@FOb C D H a) (@ApNT C D F G T1 a) (@ApNT C D G H T3 a)) (@Comp D (@FOb C D F a) (@FOb C D G a) (@FOb C D H a) (@ApNT C D F G T2 a) (@ApNT C D G H T3 a)) *)
apply Comp_r; apply eqT1_T2.
Qed.

Definition Comp_CatFunct := Build_Comp'' CompV_NT_congl CompV_NT_congr.
   
Lemma Assoc_CatFunct : Assoc_law'' Comp_CatFunct.
Proof.
(* Goal: @Assoc_law'' (Functor C D) (@NT_setoid C D) Comp_CatFunct *)
unfold Assoc_law'' in |- *; intros a b c f.
(* Goal: forall (f0 : Carrier'' (@NT_setoid C D a b)) (g : Carrier'' (@NT_setoid C D b c)) (h : Carrier'' (@NT_setoid C D c f)), @Equal'' (@NT_setoid C D a f) (@Cat_comp'' (Functor C D) (@NT_setoid C D) Comp_CatFunct a b f f0 (@Cat_comp'' (Functor C D) (@NT_setoid C D) Comp_CatFunct b c f g h)) (@Cat_comp'' (Functor C D) (@NT_setoid C D) Comp_CatFunct a c f (@Cat_comp'' (Functor C D) (@NT_setoid C D) Comp_CatFunct a b c f0 g) h) *)
intros T1 T2 T3.
(* Goal: @Equal'' (@NT_setoid C D a f) (@Cat_comp'' (Functor C D) (@NT_setoid C D) Comp_CatFunct a b f T1 (@Cat_comp'' (Functor C D) (@NT_setoid C D) Comp_CatFunct b c f T2 T3)) (@Cat_comp'' (Functor C D) (@NT_setoid C D) Comp_CatFunct a c f (@Cat_comp'' (Functor C D) (@NT_setoid C D) Comp_CatFunct a b c T1 T2) T3) *)
unfold Cat_comp'', Ap2'' in |- *; simpl in |- *.
(* Goal: @Equal_NT C D a f (@CompV_NT a b f T1 (@CompV_NT b c f T2 T3)) (@CompV_NT a c f (@CompV_NT a b c T1 T2) T3) *)
unfold Equal_NT, CompV_NT in |- *; simpl in |- *.
(* Goal: forall a0 : Ob C, @Equal (@Hom D (@FOb C D a a0) (@FOb C D f a0)) (@Comp_tau a b f T1 (@Build_NT C D b f (@Comp_tau b c f T2 T3) (@Comp_tau_nt_law b c f T2 T3)) a0) (@Comp_tau a c f (@Build_NT C D a c (@Comp_tau a b c T1 T2) (@Comp_tau_nt_law a b c T1 T2)) T3 a0) *)
intro x; unfold Comp_tau in |- *; simpl in |- *.
(* Goal: @Equal (@Hom D (@FOb C D a x) (@FOb C D f x)) (@Comp D (@FOb C D a x) (@FOb C D b x) (@FOb C D f x) (@ApNT C D a b T1 x) (@Comp D (@FOb C D b x) (@FOb C D c x) (@FOb C D f x) (@ApNT C D b c T2 x) (@ApNT C D c f T3 x))) (@Comp D (@FOb C D a x) (@FOb C D c x) (@FOb C D f x) (@Comp D (@FOb C D a x) (@FOb C D b x) (@FOb C D c x) (@ApNT C D a b T1 x) (@ApNT C D b c T2 x)) (@ApNT C D c f T3 x)) *)
apply Ass.
Qed.

(* Id *)

 Section id_catfunct_def.

 Variable F : Functor C D.

 Definition Id_CatFunct_tau (a : C) := Id (F a).
 
 Lemma Id_CatFunct_nt_law : NT_law Id_CatFunct_tau.
 Proof.
(* Goal: forall (a b : Ob C) (f : Carrier (@Hom C a b)), @Equal (@Hom D (@FOb C D F a) (@FOb C D H b)) (@Comp D (@FOb C D F a) (@FOb C D F b) (@FOb C D H b) (@FMor C D F a b f) (@Comp D (@FOb C D F b) (@FOb C D G b) (@FOb C D H b) (@ApNT C D F G T b) (@ApNT C D G H T' b))) (@Comp D (@FOb C D F a) (@FOb C D H a) (@FOb C D H b) (@Comp D (@FOb C D F a) (@FOb C D G a) (@FOb C D H a) (@ApNT C D F G T a) (@ApNT C D G H T' a)) (@FMor C D H a b f)) *)
 unfold NT_law, Id_CatFunct_tau in |- *; intros a b f. 
(* Goal: @Equal (@Hom D (@FOb C D F a) (@FOb C D F b)) (@Comp D (@FOb C D F a) (@FOb C D F b) (@FOb C D F b) (@FMor C D F a b f) (@Id D (@FOb C D F b))) (@Comp D (@FOb C D F a) (@FOb C D F a) (@FOb C D F b) (@Id D (@FOb C D F a)) (@FMor C D F a b f)) *)
 (* *) apply Trans with (FMor F f).
(* Goal: @Equal (@Hom D (@FOb C D F a) (@FOb C D F b)) (@Comp D (@FOb C D F a) (@FOb C D F b) (@FOb C D F b) (@FMor C D F a b f) (@Id D (@FOb C D F b))) (@FMor C D F a b f) *)
(* Goal: @Equal (@Hom D (@FOb C D F a) (@FOb C D F b)) (@FMor C D F a b f) (@Comp D (@FOb C D F a) (@FOb C D F a) (@FOb C D F b) (@Id D (@FOb C D F a)) (@FMor C D F a b f)) *)
 apply Idr1.
(* Goal: @Equal (@Hom D (@FOb C D F a) (@FOb C D F b)) (@FMor C D F a b f) (@Comp D (@FOb C D F a) (@FOb C D F a) (@FOb C D F b) (@Id D (@FOb C D F a)) (@FMor C D F a b f)) *)
 apply Idl1.
 Qed.
  
 Canonical Structure Id_CatFunct := Build_NT Id_CatFunct_nt_law.

 End id_catfunct_def.

Lemma Idl_CatFunct : Idl_law'' Comp_CatFunct Id_CatFunct.
Proof.
(* Goal: @Idr_law'' (Functor C D) (@NT_setoid C D) Comp_CatFunct Id_CatFunct *)
red in |- *; simple induction f.
(* Goal: forall (ApNT : forall a0 : Ob C, Carrier (@Hom D (@FOb C D b a0) (@FOb C D a a0))) (Prf_NT_law : @NT_law C D b a ApNT), @Equal'' (@NT_setoid C D b a) (@Build_NT C D b a ApNT Prf_NT_law) (@Cat_comp'' (Functor C D) (@NT_setoid C D) Comp_CatFunct b a a (@Build_NT C D b a ApNT Prf_NT_law) (Id_CatFunct a)) *)
unfold Comp_CatFunct in |- *; unfold Id_CatFunct in |- *; simpl in |- *.
(* Goal: forall (ApNT : forall a0 : Ob C, Carrier (@Hom D (@FOb C D b a0) (@FOb C D a a0))) (Prf_NT_law : @NT_law C D b a ApNT), @Equal_NT C D b a (@Build_NT C D b a ApNT Prf_NT_law) (@Cat_comp'' (Functor C D) (@NT_setoid C D) (@Build_Comp'' (Functor C D) (@NT_setoid C D) CompV_NT CompV_NT_congl CompV_NT_congr) b a a (@Build_NT C D b a ApNT Prf_NT_law) (@Build_NT C D a a (Id_CatFunct_tau a) (@Id_CatFunct_nt_law a))) *)
unfold Equal_NT in |- *; simpl in |- *.
(* Goal: forall (ApNT : forall a0 : Ob C, Carrier (@Hom D (@FOb C D b a0) (@FOb C D a a0))) (Prf_NT_law : @NT_law C D b a ApNT) (a0 : Ob C), @Equal (@Hom D (@FOb C D b a0) (@FOb C D a a0)) (ApNT a0) (@Comp_tau b a a (@Build_NT C D b a ApNT Prf_NT_law) (@Build_NT C D a a (Id_CatFunct_tau a) (@Id_CatFunct_nt_law a)) a0) *)
unfold Comp_tau in |- *; simpl in |- *.
(* Goal: forall (ApNT : forall a0 : Ob C, Carrier (@Hom D (@FOb C D b a0) (@FOb C D a a0))) (_ : @NT_law C D b a ApNT) (a0 : Ob C), @Equal (@Hom D (@FOb C D b a0) (@FOb C D a a0)) (ApNT a0) (@Comp D (@FOb C D b a0) (@FOb C D a a0) (@FOb C D a a0) (ApNT a0) (Id_CatFunct_tau a a0)) *)
unfold Id_CatFunct_tau in |- *; intros.
(* Goal: @Equal (@Hom D (@FOb C D a a0) (@FOb C D b a0)) (@Comp D (@FOb C D a a0) (@FOb C D a a0) (@FOb C D b a0) (@Id D (@FOb C D a a0)) (ApNT a0)) (ApNT a0) *)
apply Idl.
Qed.

Lemma Idr_CatFunct : Idr_law'' Comp_CatFunct Id_CatFunct.
Proof.
(* Goal: @Idr_law'' (Functor C D) (@NT_setoid C D) Comp_CatFunct Id_CatFunct *)
red in |- *; simple induction f.
(* Goal: forall (ApNT : forall a0 : Ob C, Carrier (@Hom D (@FOb C D b a0) (@FOb C D a a0))) (Prf_NT_law : @NT_law C D b a ApNT), @Equal'' (@NT_setoid C D b a) (@Build_NT C D b a ApNT Prf_NT_law) (@Cat_comp'' (Functor C D) (@NT_setoid C D) Comp_CatFunct b a a (@Build_NT C D b a ApNT Prf_NT_law) (Id_CatFunct a)) *)
unfold Comp_CatFunct in |- *; unfold Id_CatFunct in |- *; simpl in |- *.
(* Goal: forall (ApNT : forall a0 : Ob C, Carrier (@Hom D (@FOb C D b a0) (@FOb C D a a0))) (Prf_NT_law : @NT_law C D b a ApNT), @Equal_NT C D b a (@Build_NT C D b a ApNT Prf_NT_law) (@Cat_comp'' (Functor C D) (@NT_setoid C D) (@Build_Comp'' (Functor C D) (@NT_setoid C D) CompV_NT CompV_NT_congl CompV_NT_congr) b a a (@Build_NT C D b a ApNT Prf_NT_law) (@Build_NT C D a a (Id_CatFunct_tau a) (@Id_CatFunct_nt_law a))) *)
unfold Equal_NT in |- *; simpl in |- *.
(* Goal: forall (ApNT : forall a0 : Ob C, Carrier (@Hom D (@FOb C D b a0) (@FOb C D a a0))) (Prf_NT_law : @NT_law C D b a ApNT) (a0 : Ob C), @Equal (@Hom D (@FOb C D b a0) (@FOb C D a a0)) (ApNT a0) (@Comp_tau b a a (@Build_NT C D b a ApNT Prf_NT_law) (@Build_NT C D a a (Id_CatFunct_tau a) (@Id_CatFunct_nt_law a)) a0) *)
unfold Comp_tau in |- *; simpl in |- *.
(* Goal: forall (ApNT : forall a0 : Ob C, Carrier (@Hom D (@FOb C D b a0) (@FOb C D a a0))) (_ : @NT_law C D b a ApNT) (a0 : Ob C), @Equal (@Hom D (@FOb C D b a0) (@FOb C D a a0)) (ApNT a0) (@Comp D (@FOb C D b a0) (@FOb C D a a0) (@FOb C D a a0) (ApNT a0) (Id_CatFunct_tau a a0)) *)
unfold Id_CatFunct_tau in |- *; intros.
(* Goal: @Equal (@Hom D (@FOb C D b a0) (@FOb C D a a0)) (ApNT a0) (@Comp D (@FOb C D b a0) (@FOb C D a a0) (@FOb C D a a0) (ApNT a0) (@Id D (@FOb C D a a0))) *)
apply Idr.
Qed.

Canonical Structure FUNCT :=
  Build_Category'' Assoc_CatFunct Idl_CatFunct Idr_CatFunct.

End cat_functor.

Infix "o_NTv" := CompV_NT (at level 20, right associativity).

