(* 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 Formel - Calculus of Inductive Constructions V5.10        *)
(*****************************************************************************)
(*									     *)
(*            2nd definition (Equational) of Adjunctions       		     *)
(*									     *)
(*****************************************************************************)
(*									     *)
(*                     A. SAIBI	  May 95                  		     *)
(*									     *)
(*****************************************************************************)

Require Export IdCAT.
Require Export Adj_UA.

Set Implicit Arguments.
Unset Strict Implicit.

(* lois des NT: eta et epsilon *)

Section adj1_def.

Variables (C D : Category) (F : Functor D C) (G : Functor C D).

 Section adj1_laws.

 Variables (eta : NT (Id_CAT D) (F o_F G)) (eps : NT (G o_F F) (Id_CAT C)).

 (* Rmq: on utilise idCAT, qui de'finit Id_CAT sans parler
    de Functor_Setoid. Evitant ainsi l'inconsistance des
    univers *)

 Definition Adj1_law1 :=
   forall c : C, eta (G c) o FMor G (eps c) =_S Id (G c).

 Definition Adj1_law2 :=
   forall d : D, FMor F (eta d) o eps (F d) =_S Id (F d).

 End adj1_laws.

 Structure Adj1 : Type := 
   {A_eta : NT (Id_CAT D) (F o_F G);
    A_eps : NT (G o_F F) (Id_CAT C);
    Prf_Adj1_law1 : Adj1_law1 A_eta A_eps;
    Prf_Adj1_law2 : Adj1_law2 A_eta A_eps}.

End adj1_def.

Section adj_to_adj1.

Variables (C D : Category) (F : Functor D C) (G : Functor C D) (ad : Adj F G).

(* *)

Definition Unit_tau (d : D) := UA_mor (Unit ad d).

Lemma Unit_nt_law : NT_law (F:=Id_CAT D) (G:=F o_F G) Unit_tau.
Proof.
(* Goal: @NT_law D D (Id_CAT D) (@Comp_Functor D C D F G) Unit_tau *)
unfold NT_law, Unit_tau in |- *; simpl in |- *.
(* Goal: forall (a b : Ob D) (f : Carrier (@Hom D a b)), @Equal (@Hom D (@Id_CAT_ob D a) (@Comp_FOb D C D F G b)) (@Comp D (@Id_CAT_ob D a) (@Id_CAT_ob D b) (@Comp_FOb D C D F G b) (@FMor D D (Id_CAT D) a b f) (@Unit_arrow C D F G ad b)) (@Comp D (@Id_CAT_ob D a) (@Comp_FOb D C D F G a) (@Comp_FOb D C D F G b) (@Unit_arrow C D F G ad a) (@FMor D D (@Comp_Functor D C D F G) a b f)) *)
unfold Unit_arrow in |- *.
(* Goal: forall (a b : Ob C) (f : Carrier (@Hom C a b)), @Equal (@Hom C (@Comp_FOb C D C G F a) (@Id_CAT_ob C b)) (@Comp C (@Comp_FOb C D C G F a) (@Comp_FOb C D C G F b) (@Id_CAT_ob C b) (@FMor C C (@Comp_Functor C D C G F) a b f) (@ApAphi_inv C D F G (@FOb C D G b) b ad (@Id D (@FOb C D G b)))) (@Comp C (@Comp_FOb C D C G F a) (@Id_CAT_ob C a) (@Id_CAT_ob C b) (@ApAphi_inv C D F G (@FOb C D G a) a ad (@Id D (@FOb C D G a))) (@FMor C C (Id_CAT C) a b f)) *)
unfold FMor at 1 2 in |- *; simpl in |- *.
(* Goal: forall (a b : Ob D) (f : Carrier (@Hom D a b)), @Equal (@Hom D (@Id_CAT_ob D a) (@Comp_FOb D C D F G b)) (@Comp D (@Id_CAT_ob D a) (@Id_CAT_ob D b) (@Comp_FOb D C D F G b) (@Id_fun (@Hom D a b) f) (@ApAphi C D F G b (@FOb D C F b) ad (@Id C (@FOb D C F b)))) (@Comp D (@Id_CAT_ob D a) (@Comp_FOb D C D F G a) (@Comp_FOb D C D F G b) (@ApAphi C D F G a (@FOb D C F a) ad (@Id C (@FOb D C F a))) (@Comp_FMor D C D F G a b f)) *)
unfold Comp_FMor, Comp_FOb, Id_CAT_ob in |- *; intros d1 d2 f.
(* Goal: @Equal (@Hom D d1 (@FOb C D G (@FOb D C F d2))) (@Comp D d1 d2 (@FOb C D G (@FOb D C F d2)) (@Id_fun (@Hom D d1 d2) f) (@ApAphi C D F G d2 (@FOb D C F d2) ad (@Id C (@FOb D C F d2)))) (@Comp D d1 (@FOb C D G (@FOb D C F d1)) (@FOb C D G (@FOb D C F d2)) (@ApAphi C D F G d1 (@FOb D C F d1) ad (@Id C (@FOb D C F d1))) (@FMor C D G (@FOb D C F d1) (@FOb D C F d2) (@FMor D C F d1 d2 f))) *)
(* *) apply Trans with (ApAphi ad (FMor F f o Id (F d2))).
(* Goal: @Equal (@Hom D d1 (@FOb C D G (@FOb D C F d2))) (@Comp D d1 d2 (@FOb C D G (@FOb D C F d2)) (@Id_fun (@Hom D d1 d2) f) (@ApAphi C D F G d2 (@FOb D C F d2) ad (@Id C (@FOb D C F d2)))) (@ApAphi C D F G d1 (@FOb D C F d2) ad (@Comp C (@FOb D C F d1) (@FOb D C F d2) (@FOb D C F d2) (@FMor D C F d1 d2 f) (@Id C (@FOb D C F d2)))) *)
(* Goal: @Equal (@Hom D d1 (@FOb C D G (@FOb D C F d2))) (@ApAphi C D F G d1 (@FOb D C F d2) ad (@Comp C (@FOb D C F d1) (@FOb D C F d2) (@FOb D C F d2) (@FMor D C F d1 d2 f) (@Id C (@FOb D C F d2)))) (@Comp D d1 (@FOb C D G (@FOb D C F d1)) (@FOb C D G (@FOb D C F d2)) (@ApAphi C D F G d1 (@FOb D C F d1) ad (@Id C (@FOb D C F d1))) (@FMor C D G (@FOb D C F d1) (@FOb D C F d2) (@FMor D C F d1 d2 f))) *)
apply Sym; apply (Adj_eq4 ad f (Id (F d2))).
(* Goal: @Equal (@Hom D d1 (@FOb C D G (@FOb D C F d2))) (@ApAphi C D F G d1 (@FOb D C F d2) ad (@Comp C (@FOb D C F d1) (@FOb D C F d2) (@FOb D C F d2) (@FMor D C F d1 d2 f) (@Id C (@FOb D C F d2)))) (@Comp D d1 (@FOb C D G (@FOb D C F d1)) (@FOb C D G (@FOb D C F d2)) (@ApAphi C D F G d1 (@FOb D C F d1) ad (@Id C (@FOb D C F d1))) (@FMor C D G (@FOb D C F d1) (@FOb D C F d2) (@FMor D C F d1 d2 f))) *)
(* *) apply Trans with (ApAphi ad (Id (F d1) o FMor F f)).
(* Goal: @Equal (@Hom D d1 (@FOb C D G (@FOb D C F d2))) (@ApAphi C D F G d1 (@FOb D C F d2) ad (@Comp C (@FOb D C F d1) (@FOb D C F d2) (@FOb D C F d2) (@FMor D C F d1 d2 f) (@Id C (@FOb D C F d2)))) (@ApAphi C D F G d1 (@FOb D C F d2) ad (@Comp C (@FOb D C F d1) (@FOb D C F d1) (@FOb D C F d2) (@Id C (@FOb D C F d1)) (@FMor D C F d1 d2 f))) *)
(* Goal: @Equal (@Hom D d1 (@FOb C D G (@FOb D C F d2))) (@ApAphi C D F G d1 (@FOb D C F d2) ad (@Comp C (@FOb D C F d1) (@FOb D C F d1) (@FOb D C F d2) (@Id C (@FOb D C F d1)) (@FMor D C F d1 d2 f))) (@Comp D d1 (@FOb C D G (@FOb D C F d1)) (@FOb C D G (@FOb D C F d2)) (@ApAphi C D F G d1 (@FOb D C F d1) ad (@Id C (@FOb D C F d1))) (@FMor C D G (@FOb D C F d1) (@FOb D C F d2) (@FMor D C F d1 d2 f))) *)
apply AphiPres; apply Idrl.
(* Goal: @Equal (@Hom D d1 (@FOb C D G (@FOb D C F d2))) (@ApAphi C D F G d1 (@FOb D C F d2) ad (@Comp C (@FOb D C F d1) (@FOb D C F d1) (@FOb D C F d2) (@Id C (@FOb D C F d1)) (@FMor D C F d1 d2 f))) (@Comp D d1 (@FOb C D G (@FOb D C F d1)) (@FOb C D G (@FOb D C F d2)) (@ApAphi C D F G d1 (@FOb D C F d1) ad (@Id C (@FOb D C F d1))) (@FMor C D G (@FOb D C F d1) (@FOb D C F d2) (@FMor D C F d1 d2 f))) *)
apply (Adj_eq3 ad (FMor F f) (Id (F d1))).
Qed.

Canonical Structure Unit_NT := Build_NT Unit_nt_law.

(* *)

Definition CoUnit_tau (c : C) := CoUA_mor (CoUnit ad c).

Lemma CoUnit_nt_law : NT_law (F:=G o_F F) (G:=Id_CAT C) CoUnit_tau.
Proof.
(* Goal: @NT_law C C (@Comp_Functor C D C G F) (Id_CAT C) CoUnit_tau *)
unfold NT_law, CoUnit_tau in |- *; simpl in |- *.
(* Goal: forall (a b : Ob C) (f : Carrier (@Hom C a b)), @Equal (@Hom C (@Comp_FOb C D C G F a) (@Id_CAT_ob C b)) (@Comp C (@Comp_FOb C D C G F a) (@Comp_FOb C D C G F b) (@Id_CAT_ob C b) (@FMor C C (@Comp_Functor C D C G F) a b f) (@CoUnit_arrow C D F G ad b)) (@Comp C (@Comp_FOb C D C G F a) (@Id_CAT_ob C a) (@Id_CAT_ob C b) (@CoUnit_arrow C D F G ad a) (@FMor C C (Id_CAT C) a b f)) *)
unfold CoUnit_arrow in |- *.
(* Goal: forall (a b : Ob C) (f : Carrier (@Hom C a b)), @Equal (@Hom C (@Comp_FOb C D C G F a) (@Id_CAT_ob C b)) (@Comp C (@Comp_FOb C D C G F a) (@Comp_FOb C D C G F b) (@Id_CAT_ob C b) (@FMor C C (@Comp_Functor C D C G F) a b f) (@ApAphi_inv C D F G (@FOb C D G b) b ad (@Id D (@FOb C D G b)))) (@Comp C (@Comp_FOb C D C G F a) (@Id_CAT_ob C a) (@Id_CAT_ob C b) (@ApAphi_inv C D F G (@FOb C D G a) a ad (@Id D (@FOb C D G a))) (@FMor C C (Id_CAT C) a b f)) *)
unfold FMor at 1 2 in |- *; simpl in |- *.
(* Goal: forall (a b : Ob C) (f : Carrier (@Hom C a b)), @Equal (@Hom C (@Comp_FOb C D C G F a) (@Id_CAT_ob C b)) (@Comp C (@Comp_FOb C D C G F a) (@Comp_FOb C D C G F b) (@Id_CAT_ob C b) (@Comp_FMor C D C G F a b f) (@ApAphi_inv C D F G (@FOb C D G b) b ad (@Id D (@FOb C D G b)))) (@Comp C (@Comp_FOb C D C G F a) (@Id_CAT_ob C a) (@Id_CAT_ob C b) (@ApAphi_inv C D F G (@FOb C D G a) a ad (@Id D (@FOb C D G a))) (@Id_fun (@Hom C a b) f)) *)
unfold Comp_FMor, Comp_FOb, Id_CAT_ob in |- *.
(* Goal: forall (a b : Ob C) (f : Carrier (@Hom C a b)), @Equal (@Hom C (@FOb D C F (@FOb C D G a)) b) (@Comp C (@FOb D C F (@FOb C D G a)) (@FOb D C F (@FOb C D G b)) b (@FMor D C F (@FOb C D G a) (@FOb C D G b) (@FMor C D G a b f)) (@ApAphi_inv C D F G (@FOb C D G b) b ad (@Id D (@FOb C D G b)))) (@Comp C (@FOb D C F (@FOb C D G a)) a b (@ApAphi_inv C D F G (@FOb C D G a) a ad (@Id D (@FOb C D G a))) (@Id_fun (@Hom C a b) f)) *)
intros c1 c2 f.
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb C D G c1)) c2) (@Comp C (@FOb D C F (@FOb C D G c1)) (@FOb D C F (@FOb C D G c2)) c2 (@FMor D C F (@FOb C D G c1) (@FOb C D G c2) (@FMor C D G c1 c2 f)) (@ApAphi_inv C D F G (@FOb C D G c2) c2 ad (@Id D (@FOb C D G c2)))) (@Comp C (@FOb D C F (@FOb C D G c1)) c1 c2 (@ApAphi_inv C D F G (@FOb C D G c1) c1 ad (@Id D (@FOb C D G c1))) (@Id_fun (@Hom C c1 c2) f)) *)
(* *) apply Trans with (ApAphi_inv ad (FMor G f o Id (G c2))).
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb C D G c1)) c2) (@Comp C (@FOb D C F (@FOb C D G c1)) (@FOb D C F (@FOb C D G c2)) c2 (@FMor D C F (@FOb C D G c1) (@FOb C D G c2) (@FMor C D G c1 c2 f)) (@ApAphi_inv C D F G (@FOb C D G c2) c2 ad (@Id D (@FOb C D G c2)))) (@ApAphi_inv C D F G (@FOb C D G c1) c2 ad (@Comp D (@FOb C D G c1) (@FOb C D G c2) (@FOb C D G c2) (@FMor C D G c1 c2 f) (@Id D (@FOb C D G c2)))) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb C D G c1)) c2) (@ApAphi_inv C D F G (@FOb C D G c1) c2 ad (@Comp D (@FOb C D G c1) (@FOb C D G c2) (@FOb C D G c2) (@FMor C D G c1 c2 f) (@Id D (@FOb C D G c2)))) (@Comp C (@FOb D C F (@FOb C D G c1)) c1 c2 (@ApAphi_inv C D F G (@FOb C D G c1) c1 ad (@Id D (@FOb C D G c1))) (@Id_fun (@Hom C c1 c2) f)) *)
apply Sym; apply (Adj_eq6 ad (FMor G f) (Id (G c2))). 
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb C D G c1)) c2) (@ApAphi_inv C D F G (@FOb C D G c1) c2 ad (@Comp D (@FOb C D G c1) (@FOb C D G c2) (@FOb C D G c2) (@FMor C D G c1 c2 f) (@Id D (@FOb C D G c2)))) (@Comp C (@FOb D C F (@FOb C D G c1)) c1 c2 (@ApAphi_inv C D F G (@FOb C D G c1) c1 ad (@Id D (@FOb C D G c1))) (@Id_fun (@Hom C c1 c2) f)) *)
(* *) apply Trans with (ApAphi_inv ad (Id (G c1) o FMor G f)).
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb C D G c1)) c2) (@ApAphi_inv C D F G (@FOb C D G c1) c2 ad (@Comp D (@FOb C D G c1) (@FOb C D G c2) (@FOb C D G c2) (@FMor C D G c1 c2 f) (@Id D (@FOb C D G c2)))) (@ApAphi_inv C D F G (@FOb C D G c1) c2 ad (@Comp D (@FOb C D G c1) (@FOb C D G c1) (@FOb C D G c2) (@Id D (@FOb C D G c1)) (@FMor C D G c1 c2 f))) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb C D G c1)) c2) (@ApAphi_inv C D F G (@FOb C D G c1) c2 ad (@Comp D (@FOb C D G c1) (@FOb C D G c1) (@FOb C D G c2) (@Id D (@FOb C D G c1)) (@FMor C D G c1 c2 f))) (@Comp C (@FOb D C F (@FOb C D G c1)) c1 c2 (@ApAphi_inv C D F G (@FOb C D G c1) c1 ad (@Id D (@FOb C D G c1))) (@Id_fun (@Hom C c1 c2) f)) *)
apply Aphi_invPres; apply Idrl.
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb C D G c1)) c2) (@ApAphi_inv C D F G (@FOb C D G c1) c2 ad (@Comp D (@FOb C D G c1) (@FOb C D G c1) (@FOb C D G c2) (@Id D (@FOb C D G c1)) (@FMor C D G c1 c2 f))) (@Comp C (@FOb D C F (@FOb C D G c1)) c1 c2 (@ApAphi_inv C D F G (@FOb C D G c1) c1 ad (@Id D (@FOb C D G c1))) (@Id_fun (@Hom C c1 c2) f)) *)
apply (Adj_eq5 ad f (Id (G c1))).
Qed.
 
Canonical Structure CoUnit_NT := Build_NT CoUnit_nt_law.

(* Unit et CoUnit verifient ces deux lois *)

Lemma Unit_and_CoUnit_law1 : Adj1_law1 Unit_NT CoUnit_NT.
Proof.
(* Goal: @Adj1_law1 C D F G Unit_NT CoUnit_NT *)
unfold Adj1_law1, Unit_NT, CoUnit_NT in |- *; simpl in |- *.
(* Goal: forall d : Ob D, @Equal (@Hom C (@FOb D C F (@Id_CAT_ob D d)) (@Id_CAT_ob C (@FOb D C F d))) (@Comp C (@FOb D C F (@Id_CAT_ob D d)) (@FOb D C F (@Comp_FOb D C D F G d)) (@Id_CAT_ob C (@FOb D C F d)) (@FMor D C F (@Id_CAT_ob D d) (@Comp_FOb D C D F G d) (Unit_tau d)) (CoUnit_tau (@FOb D C F d))) (@Id C (@FOb D C F d)) *)
unfold Unit_tau, CoUnit_tau in |- *; simpl in |- *.
(* Goal: forall d : Ob D, @Equal (@Hom C (@FOb D C F (@Id_CAT_ob D d)) (@Id_CAT_ob C (@FOb D C F d))) (@Comp C (@FOb D C F (@Id_CAT_ob D d)) (@FOb D C F (@Comp_FOb D C D F G d)) (@Id_CAT_ob C (@FOb D C F d)) (@FMor D C F (@Id_CAT_ob D d) (@Comp_FOb D C D F G d) (@Unit_arrow C D F G ad d)) (@CoUnit_arrow C D F G ad (@FOb D C F d))) (@Id C (@FOb D C F d)) *)
unfold Unit_arrow, CoUnit_arrow, Id_CAT_ob in |- *.
(* Goal: forall c : Ob C, @Equal (@Hom D (@FOb C D G c) (@FOb C D G c)) (@Comp D (@FOb C D G c) (@Comp_FOb D C D F G (@FOb C D G c)) (@FOb C D G c) (@ApAphi C D F G (@FOb C D G c) (@FOb D C F (@FOb C D G c)) ad (@Id C (@FOb D C F (@FOb C D G c)))) (@FMor C D G (@Comp_FOb C D C G F c) c (@ApAphi_inv C D F G (@FOb C D G c) c ad (@Id D (@FOb C D G c))))) (@Id D (@FOb C D G c)) *)
intro c.
(* Goal: @Equal (@Hom D (@FOb C D G c) (@FOb C D G c)) (@Comp D (@FOb C D G c) (@Comp_FOb D C D F G (@FOb C D G c)) (@FOb C D G c) (@ApAphi C D F G (@FOb C D G c) (@FOb D C F (@FOb C D G c)) ad (@Id C (@FOb D C F (@FOb C D G c)))) (@FMor C D G (@Comp_FOb C D C G F c) c (@ApAphi_inv C D F G (@FOb C D G c) c ad (@Id D (@FOb C D G c))))) (@Id D (@FOb C D G c)) *)
(* *) apply Trans with (ApAphi ad (Id (F (G c)) o ApAphi_inv ad (Id (G c)))).
(* Goal: @Equal (@Hom D (@FOb C D G c) (@FOb C D G c)) (@Comp D (@FOb C D G c) (@Comp_FOb D C D F G (@FOb C D G c)) (@FOb C D G c) (@ApAphi C D F G (@FOb C D G c) (@FOb D C F (@FOb C D G c)) ad (@Id C (@FOb D C F (@FOb C D G c)))) (@FMor C D G (@Comp_FOb C D C G F c) c (@ApAphi_inv C D F G (@FOb C D G c) c ad (@Id D (@FOb C D G c))))) (@ApAphi C D F G (@FOb C D G c) c ad (@Comp C (@FOb D C F (@FOb C D G c)) (@FOb D C F (@FOb C D G c)) c (@Id C (@FOb D C F (@FOb C D G c))) (@ApAphi_inv C D F G (@FOb C D G c) c ad (@Id D (@FOb C D G c))))) *)
(* Goal: @Equal (@Hom D (@FOb C D G c) (@FOb C D G c)) (@ApAphi C D F G (@FOb C D G c) c ad (@Comp C (@FOb D C F (@FOb C D G c)) (@FOb D C F (@FOb C D G c)) c (@Id C (@FOb D C F (@FOb C D G c))) (@ApAphi_inv C D F G (@FOb C D G c) c ad (@Id D (@FOb C D G c))))) (@Id D (@FOb C D G c)) *)
apply Sym; apply (Adj_eq3 ad (ApAphi_inv ad (Id (G c))) (Id (F (G c)))).
(* Goal: @Equal (@Hom D (@FOb C D G c) (@FOb C D G c)) (@ApAphi C D F G (@FOb C D G c) c ad (@Comp C (@FOb D C F (@FOb C D G c)) (@FOb D C F (@FOb C D G c)) c (@Id C (@FOb D C F (@FOb C D G c))) (@ApAphi_inv C D F G (@FOb C D G c) c ad (@Id D (@FOb C D G c))))) (@Id D (@FOb C D G c)) *)
(* *) apply Trans with (ApAphi ad (ApAphi_inv ad (Id (G c)))).
(* Goal: @Equal (@Hom D (@FOb C D G c) (@FOb C D G c)) (@ApAphi C D F G (@FOb C D G c) c ad (@Comp C (@FOb D C F (@FOb C D G c)) (@FOb D C F (@FOb C D G c)) c (@Id C (@FOb D C F (@FOb C D G c))) (@ApAphi_inv C D F G (@FOb C D G c) c ad (@Id D (@FOb C D G c))))) (@ApAphi C D F G (@FOb C D G c) c ad (@ApAphi_inv C D F G (@FOb C D G c) c ad (@Id D (@FOb C D G c)))) *)
(* Goal: @Equal (@Hom D (@FOb C D G c) (@FOb C D G c)) (@ApAphi C D F G (@FOb C D G c) c ad (@ApAphi_inv C D F G (@FOb C D G c) c ad (@Id D (@FOb C D G c)))) (@Id D (@FOb C D G c)) *)
apply AphiPres; apply Idl.
(* Goal: @Equal (@Hom D (@FOb C D G c) (@FOb C D G c)) (@ApAphi C D F G (@FOb C D G c) c ad (@ApAphi_inv C D F G (@FOb C D G c) c ad (@Id D (@FOb C D G c)))) (@Id D (@FOb C D G c)) *)
apply (Idl_inv (NTa_areIso ad (Build_POb1 (G c) c)) (Id (G c))).
Qed.

Lemma Unit_and_CoUnit_law2 : Adj1_law2 Unit_NT CoUnit_NT.
Proof.
(* Goal: @Adj1_law2 C D F G Unit_NT CoUnit_NT *)
unfold Adj1_law2, Unit_NT, CoUnit_NT in |- *; simpl in |- *.
(* Goal: forall d : Ob D, @Equal (@Hom C (@FOb D C F (@Id_CAT_ob D d)) (@Id_CAT_ob C (@FOb D C F d))) (@Comp C (@FOb D C F (@Id_CAT_ob D d)) (@FOb D C F (@Comp_FOb D C D F G d)) (@Id_CAT_ob C (@FOb D C F d)) (@FMor D C F (@Id_CAT_ob D d) (@Comp_FOb D C D F G d) (Unit_tau d)) (CoUnit_tau (@FOb D C F d))) (@Id C (@FOb D C F d)) *)
unfold Unit_tau, CoUnit_tau in |- *; simpl in |- *.
(* Goal: forall d : Ob D, @Equal (@Hom C (@FOb D C F (@Id_CAT_ob D d)) (@Id_CAT_ob C (@FOb D C F d))) (@Comp C (@FOb D C F (@Id_CAT_ob D d)) (@FOb D C F (@Comp_FOb D C D F G d)) (@Id_CAT_ob C (@FOb D C F d)) (@FMor D C F (@Id_CAT_ob D d) (@Comp_FOb D C D F G d) (@Unit_arrow C D F G ad d)) (@CoUnit_arrow C D F G ad (@FOb D C F d))) (@Id C (@FOb D C F d)) *)
unfold Unit_arrow, CoUnit_arrow, Id_CAT_ob in |- *.
(* Goal: forall d : Ob D, @Equal (@Hom C (@FOb D C F d) (@FOb D C F d)) (@Comp C (@FOb D C F d) (@FOb D C F (@Comp_FOb D C D F G d)) (@FOb D C F d) (@FMor D C F d (@Comp_FOb D C D F G d) (@ApAphi C D F G d (@FOb D C F d) ad (@Id C (@FOb D C F d)))) (@ApAphi_inv C D F G (@FOb C D G (@FOb D C F d)) (@FOb D C F d) ad (@Id D (@FOb C D G (@FOb D C F d))))) (@Id C (@FOb D C F d)) *)
intro d.
(* Goal: @Equal (@Hom C (@FOb D C F d) (@FOb D C F d)) (@Comp C (@FOb D C F d) (@FOb D C F (@Comp_FOb D C D F G d)) (@FOb D C F d) (@FMor D C F d (@Comp_FOb D C D F G d) (@ApAphi C D F G d (@FOb D C F d) ad (@Id C (@FOb D C F d)))) (@ApAphi_inv C D F G (@FOb C D G (@FOb D C F d)) (@FOb D C F d) ad (@Id D (@FOb C D G (@FOb D C F d))))) (@Id C (@FOb D C F d)) *)
(* *) apply Trans with (ApAphi_inv ad (ApAphi ad (Id (F d)) o Id (G (F d)))).
(* Goal: @Equal (@Hom C (@FOb D C F d) (@FOb D C F d)) (@Comp C (@FOb D C F d) (@FOb D C F (@Comp_FOb D C D F G d)) (@FOb D C F d) (@FMor D C F d (@Comp_FOb D C D F G d) (@ApAphi C D F G d (@FOb D C F d) ad (@Id C (@FOb D C F d)))) (@ApAphi_inv C D F G (@FOb C D G (@FOb D C F d)) (@FOb D C F d) ad (@Id D (@FOb C D G (@FOb D C F d))))) (@ApAphi_inv C D F G d (@FOb D C F d) ad (@Comp D d (@FOb C D G (@FOb D C F d)) (@FOb C D G (@FOb D C F d)) (@ApAphi C D F G d (@FOb D C F d) ad (@Id C (@FOb D C F d))) (@Id D (@FOb C D G (@FOb D C F d))))) *)
(* Goal: @Equal (@Hom C (@FOb D C F d) (@FOb D C F d)) (@ApAphi_inv C D F G d (@FOb D C F d) ad (@Comp D d (@FOb C D G (@FOb D C F d)) (@FOb C D G (@FOb D C F d)) (@ApAphi C D F G d (@FOb D C F d) ad (@Id C (@FOb D C F d))) (@Id D (@FOb C D G (@FOb D C F d))))) (@Id C (@FOb D C F d)) *)
apply Sym; apply (Adj_eq6 ad (ApAphi ad (Id (F d))) (Id (G (F d)))).
(* Goal: @Equal (@Hom C (@FOb D C F d) (@FOb D C F d)) (@ApAphi_inv C D F G d (@FOb D C F d) ad (@Comp D d (@FOb C D G (@FOb D C F d)) (@FOb C D G (@FOb D C F d)) (@ApAphi C D F G d (@FOb D C F d) ad (@Id C (@FOb D C F d))) (@Id D (@FOb C D G (@FOb D C F d))))) (@Id C (@FOb D C F d)) *)
(* *) apply Trans with (ApAphi_inv ad (ApAphi ad (Id (F d)))).
(* Goal: @Equal (@Hom C (@FOb D C F d) (@FOb D C F d)) (@ApAphi_inv C D F G d (@FOb D C F d) ad (@Comp D d (@FOb C D G (@FOb D C F d)) (@FOb C D G (@FOb D C F d)) (@ApAphi C D F G d (@FOb D C F d) ad (@Id C (@FOb D C F d))) (@Id D (@FOb C D G (@FOb D C F d))))) (@ApAphi_inv C D F G d (@FOb D C F d) ad (@ApAphi C D F G d (@FOb D C F d) ad (@Id C (@FOb D C F d)))) *)
(* Goal: @Equal (@Hom C (@FOb D C F d) (@FOb D C F d)) (@ApAphi_inv C D F G d (@FOb D C F d) ad (@ApAphi C D F G d (@FOb D C F d) ad (@Id C (@FOb D C F d)))) (@Id C (@FOb D C F d)) *)
apply Aphi_invPres; apply Idr1.
(* Goal: @Equal (@Hom C (@FOb D C F d) (@FOb D C F d)) (@ApAphi_inv C D F G d (@FOb D C F d) ad (@ApAphi C D F G d (@FOb D C F d) ad (@Id C (@FOb D C F d)))) (@Id C (@FOb D C F d)) *)
apply (Idr_inv (NTa_areIso ad (Build_POb1 d (F d))) (Id (F d))).
Qed.

Canonical Structure Adj_to_Adj1 :=
  Build_Adj1 Unit_and_CoUnit_law1 Unit_and_CoUnit_law2.

End adj_to_adj1.

Coercion Adj_to_Adj1 : Adj >-> Adj1.

(* *)

Section adj1_to_adj.

Variables (C D : Category) (F : Functor D C) (G : Functor C D)
  (ad : Adj1 F G).

(* a` partir de ces elements, construisons une adjunction, i.e.
   un iso teta : C(F-,-) -> D(-,G-) *)

 Section teta_tau_def.

 Variable dxc : POb (Dual D) C.

 Definition Teta_arrow (f : F (OB_l dxc) --> Ob_r dxc) :=
   A_eta ad (OB_l dxc) o FMor G f.

 Lemma Teta_arrow_map_law : Map_law Teta_arrow.
 Proof.
(* Goal: @Map_law (@Hom C (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc)) (@Hom D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc))) Teta_arrow *)
 unfold Map_law, Teta_arrow in |- *.
(* Goal: forall (x y : Carrier (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)))) (_ : @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) x y), @Equal (@Hom C (@FOb D C F (@OB_l C D dxc)) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) x) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) y) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))) *)
 intros f g H.
(* Goal: @Equal (@Hom D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f)) (@Comp D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) g)) *)
 unfold FOb at 1 in |- *; simpl in |- *; unfold Id_CAT_ob in |- *.
(* Goal: @Equal (@Hom D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)))) (@Comp D (@Id_CAT_ob D (@OB_l C D dxc)) (@Comp_FOb D C D F G (@OB_l C D dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) (@Comp C (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Id_CAT_ob C (@Ob_r (Dual D) C dxc)) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) f) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))))) (@Comp D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc)) (@Comp D (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc)))) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) f)) (@FMor C D G (@FOb C C (@Comp_Functor C D C G F) (@Ob_r (Dual D) C dxc)) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))))) *)
(* Goal: @Equal (@Hom D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)))) (@Comp D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc)) (@Comp D (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc)))) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) f)) (@FMor C D G (@FOb C C (@Comp_Functor C D C G F) (@Ob_r (Dual D) C dxc)) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))))) f *)
(* Goal: forall x : Carrier (@FunSET2_r_ob C D F dxc), @Equal (@FunSET2_r_ob C D F dxc) (@Teta_1_arrow dxc (@Teta_arrow dxc x)) (@Id_fun (@FunSET2_r_ob C D F dxc) x) *)
 apply Comp_l.
(* Goal: @Equal (@Hom D (@Comp_FOb D C D F G (@OB_l C D dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) g) *)
 unfold Comp_FOb in |- *; apply FPres; assumption.
 Qed.

 Canonical Structure Teta_tau := Build_Map Teta_arrow_map_law.

 End teta_tau_def.

Lemma Teta_tau_NT_law : NT_law (F:=FunSET2_r F) (G:=FunSET2_l G) Teta_tau.
Proof.
(* Goal: @NT_law (PROD (Dual D) C) SET (@FunSET2_r C D F) (@FunSET2_l C D G) Teta_tau *)
unfold NT_law, Teta_tau, Teta_arrow in |- *; simpl in |- *.
(* Goal: forall (a b : POb (Dual D) C) (f : @Pmor (Dual D) C a b), @Ext (@FunSET2_l_ob C D G a) (@FunSET2_r_ob C D F b) (@Comp SET (@FunSET2_l_ob C D G a) (@FunSET2_l_ob C D G b) (@FunSET2_r_ob C D F b) (@FMor (PROD (Dual D) C) SET (@FunSET2_l C D G) a b f) (Teta_1_tau b)) (@Comp SET (@FunSET2_l_ob C D G a) (@FunSET2_r_ob C D F a) (@FunSET2_r_ob C D F b) (Teta_1_tau a) (@FMor (PROD (Dual D) C) SET (@FunSET2_r C D F) a b f)) *)
unfold Ext in |- *; simpl in |- *.
(* Goal: forall (a b : POb (Dual D) C) (f : @Pmor (Dual D) C a b) (x : Carrier (@FunSET2_l_ob C D G a)), @Equal (@FunSET2_r_ob C D F b) (@Teta_1_arrow b (@FunSET2_l_mor1 C D G a b f x)) (@FunSET2_r_mor1 C D F a b f (@Teta_1_arrow a x)) *)
intros d1xc1 d2xc2 fxg h.
(* Goal: @Equal (@FunSET2_l_ob C D G d2xc2) (@Comp D (@Id_CAT_ob D (@OB_l C D d2xc2)) (@Comp_FOb D C D F G (@OB_l C D d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D d2xc2)) (@FMor C D G (@FOb D C F (@OB_l C D d2xc2)) (@Ob_r (Dual D) C d2xc2) (@FunSET2_r_mor1 C D F d1xc1 d2xc2 fxg h))) (@FunSET2_l_mor1 C D G d1xc1 d2xc2 fxg (@Comp D (@Id_CAT_ob D (@OB_l C D d1xc1)) (@Comp_FOb D C D F G (@OB_l C D d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D d1xc1)) (@FMor C D G (@FOb D C F (@OB_l C D d1xc1)) (@Ob_r (Dual D) C d1xc1) h))) *)
unfold FunSET2_r_mor1, FunSET2_l_mor1 in |- *.
(* Goal: forall x : Carrier (@FunSET2_l_ob C D G dxc), @Equal (@FunSET2_l_ob C D G dxc) (@Comp D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) (@Comp C (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) x) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))))) x *)
(* Goal: forall x : Carrier (@FunSET2_r_ob C D F dxc), @Equal (@FunSET2_r_ob C D F dxc) (@Teta_1_arrow dxc (@Teta_arrow dxc x)) (@Id_fun (@FunSET2_r_ob C D F dxc) x) *)
unfold FOb at 1 in |- *; simpl in |- *; unfold FunSET2_l_ob in |- *.
(* *) apply
       Trans
        with
          (A_eta ad (OB_l d2xc2)
           o FMor G (FMor F (HOM_l fxg) o h) o FMor G (Hom_r fxg)).
apply Comp_l; unfold FOb at 1 in |- *; simpl in |- *; unfold Comp_FOb in |- *;
 apply FComp.
(* *) apply
       Trans
        with
          ((A_eta ad (OB_l d2xc2) o FMor G (FMor F (HOM_l fxg) o h))
           o FMor G (Hom_r fxg)).
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@Comp C (@FOb C C (@Comp_Functor C D C G F) (@FOb D C F (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@FOb D C F (@OB_l C D dxc))) f)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@FOb D C F (@OB_l C D dxc)))) f) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@FOb D C F (@OB_l C D dxc)))) f) f *)
apply Ass.
(* Goal: @Equal (@Hom D (@FOb D D (Id_CAT D) (@OB_l C D d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@Comp D (@FOb D D (Id_CAT D) (@OB_l C D d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@FOb D D (Id_CAT D) (@OB_l C D d2xc2)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D d2xc2)) (@FMor C D G (@FOb D C F (@OB_l C D d2xc2)) (@Ob_r (Dual D) C d1xc1) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@OB_l C D d1xc1)) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@HOM_l C D d1xc1 d2xc2 fxg)) h))) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 fxg) (@Comp D (@Id_CAT_ob D (@OB_l C D d1xc1)) (@Comp_FOb D C D F G (@OB_l C D d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D d1xc1)) (@FMor C D G (@FOb D C F (@OB_l C D d1xc1)) (@Ob_r (Dual D) C d1xc1) h))) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) *)
apply Comp_r.
(* *) apply
       Trans
        with (A_eta ad (OB_l d2xc2) o FMor G (FMor F (HOM_l fxg)) o FMor G h).
(* Goal: @Equal (@Hom D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)))) (@Comp D (@Id_CAT_ob D (@OB_l C D dxc)) (@Comp_FOb D C D F G (@OB_l C D dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) (@Comp C (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Id_CAT_ob C (@Ob_r (Dual D) C dxc)) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) f) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))))) (@Comp D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc)) (@Comp D (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc)))) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) f)) (@FMor C D G (@FOb C C (@Comp_Functor C D C G F) (@Ob_r (Dual D) C dxc)) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))))) *)
(* Goal: @Equal (@Hom D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)))) (@Comp D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc)) (@Comp D (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc)))) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) f)) (@FMor C D G (@FOb C C (@Comp_Functor C D C G F) (@Ob_r (Dual D) C dxc)) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))))) f *)
(* Goal: forall x : Carrier (@FunSET2_r_ob C D F dxc), @Equal (@FunSET2_r_ob C D F dxc) (@Teta_1_arrow dxc (@Teta_arrow dxc x)) (@Id_fun (@FunSET2_r_ob C D F dxc) x) *)
apply Comp_l.
(* Goal: @Equal (@Hom D (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d1xc1))) (@FMor C D G (@FOb D C F (@OB_l C D d2xc2)) (@Ob_r (Dual D) C d1xc1) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@OB_l C D d1xc1)) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@HOM_l C D d1xc1 d2xc2 fxg)) h)) (@Comp D (@FOb C D G (@FOb D C F (@OB_l C D d2xc2))) (@FOb C D G (@FOb D C F (@OB_l C D d1xc1))) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FMor C D G (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@OB_l C D d1xc1)) (@FMor D C F (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@HOM_l C D d1xc1 d2xc2 fxg))) (@FMor C D G (@FOb D C F (@OB_l C D d1xc1)) (@Ob_r (Dual D) C d1xc1) h)) *)
(* Goal: @Equal (@Hom D (@FOb D D (Id_CAT D) (@OB_l C D d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d1xc1))) (@Comp D (@FOb D D (Id_CAT D) (@OB_l C D d2xc2)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D d2xc2)) (@Comp D (@FOb C D G (@FOb D C F (@OB_l C D d2xc2))) (@FOb C D G (@FOb D C F (@OB_l C D d1xc1))) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FMor C D G (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@OB_l C D d1xc1)) (@FMor D C F (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@HOM_l C D d1xc1 d2xc2 fxg))) (@FMor C D G (@FOb D C F (@OB_l C D d1xc1)) (@Ob_r (Dual D) C d1xc1) h))) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 fxg) (@Comp D (@Id_CAT_ob D (@OB_l C D d1xc1)) (@Comp_FOb D C D F G (@OB_l C D d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D d1xc1)) (@FMor C D G (@FOb D C F (@OB_l C D d1xc1)) (@Ob_r (Dual D) C d1xc1) h))) *)
unfold FOb at 1 in |- *; simpl in |- *; unfold Comp_FOb in |- *; apply FComp.
(* *) apply
       Trans
        with
          ((A_eta ad (OB_l d2xc2) o FMor G (FMor F (HOM_l fxg))) o FMor G h).
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@Comp C (@FOb C C (@Comp_Functor C D C G F) (@FOb D C F (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@FOb D C F (@OB_l C D dxc))) f)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@FOb D C F (@OB_l C D dxc)))) f) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@FOb D C F (@OB_l C D dxc)))) f) f *)
apply Ass.
(* Goal: @Equal (@Hom D (@FOb D D (Id_CAT D) (@OB_l C D d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d1xc1))) (@Comp D (@FOb D D (Id_CAT D) (@OB_l C D d2xc2)) (@FOb C D G (@FOb D C F (@OB_l C D d1xc1))) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp D (@FOb D D (Id_CAT D) (@OB_l C D d2xc2)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D d2xc2)) (@FOb C D G (@FOb D C F (@OB_l C D d1xc1))) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D d2xc2)) (@FMor C D G (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@OB_l C D d1xc1)) (@FMor D C F (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@HOM_l C D d1xc1 d2xc2 fxg)))) (@FMor C D G (@FOb D C F (@OB_l C D d1xc1)) (@Ob_r (Dual D) C d1xc1) h)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 fxg) (@Comp D (@Id_CAT_ob D (@OB_l C D d1xc1)) (@Comp_FOb D C D F G (@OB_l C D d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D d1xc1)) (@FMor C D G (@FOb D C F (@OB_l C D d1xc1)) (@Ob_r (Dual D) C d1xc1) h))) *)
(* *) apply Trans with ((HOM_l fxg o A_eta ad (OB_l d1xc1)) o FMor G h).
(* Goal: @Equal (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1))) (@Comp D (@FOb D D (Id_CAT D) (@OB_l C D d2xc2)) (@FOb C D G (@FOb D C F (@OB_l C D d1xc1))) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp D (@FOb D D (Id_CAT D) (@OB_l C D d2xc2)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D d2xc2)) (@FOb C D G (@FOb D C F (@OB_l C D d1xc1))) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D d2xc2)) (@FMor C D G (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@OB_l C D d1xc1)) (@FMor D C F (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@HOM_l C D d1xc1 d2xc2 fxg)))) (@FMor C D G (@FOb D C F (@OB_l C D d1xc1)) (@Ob_r (Dual D) C d1xc1) h)) (@Comp D (@OB_l C D d2xc2) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D d1xc1)) (@HOM_l C D d1xc1 d2xc2 fxg) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D d1xc1))) (@FMor C D G (@FOb D C F (@OB_l C D d1xc1)) (@Ob_r (Dual D) C d1xc1) h)) *)
(* Goal: @Equal (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1))) (@Comp D (@OB_l C D d2xc2) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D d1xc1)) (@HOM_l C D d1xc1 d2xc2 fxg) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D d1xc1))) (@FMor C D G (@FOb D C F (@OB_l C D d1xc1)) (@Ob_r (Dual D) C d1xc1) h)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 fxg) (@Comp D (@Id_CAT_ob D (@OB_l C D d1xc1)) (@Comp_FOb D C D F G (@OB_l C D d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D d1xc1)) (@FMor C D G (@FOb D C F (@OB_l C D d1xc1)) (@Ob_r (Dual D) C d1xc1) h))) *)
apply Comp_r; apply Sym.
(* Goal: @Equal (@Hom D (@OB_l C D d2xc2) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D d1xc1))) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D d1xc1)) (@HOM_l C D d1xc1 d2xc2 fxg) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D d1xc1))) (@Comp D (@FOb D D (Id_CAT D) (@OB_l C D d2xc2)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D d2xc2)) (@FOb C D G (@FOb D C F (@OB_l C D d1xc1))) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D d2xc2)) (@FMor C D G (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@OB_l C D d1xc1)) (@FMor D C F (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@HOM_l C D d1xc1 d2xc2 fxg)))) *)
(* Goal: @Equal (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1))) (@Comp D (@OB_l C D d2xc2) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D d1xc1)) (@HOM_l C D d1xc1 d2xc2 fxg) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D d1xc1))) (@FMor C D G (@FOb D C F (@OB_l C D d1xc1)) (@Ob_r (Dual D) C d1xc1) h)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 fxg) (@Comp D (@Id_CAT_ob D (@OB_l C D d1xc1)) (@Comp_FOb D C D F G (@OB_l C D d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D d1xc1)) (@FMor C D G (@FOb D C F (@OB_l C D d1xc1)) (@Ob_r (Dual D) C d1xc1) h))) *)
apply (Prf_NT_law (A_eta ad) (HOM_l fxg)).
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@FMor D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@Comp C (@FOb D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc)))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f)) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc)))) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@Comp C (@FOb D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc)))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f)) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc)))) f *)
apply Ass1.
Qed.

Canonical Structure Teta := Build_NT Teta_tau_NT_law.

(* Construisons maintenant Teta_1 *)

 Section teta_1_tau_def.

 Variable dxc : POb (Dual D) C.

 Definition Teta_1_arrow (g : OB_l dxc --> G (Ob_r dxc)) :=
   FMor F g o A_eps ad (Ob_r dxc).

 Lemma Teta_1_arrow_Map_law : Map_law Teta_1_arrow.
 Proof.
(* Goal: @Map_law (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Hom C (@FOb D C F (@OB_l C D dxc)) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) Teta_1_arrow *)
 unfold Map_law, Teta_1_arrow in |- *.
(* Goal: forall (x y : Carrier (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)))) (_ : @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) x y), @Equal (@Hom C (@FOb D C F (@OB_l C D dxc)) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) x) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) y) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))) *)
 intros f g H.
(* Goal: @Equal (@Hom C (@FOb D C F (@OB_l C D dxc)) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) f) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) g) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))) *)
 apply Comp_r; apply FPres; assumption.
 Qed.

 Canonical Structure Teta_1_tau := Build_Map Teta_1_arrow_Map_law.

 End teta_1_tau_def.

Lemma Teta_1_tau_NT_law : NT_law (F:=FunSET2_l G) (G:=FunSET2_r F) Teta_1_tau.
Proof.
(* Goal: @NT_law (PROD (Dual D) C) SET (@FunSET2_l C D G) (@FunSET2_r C D F) Teta_1_tau *)
unfold NT_law in |- *; simpl in |- *.
(* Goal: forall (a b : POb (Dual D) C) (f : @Pmor (Dual D) C a b), @Ext (@FunSET2_l_ob C D G a) (@FunSET2_r_ob C D F b) (@Comp SET (@FunSET2_l_ob C D G a) (@FunSET2_l_ob C D G b) (@FunSET2_r_ob C D F b) (@FMor (PROD (Dual D) C) SET (@FunSET2_l C D G) a b f) (Teta_1_tau b)) (@Comp SET (@FunSET2_l_ob C D G a) (@FunSET2_r_ob C D F a) (@FunSET2_r_ob C D F b) (Teta_1_tau a) (@FMor (PROD (Dual D) C) SET (@FunSET2_r C D F) a b f)) *)
unfold Ext in |- *; simpl in |- *.
(* Goal: forall (a b : POb (Dual D) C) (f : @Pmor (Dual D) C a b) (x : Carrier (@FunSET2_l_ob C D G a)), @Equal (@FunSET2_r_ob C D F b) (@Teta_1_arrow b (@FunSET2_l_mor1 C D G a b f x)) (@FunSET2_r_mor1 C D F a b f (@Teta_1_arrow a x)) *)
intros d1xc1 d2xc2 fxg h.
(* Goal: @Equal (@FunSET2_r_ob C D F d2xc2) (@Teta_1_arrow d2xc2 (@FunSET2_l_mor1 C D G d1xc1 d2xc2 fxg h)) (@FunSET2_r_mor1 C D F d1xc1 d2xc2 fxg (@Teta_1_arrow d1xc1 h)) *)
unfold Teta_1_arrow, FunSET2_r_mor1, FunSET2_l_mor1 in |- *.
(* Goal: @Equal (@FunSET2_r_ob C D F d2xc2) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C d2xc2)) (@FMor D C F (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 fxg) h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C d2xc2))) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@OB_l C D d1xc1)) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@HOM_l C D d1xc1 d2xc2 fxg)) (@Comp C (@FOb D C F (@OB_l C D d1xc1)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C d1xc1))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C d1xc1)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) h) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C d1xc1)))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
unfold FOb at 1 in |- *; simpl in |- *; unfold FunSET2_r_ob in |- *.
(* *) apply
       Trans
        with
          ((FMor F (HOM_l fxg o h) o FMor F (FMor G (Hom_r fxg)))
           o A_eps ad (Ob_r d2xc2)).
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@Comp C ((let (FOb, FMap, _, _) := F in FOb) (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Id_CAT_ob C (@Ob_r (Dual D) C dxc)) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Comp D (@Id_CAT_ob D (@OB_l C D dxc)) (@Comp_FOb D C D F G (@OB_l C D dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@FMor D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@FMor D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))) f *)
apply Comp_r; apply FComp.
(* *) apply
       Trans
        with
          (FMor F (HOM_l fxg o h)
           o FMor F (FMor G (Hom_r fxg)) o A_eps ad (Ob_r d2xc2)).
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@FMor D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@Comp C (@FOb D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc)))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f)) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc)))) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@Comp C (@FOb D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc)))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f)) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc)))) f *)
apply Ass1.
(* *) apply
       Trans
        with
          ((FMor F (HOM_l fxg) o FMor F h)
           o FMor F (FMor G (Hom_r fxg)) o A_eps ad (Ob_r d2xc2)).
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@Comp C ((let (FOb, FMap, _, _) := F in FOb) (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Id_CAT_ob C (@Ob_r (Dual D) C dxc)) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Comp D (@Id_CAT_ob D (@OB_l C D dxc)) (@Comp_FOb D C D F G (@OB_l C D dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@FMor D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@FMor D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))) f *)
apply Comp_r; apply FComp. 
(* *) apply
       Trans
        with
          (FMor F (HOM_l fxg)
           o FMor F h o FMor F (FMor G (Hom_r fxg)) o A_eps ad (Ob_r d2xc2)).
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@FMor D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@Comp C (@FOb D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc)))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f)) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc)))) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@Comp C (@FOb D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc)))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f)) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc)))) f *)
apply Ass1.
(* *) apply
       Trans
        with
          (FMor F (HOM_l fxg)
           o (FMor F h o A_eps ad (Ob_r d1xc1)) o Hom_r fxg).
(* Goal: @Equal (@Hom D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)))) (@Comp D (@Id_CAT_ob D (@OB_l C D dxc)) (@Comp_FOb D C D F G (@OB_l C D dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) (@Comp C (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Id_CAT_ob C (@Ob_r (Dual D) C dxc)) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) f) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))))) (@Comp D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc)) (@Comp D (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc)))) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) f)) (@FMor C D G (@FOb C C (@Comp_Functor C D C G F) (@Ob_r (Dual D) C dxc)) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))))) *)
(* Goal: @Equal (@Hom D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)))) (@Comp D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc)) (@Comp D (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc)))) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) f)) (@FMor C D G (@FOb C C (@Comp_Functor C D C G F) (@Ob_r (Dual D) C dxc)) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))))) f *)
(* Goal: forall x : Carrier (@FunSET2_r_ob C D F dxc), @Equal (@FunSET2_r_ob C D F dxc) (@Teta_1_arrow dxc (@Teta_arrow dxc x)) (@Id_fun (@FunSET2_r_ob C D F dxc) x) *)
apply Comp_l.
(* Goal: @Equal (@Hom C (@FOb D C F (@OB_l C D d1xc1)) (@Ob_r (Dual D) C d2xc2)) (@Comp C (@FOb D C F (@OB_l C D d1xc1)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C d1xc1))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C d2xc2)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C d2xc2)) (@FMor D C F (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C d2xc2)))) (@Comp C (@FOb D C F (@OB_l C D d1xc1)) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C d1xc1)) (@Ob_r (Dual D) C d2xc2) (@Comp C (@FOb D C F (@OB_l C D d1xc1)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C d1xc1))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C d1xc1)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) h) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C d1xc1))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@OB_l C D d2xc2)) (@Ob_r (Dual D) C d2xc2)) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@OB_l C D d1xc1)) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@HOM_l C D d1xc1 d2xc2 fxg)) (@Comp C (@FOb D C F (@OB_l C D d1xc1)) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C d1xc1)) (@Ob_r (Dual D) C d2xc2) (@Comp C (@FOb D C F (@OB_l C D d1xc1)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C d1xc1))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C d1xc1)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) h) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C d1xc1))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@OB_l C D d1xc1)) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@HOM_l C D d1xc1 d2xc2 fxg)) (@Comp C (@FOb D C F (@OB_l C D d1xc1)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C d1xc1))) (@Id_CAT_ob C (@Ob_r (Dual D) C d1xc1)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) h) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C d1xc1)))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
(* *) apply Trans with (FMor F h o A_eps ad (Ob_r d1xc1) o Hom_r fxg).
(* Goal: @Equal (@Hom C (@FOb D C F (@OB_l C D d1xc1)) (@Ob_r (Dual D) C d2xc2)) (@Comp C (@FOb D C F (@OB_l C D d1xc1)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C d1xc1))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C d2xc2)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C d2xc2)) (@FMor D C F (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C d2xc2)))) (@Comp C (@FOb D C F (@OB_l C D d1xc1)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb C C (@Comp_Functor C D C G F) (@Ob_r (Dual D) C d1xc1)) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C d1xc1)) (@Ob_r (Dual D) C d2xc2) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C d1xc1)) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@OB_l C D d1xc1)) (@Ob_r (Dual D) C d2xc2)) (@Comp C (@FOb D C F (@OB_l C D d1xc1)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb C C (@Comp_Functor C D C G F) (@Ob_r (Dual D) C d1xc1)) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C d1xc1)) (@Ob_r (Dual D) C d2xc2) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C d1xc1)) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@Comp C (@FOb D C F (@OB_l C D d1xc1)) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C d1xc1)) (@Ob_r (Dual D) C d2xc2) (@Comp C (@FOb D C F (@OB_l C D d1xc1)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C d1xc1))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C d1xc1)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) h) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C d1xc1))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@OB_l C D d2xc2)) (@Ob_r (Dual D) C d2xc2)) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@OB_l C D d1xc1)) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@HOM_l C D d1xc1 d2xc2 fxg)) (@Comp C (@FOb D C F (@OB_l C D d1xc1)) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C d1xc1)) (@Ob_r (Dual D) C d2xc2) (@Comp C (@FOb D C F (@OB_l C D d1xc1)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C d1xc1))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C d1xc1)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) h) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C d1xc1))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@OB_l C D d1xc1)) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@HOM_l C D d1xc1 d2xc2 fxg)) (@Comp C (@FOb D C F (@OB_l C D d1xc1)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C d1xc1))) (@Id_CAT_ob C (@Ob_r (Dual D) C d1xc1)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) h) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C d1xc1)))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply Comp_l; apply (Prf_NT_law (A_eps ad) (Hom_r fxg)).
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@Comp C (@FOb C C (@Comp_Functor C D C G F) (@FOb D C F (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@FOb D C F (@OB_l C D dxc))) f)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@FOb D C F (@OB_l C D dxc)))) f) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@FOb D C F (@OB_l C D dxc)))) f) f *)
apply Ass.
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@Comp C (@FOb C C (@Comp_Functor C D C G F) (@FOb D C F (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@FOb D C F (@OB_l C D dxc))) f)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@FOb D C F (@OB_l C D dxc)))) f) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@FOb D C F (@OB_l C D dxc)))) f) f *)
apply Ass.
Qed.

Canonical Structure Teta_1 := Build_NT Teta_1_tau_NT_law.

(* dem. que Teta et Teta_1 sont iso *)

(* a` prouver: eta(d) o G(Ff o eps(c)) = f *)
(* f o eta(Gc) o G(eps(c)) =f (car eta NT) *)
(* f o Id(Gc) = f                 (car C1)     *)

 Section teta_iso.

 Variable dxc : POb (Dual D) C.

 Lemma Teta_1_o_Teta : AreIsos (Teta dxc) (Teta_1 dxc).
 Proof.
 unfold AreIsos, RIso_law in |- *; split; simpl in |- *; unfold Ext in |- *;
  simpl in |- *.
(* Goal: forall x : Carrier (@FunSET2_l_ob C D G dxc), @Equal (@FunSET2_l_ob C D G dxc) (@Teta_arrow dxc (@Teta_1_arrow dxc x)) (@Id_fun (@FunSET2_l_ob C D G dxc) x) *)
(* Goal: forall x : Carrier (@FunSET2_r_ob C D F dxc), @Equal (@FunSET2_r_ob C D F dxc) (@Teta_1_arrow dxc (@Teta_arrow dxc x)) (@Id_fun (@FunSET2_r_ob C D F dxc) x) *)
 unfold Teta_arrow, Id_fun, Teta_1_arrow in |- *.
(* Goal: forall x : Carrier (@FunSET2_l_ob C D G dxc), @Equal (@FunSET2_l_ob C D G dxc) (@Comp D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) (@Comp C (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) x) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))))) x *)
(* Goal: forall x : Carrier (@FunSET2_r_ob C D F dxc), @Equal (@FunSET2_r_ob C D F dxc) (@Teta_1_arrow dxc (@Teta_arrow dxc x)) (@Id_fun (@FunSET2_r_ob C D F dxc) x) *)
 unfold FOb at 1 in |- *; simpl in |- *; unfold FunSET2_l_ob in |- *.
(* Goal: forall x : Carrier (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))), @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@Id_CAT_ob D (@OB_l C D dxc)) (@Comp_FOb D C D F G (@OB_l C D dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) (@Comp C (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Id_CAT_ob C (@Ob_r (Dual D) C dxc)) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) x) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))))) x *)
(* Goal: forall x : Carrier (@FunSET2_r_ob C D F dxc), @Equal (@FunSET2_r_ob C D F dxc) (@Teta_1_arrow dxc (@Teta_arrow dxc x)) (@Id_fun (@FunSET2_r_ob C D F dxc) x) *)
 intros f.
 (* *) apply
        Trans
         with
           (A_eta ad (OB_l dxc)
            o FMor G (FMor F f) o FMor G (A_eps ad (Ob_r dxc))).
(* Goal: @Equal (@Hom D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)))) (@Comp D (@Id_CAT_ob D (@OB_l C D dxc)) (@Comp_FOb D C D F G (@OB_l C D dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) (@Comp C (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Id_CAT_ob C (@Ob_r (Dual D) C dxc)) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) f) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))))) (@Comp D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc)) (@Comp D (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc)))) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) f)) (@FMor C D G (@FOb C C (@Comp_Functor C D C G F) (@Ob_r (Dual D) C dxc)) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))))) *)
(* Goal: @Equal (@Hom D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)))) (@Comp D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc)) (@Comp D (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc)))) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) f)) (@FMor C D G (@FOb C C (@Comp_Functor C D C G F) (@Ob_r (Dual D) C dxc)) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))))) f *)
(* Goal: forall x : Carrier (@FunSET2_r_ob C D F dxc), @Equal (@FunSET2_r_ob C D F dxc) (@Teta_1_arrow dxc (@Teta_arrow dxc x)) (@Id_fun (@FunSET2_r_ob C D F dxc) x) *)
 apply Comp_l.
 unfold Comp_Functor in |- *; simpl in |- *; unfold Comp_FOb in |- *;
  apply FComp.
 (* *) apply
        Trans
         with
           ((A_eta ad (OB_l dxc) o FMor G (FMor F f))
            o FMor G (A_eps ad (Ob_r dxc))).
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@Comp C (@FOb C C (@Comp_Functor C D C G F) (@FOb D C F (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@FOb D C F (@OB_l C D dxc))) f)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@FOb D C F (@OB_l C D dxc)))) f) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@FOb D C F (@OB_l C D dxc)))) f) f *)
 apply Ass.
 (* *) apply
        Trans
         with ((f o A_eta ad (G (Ob_r dxc))) o FMor G (A_eps ad (Ob_r dxc))).
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)))) (@Comp D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb C D G (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc)))) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@Comp D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@FOb C D G (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc)))) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) f))) (@FMor C D G (@FOb C C (@Comp_Functor C D C G F) (@Ob_r (Dual D) C dxc)) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc)))) (@Comp D (@OB_l C D dxc) (@FOb D D (@Comp_Functor D C D F G) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb D D (@Comp_Functor D C D F G) (@FOb C D G (@Ob_r (Dual D) C dxc))) f (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@FOb C D G (@Ob_r (Dual D) C dxc)))) (@FMor C D G (@FOb C C (@Comp_Functor C D C G F) (@Ob_r (Dual D) C dxc)) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc)))) *)
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)))) (@Comp D (@OB_l C D dxc) (@FOb D D (@Comp_Functor D C D F G) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb D D (@Comp_Functor D C D F G) (@FOb C D G (@Ob_r (Dual D) C dxc))) f (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@FOb C D G (@Ob_r (Dual D) C dxc)))) (@FMor C D G (@FOb C C (@Comp_Functor C D C G F) (@Ob_r (Dual D) C dxc)) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc)))) f *)
(* Goal: forall x : Carrier (@FunSET2_r_ob C D F dxc), @Equal (@FunSET2_r_ob C D F dxc) (@Teta_1_arrow dxc (@Teta_arrow dxc x)) (@Id_fun (@FunSET2_r_ob C D F dxc) x) *)
 apply Comp_r; apply Sym; apply (Prf_NT_law (A_eta ad) f).
 (* *) apply
        Trans
         with (f o A_eta ad (G (Ob_r dxc)) o FMor G (A_eps ad (Ob_r dxc))).
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@FMor D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@Comp C (@FOb D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc)))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f)) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc)))) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@Comp C (@FOb D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc)))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f)) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc)))) f *)
 apply Ass1.
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)))) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) f (@Comp D (@FOb D D (Id_CAT D) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb D D (@Comp_Functor D C D F G) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FMor C D G (@FOb C C (@Comp_Functor C D C G F) (@Ob_r (Dual D) C dxc)) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))))) f *)
(* Goal: forall x : Carrier (@FunSET2_r_ob C D F dxc), @Equal (@FunSET2_r_ob C D F dxc) (@Teta_1_arrow dxc (@Teta_arrow dxc x)) (@Id_fun (@FunSET2_r_ob C D F dxc) x) *)
 (* *) apply Trans with (f o Id (G (Ob_r dxc))).
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) f (@Comp D (@FOb D D (Id_CAT D) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb D D (@Comp_Functor D C D F G) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C D G (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FMor C D G (@FOb C C (@Comp_Functor C D C G F) (@Ob_r (Dual D) C dxc)) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))))) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) f (@Id D (@FOb C D G (@Ob_r (Dual D) C dxc)))) *)
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) f (@Id D (@FOb C D G (@Ob_r (Dual D) C dxc)))) f *)
(* Goal: forall x : Carrier (@FunSET2_r_ob C D F dxc), @Equal (@FunSET2_r_ob C D F dxc) (@Teta_1_arrow dxc (@Teta_arrow dxc x)) (@Id_fun (@FunSET2_r_ob C D F dxc) x) *)
 apply Comp_l; apply (Prf_Adj1_law1 ad (Ob_r dxc)).
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) f (@Id D (@FOb C D G (@Ob_r (Dual D) C dxc)))) f *)
(* Goal: forall x : Carrier (@FunSET2_r_ob C D F dxc), @Equal (@FunSET2_r_ob C D F dxc) (@Teta_1_arrow dxc (@Teta_arrow dxc x)) (@Id_fun (@FunSET2_r_ob C D F dxc) x) *)
 apply Idr1.
 (**)
(* Goal: forall x : Carrier (@FunSET2_r_ob C D F dxc), @Equal (@FunSET2_r_ob C D F dxc) (@Teta_1_arrow dxc (@Teta_arrow dxc x)) (@Id_fun (@FunSET2_r_ob C D F dxc) x) *)
 unfold Teta_1_arrow, Teta_arrow, Id_fun in |- *.
(* Goal: forall x : Carrier (@FunSET2_r_ob C D F dxc), @Equal (@FunSET2_r_ob C D F dxc) (@Comp C (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Comp D (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) x))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))) x *)
 unfold FOb at 1 in |- *; simpl in |- *; unfold FunSET2_r_ob in |- *; intro f.
 (* *) apply
        Trans
         with
           ((FMor F (A_eta ad (OB_l dxc)) o FMor F (FMor G f))
            o A_eps ad (Ob_r dxc)).
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@Comp C ((let (FOb, FMap, _, _) := F in FOb) (@OB_l C D dxc)) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Id_CAT_ob C (@Ob_r (Dual D) C dxc)) (@FMor D C F (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Comp D (@Id_CAT_ob D (@OB_l C D dxc)) (@Comp_FOb D C D F G (@OB_l C D dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@FMor D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@FMor D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))) f *)
 apply Comp_r; apply FComp.
 (* *) apply
        Trans
         with
           (FMor F (A_eta ad (OB_l dxc))
            o FMor F (FMor G f) o A_eps ad (Ob_r dxc)).
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@FMor D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@Comp C (@FOb D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc)))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f)) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc)))) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc))) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@Comp C (@FOb D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc)))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f)) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc)))) f *)
 apply Ass1.
 (* *) apply
        Trans
         with (FMor F (A_eta ad (OB_l dxc)) o A_eps ad (F (OB_l dxc)) o f).
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@Comp C (@FOb D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc)))) (@FOb D C F (@FOb C D G (@Ob_r (Dual D) C dxc))) (@FOb C C (Id_CAT C) (@Ob_r (Dual D) C dxc)) (@FMor D C F (@FOb C D G (@FOb D C F (@OB_l C D dxc))) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FMor C D G (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) f)) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@Ob_r (Dual D) C dxc)))) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@Comp C (@FOb C C (@Comp_Functor C D C G F) (@FOb D C F (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@FOb D C F (@OB_l C D dxc))) f)) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@Comp C (@FOb C C (@Comp_Functor C D C G F) (@FOb D C F (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@FOb D C F (@OB_l C D dxc))) f)) f *)
 apply Comp_l; apply (Prf_NT_law (A_eps ad) f).
 (* *) apply
        Trans
         with ((FMor F (A_eta ad (OB_l dxc)) o A_eps ad (F (OB_l dxc))) o f).
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@Comp C (@FOb C C (@Comp_Functor C D C G F) (@FOb D C F (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@FOb D C F (@OB_l C D dxc))) f)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@FOb D C F (@OB_l C D dxc)))) f) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@FOb D C F (@OB_l C D dxc)))) f) f *)
 apply Ass.
(* Goal: @Equal (@Hom C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@FOb D C F (@OB_l C D dxc)))) f) f *)
 (* *) apply Trans with (Id (F (OB_l dxc)) o f).
(* Goal: @Equal (@Hom C (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@Ob_r (Dual D) C dxc) (@Comp C (@FOb D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc))) (@FOb D C F (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc))) (@FOb C C (Id_CAT C) (@FOb D C F (@OB_l C D dxc))) (@FMor D C F (@FOb D D (Id_CAT D) (@OB_l C D dxc)) (@FOb D D (@Comp_Functor D C D F G) (@OB_l C D dxc)) (@ApNT D D (Id_CAT D) (@Comp_Functor D C D F G) (@A_eta C D F G ad) (@OB_l C D dxc))) (@ApNT C C (@Comp_Functor C D C G F) (Id_CAT C) (@A_eps C D F G ad) (@FOb D C F (@OB_l C D dxc)))) f) (@Comp C (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) (@Id C (@FOb D C F (@OB_l C D dxc))) f) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) (@Id C (@FOb D C F (@OB_l C D dxc))) f) f *)
 apply Comp_r; apply (Prf_Adj1_law2 ad (OB_l dxc)).
(* Goal: @Equal (@Hom C (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc) (@Id C (@FOb D C F (@OB_l C D dxc))) f) f *)
 apply Idl.
 Qed.

 End teta_iso.

Definition Adj1_to_Adj := Build_Adj (NT_Iso Teta_1_o_Teta).

End adj1_to_adj.
 
Coercion Adj1_to_Adj : Adj1 >-> Adj.

(* Les deux defs sont e'quivalentes: a faire *)

Section adj_equiv.

Variables (C D : Category) (F : Functor D C) (G : Functor C D).

Definition Eq_Adj (ad ad' : Adj F G) := ad =_NT ad'.

Definition Eq_Adj1 (ad ad' : Adj1 F G) :=
  A_eta ad =_NT A_eta ad' /\ A_eps ad =_NT A_eps ad'.

End adj_equiv.

