(* 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        *)
(*****************************************************************************)
(*									     *)
(*	            Existence of Right Adjoint                		     *)
(*									     *)
(*****************************************************************************)
(*									     *)
(*                     A. SAIBI	  May 95                  		     *)
(*									     *)
(*****************************************************************************)

Require Export Adj_UA. 

Set Implicit Arguments.
Unset Strict Implicit.

Section ua_to_radj.

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

Hypothesis UA_of : forall c : C, CoUA c F.

(* construction de l'adj droit *)

Definition CoadjointUA_ob (c : C) := CoUA_ob (UA_of c).
 
 Section coadjoint_ua_map_def.

 Variable c c' : C.

 Definition CoadjointUA_mor (f : c --> c') :=
   CoUA_diese (UA_of c') (CoUA_mor (UA_of c) o f).

 Lemma CoadjointUA_map_law : Map_law CoadjointUA_mor.
 Proof.
(* Goal: @Map_law (@Hom C c c') (@Hom D (@CoUA_ob D C c F (UA_of c)) (@CoUA_ob D C c' F (UA_of c'))) CoadjointUA_mor *)
 unfold Map_law, CoadjointUA_mor in |- *; intros f g H.
 apply
  (Codiese_map (UA_of c') (x:=CoUA_mor (UA_of c) o f)
     (y:=CoUA_mor (UA_of c) o g)).
(* Goal: @Equal (@Hom C (@FOb D C F (@CoUA_ob D C c F (UA_of c))) c') (@Comp C (@FOb D C F (@CoUA_ob D C c F (UA_of c))) c c' (@CoUA_mor D C c F (UA_of c)) f) (@Comp C (@FOb D C F (@CoUA_ob D C c F (UA_of c))) c c' (@CoUA_mor D C c F (UA_of c)) g) *)
 apply Comp_l; assumption.
 Qed.

 Canonical Structure CoadjointUA_map :
   Map (c --> c') (CoadjointUA_ob c --> CoadjointUA_ob c') :=
   CoadjointUA_map_law.

 End coadjoint_ua_map_def.

Lemma CoadjointUA_id_law : Fid_law CoadjointUA_map.
Proof.
(* Goal: @Fid_law C D CoadjointUA_ob CoadjointUA_map *)
unfold Fid_law in |- *; simpl in |- *.
(* Goal: forall a : Ob C, @Equal (@Hom D (CoadjointUA_ob a) (CoadjointUA_ob a)) (@CoadjointUA_mor a a (@Id C a)) (@Id D (CoadjointUA_ob a)) *)
unfold CoadjointUA_mor, CoadjointUA_ob in |- *.
(* Goal: forall a : Ob C, @Equal (@Hom D (@CoUA_ob D C a F (UA_of a)) (@CoUA_ob D C a F (UA_of a))) (@CoUA_diese D C a F (@CoUA_ob D C a F (UA_of a)) (@CoUA_mor D C a F (UA_of a)) (@Prf_IsCoUA D C a F (UA_of a)) (@CoUA_ob D C a F (UA_of a)) (@Comp C (@FOb D C F (@CoUA_ob D C a F (UA_of a))) a a (@CoUA_mor D C a F (UA_of a)) (@Id C a))) (@Id D (@CoUA_ob D C a F (UA_of a))) *)
intro c.
(* Goal: @Equal (@Hom D (@OB_l C D d2xc2) (@CoUA_ob D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2)))) (@CoUA_diese D C (@Ob_r (Dual D) C d2xc2) F (@CoUA_ob D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))) (@Prf_IsCoUA D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))) (@Ob_l (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)) h) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@Comp D (@OB_l C D d2xc2) (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@CoUA_ob D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@HOM_l C D d1xc1 d2xc2 fxg) (@CoUA_diese D C (@Ob_r (Dual D) C d1xc1) F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@Prf_IsCoUA D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@Ob_l (Dual D) C d1xc1) h)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) *)
apply CoUA_unic1.
(* Goal: @Equal (@Hom C (@FOb D C F (@CoUA_ob D C c F (UA_of c))) c) (@Comp C (@FOb D C F (@CoUA_ob D C c F (UA_of c))) (@FOb D C F (@CoUA_ob D C c F (UA_of c))) c (@FMor D C F (@CoUA_ob D C c F (UA_of c)) (@CoUA_ob D C c F (UA_of c)) (@Id D (@CoUA_ob D C c F (UA_of c)))) (@CoUA_mor D C c F (UA_of c))) (@Comp C (@FOb D C F (@CoUA_ob D C c F (UA_of c))) c c (@CoUA_mor D C c F (UA_of c)) (@Id C c)) *)
(* *) apply Trans with (Id (F (CoUA_ob (UA_of c))) o CoUA_mor (UA_of c)).
(* Goal: @Equal (@Hom C (@FOb D C F (@CoUA_ob D C c F (UA_of c))) c) (@Comp C (@FOb D C F (@CoUA_ob D C c F (UA_of c))) (@FOb D C F (@CoUA_ob D C c F (UA_of c))) c (@FMor D C F (@CoUA_ob D C c F (UA_of c)) (@CoUA_ob D C c F (UA_of c)) (@Id D (@CoUA_ob D C c F (UA_of c)))) (@CoUA_mor D C c F (UA_of c))) (@Comp C (@FOb D C F (@CoUA_ob D C c F (UA_of c))) (@FOb D C F (@CoUA_ob D C c F (UA_of c))) c (@Id C (@FOb D C F (@CoUA_ob D C c F (UA_of c)))) (@CoUA_mor D C c F (UA_of c))) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@CoUA_ob D C c F (UA_of c))) c) (@Comp C (@FOb D C F (@CoUA_ob D C c F (UA_of c))) (@FOb D C F (@CoUA_ob D C c F (UA_of c))) c (@Id C (@FOb D C F (@CoUA_ob D C c F (UA_of c)))) (@CoUA_mor D C c F (UA_of c))) (@Comp C (@FOb D C F (@CoUA_ob D C c F (UA_of c))) c c (@CoUA_mor D C c F (UA_of c)) (@Id C c)) *)
apply Comp_r; apply FId.
(* Goal: @Equal (@Hom C (@FOb D C F (@CoUA_ob D C c F (UA_of c))) c) (@Comp C (@FOb D C F (@CoUA_ob D C c F (UA_of c))) (@FOb D C F (@CoUA_ob D C c F (UA_of c))) c (@Id C (@FOb D C F (@CoUA_ob D C c F (UA_of c)))) (@CoUA_mor D C c F (UA_of c))) (@Comp C (@FOb D C F (@CoUA_ob D C c F (UA_of c))) c c (@CoUA_mor D C c F (UA_of c)) (@Id C c)) *)
(* *) apply Trans with (CoUA_mor (UA_of c)).
(* Goal: @Equal (@Hom C (@FOb D C F (@CoUA_ob D C c F (UA_of c))) c) (@Comp C (@FOb D C F (@CoUA_ob D C c F (UA_of c))) (@FOb D C F (@CoUA_ob D C c F (UA_of c))) c (@Id C (@FOb D C F (@CoUA_ob D C c F (UA_of c)))) (@CoUA_mor D C c F (UA_of c))) (@CoUA_mor D C c F (UA_of c)) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@CoUA_ob D C c F (UA_of c))) c) (@CoUA_mor D C c F (UA_of c)) (@Comp C (@FOb D C F (@CoUA_ob D C c F (UA_of c))) c c (@CoUA_mor D C c F (UA_of c)) (@Id C c)) *)
apply Idl.
(* Goal: @Equal (@Hom C (@FOb D C F (@CoUA_ob D C c F (UA_of c))) c) (@CoUA_mor D C c F (UA_of c)) (@Comp C (@FOb D C F (@CoUA_ob D C c F (UA_of c))) c c (@CoUA_mor D C c F (UA_of c)) (@Id C c)) *)
apply Idr.
Qed.

Lemma CoadjointUA_comp_law : Fcomp_law CoadjointUA_map.
Proof.
(* Goal: @Fcomp_law C D CoadjointUA_ob CoadjointUA_map *)
unfold Fcomp_law in |- *; simpl in |- *.
(* Goal: forall (a b c : Ob C) (f : Carrier (@Hom C a b)) (g : Carrier (@Hom C b c)), @Equal (@Hom D (CoadjointUA_ob a) (CoadjointUA_ob c)) (@CoadjointUA_mor a c (@Comp C a b c f g)) (@Comp D (CoadjointUA_ob a) (CoadjointUA_ob b) (CoadjointUA_ob c) (@CoadjointUA_mor a b f) (@CoadjointUA_mor b c g)) *)
unfold CoadjointUA_mor, CoadjointUA_ob in |- *; intros c1 c2 c3 f g.
(* Goal: @Equal (@Hom D (@OB_l C D d2xc2) (@CoUA_ob D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2)))) (@CoUA_diese D C (@Ob_r (Dual D) C d2xc2) F (@CoUA_ob D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))) (@Prf_IsCoUA D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))) (@Ob_l (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)) h) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@Comp D (@OB_l C D d2xc2) (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@CoUA_ob D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@HOM_l C D d1xc1 d2xc2 fxg) (@CoUA_diese D C (@Ob_r (Dual D) C d1xc1) F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@Prf_IsCoUA D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@Ob_l (Dual D) C d1xc1) h)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) *)
apply CoUA_unic1.
(* *) apply
       Trans
        with
          ((FMor F (CoUA_diese (UA_of c2) (CoUA_mor (UA_of c1) o f))
            o FMor F (CoUA_diese (UA_of c3) (CoUA_mor (UA_of c2) o g)))
           o CoUA_mor (UA_of c3)).
(* Goal: @Equal (@Hom C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)))) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@FMor D C F (@OB_l C D d2xc2) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 fxg) h)) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)))) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h)) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@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 (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h)) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply Comp_r; apply FComp.
(* *) apply
       Trans
        with
          (FMor F (CoUA_diese (UA_of c2) (CoUA_mor (UA_of c1) o f))
           o FMor F (CoUA_diese (UA_of c3) (CoUA_mor (UA_of c2) o g))
             o CoUA_mor (UA_of c3)).
(* 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 (@FOb C D CoadjointUA (@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)) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h)) (@Comp C (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@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 D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2)))))) *)
(* 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 D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply Ass1.
(* *) apply
       Trans
        with
          (FMor F (CoUA_diese (UA_of c2) (CoUA_mor (UA_of c1) o f))
           o CoUA_mor (UA_of c2) o g).
(* Goal: @Equal (@Hom C (@FOb D C F (@CoUA_ob D C c1 F (UA_of c1))) c3) (@Comp C (@FOb D C F (@CoUA_ob D C c1 F (UA_of c1))) (@FOb D C F (@CoUA_ob D C c2 F (UA_of c2))) c3 (@FMor D C F (@CoUA_ob D C c1 F (UA_of c1)) (@CoUA_ob D C c2 F (UA_of c2)) (@CoUA_diese D C c2 F (@CoUA_ob D C c2 F (UA_of c2)) (@CoUA_mor D C c2 F (UA_of c2)) (@Prf_IsCoUA D C c2 F (UA_of c2)) (@CoUA_ob D C c1 F (UA_of c1)) (@Comp C (@FOb D C F (@CoUA_ob D C c1 F (UA_of c1))) c1 c2 (@CoUA_mor D C c1 F (UA_of c1)) f))) (@Comp C (@FOb D C F (@CoUA_ob D C c2 F (UA_of c2))) (@FOb D C F (@CoUA_ob D C c3 F (UA_of c3))) c3 (@FMor D C F (@CoUA_ob D C c2 F (UA_of c2)) (@CoUA_ob D C c3 F (UA_of c3)) (@CoUA_diese D C c3 F (@CoUA_ob D C c3 F (UA_of c3)) (@CoUA_mor D C c3 F (UA_of c3)) (@Prf_IsCoUA D C c3 F (UA_of c3)) (@CoUA_ob D C c2 F (UA_of c2)) (@Comp C (@FOb D C F (@CoUA_ob D C c2 F (UA_of c2))) c2 c3 (@CoUA_mor D C c2 F (UA_of c2)) g))) (@CoUA_mor D C c3 F (UA_of c3)))) (@Comp C (@FOb D C F (@CoUA_ob D C c1 F (UA_of c1))) (@FOb D C F (@CoUA_ob D C c2 F (UA_of c2))) c3 (@FMor D C F (@CoUA_ob D C c1 F (UA_of c1)) (@CoUA_ob D C c2 F (UA_of c2)) (@CoUA_diese D C c2 F (@CoUA_ob D C c2 F (UA_of c2)) (@CoUA_mor D C c2 F (UA_of c2)) (@Prf_IsCoUA D C c2 F (UA_of c2)) (@CoUA_ob D C c1 F (UA_of c1)) (@Comp C (@FOb D C F (@CoUA_ob D C c1 F (UA_of c1))) c1 c2 (@CoUA_mor D C c1 F (UA_of c1)) f))) (@Comp C (@FOb D C F (@CoUA_ob D C c2 F (UA_of c2))) c2 c3 (@CoUA_mor D C c2 F (UA_of c2)) g)) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@CoUA_ob D C c1 F (UA_of c1))) c3) (@Comp C (@FOb D C F (@CoUA_ob D C c1 F (UA_of c1))) (@FOb D C F (@CoUA_ob D C c2 F (UA_of c2))) c3 (@FMor D C F (@CoUA_ob D C c1 F (UA_of c1)) (@CoUA_ob D C c2 F (UA_of c2)) (@CoUA_diese D C c2 F (@CoUA_ob D C c2 F (UA_of c2)) (@CoUA_mor D C c2 F (UA_of c2)) (@Prf_IsCoUA D C c2 F (UA_of c2)) (@CoUA_ob D C c1 F (UA_of c1)) (@Comp C (@FOb D C F (@CoUA_ob D C c1 F (UA_of c1))) c1 c2 (@CoUA_mor D C c1 F (UA_of c1)) f))) (@Comp C (@FOb D C F (@CoUA_ob D C c2 F (UA_of c2))) c2 c3 (@CoUA_mor D C c2 F (UA_of c2)) g)) (@Comp C (@FOb D C F (@CoUA_ob D C c1 F (UA_of c1))) c1 c3 (@CoUA_mor D C c1 F (UA_of c1)) (@Comp C c1 c2 c3 f g)) *)
apply Comp_l; apply CoUA_diag.

(* *) apply
       Trans
        with
          ((FMor F (CoUA_diese (UA_of c2) (CoUA_mor (UA_of c1) o f))
            o CoUA_mor (UA_of c2)) o g).
(* 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)) (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply Ass.

(* Goal: @Equal (@Hom C (@FOb D C F (@CoUA_ob D C c1 F (UA_of c1))) c3) (@Comp C (@FOb D C F (@CoUA_ob D C c1 F (UA_of c1))) c2 c3 (@Comp C (@FOb D C F (@CoUA_ob D C c1 F (UA_of c1))) (@FOb D C F (@CoUA_ob D C c2 F (UA_of c2))) c2 (@FMor D C F (@CoUA_ob D C c1 F (UA_of c1)) (@CoUA_ob D C c2 F (UA_of c2)) (@CoUA_diese D C c2 F (@CoUA_ob D C c2 F (UA_of c2)) (@CoUA_mor D C c2 F (UA_of c2)) (@Prf_IsCoUA D C c2 F (UA_of c2)) (@CoUA_ob D C c1 F (UA_of c1)) (@Comp C (@FOb D C F (@CoUA_ob D C c1 F (UA_of c1))) c1 c2 (@CoUA_mor D C c1 F (UA_of c1)) f))) (@CoUA_mor D C c2 F (UA_of c2))) g) (@Comp C (@FOb D C F (@CoUA_ob D C c1 F (UA_of c1))) c1 c3 (@CoUA_mor D C c1 F (UA_of c1)) (@Comp C c1 c2 c3 f g)) *)
(* *) apply Trans with ((CoUA_mor (UA_of c1) o f) o g).
(* 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)) (@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 (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1)))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@CoUA_diese D C (@Ob_r (Dual D) C d1xc1) F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@Prf_IsCoUA D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@OB_l C D d1xc1) h)) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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)) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) h (@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)) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) h (@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)) h) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply Comp_r; apply CoUA_diag.
(* 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 (@FOb C D CoadjointUA (@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)) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h)) (@Comp C (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@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 D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2)))))) *)
(* 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 D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply Ass1.
Qed.

Canonical Structure CoadjointUA :=
  Build_Functor CoadjointUA_comp_law CoadjointUA_id_law.

(* *)

(* definition de PhiUA':C(F-,-) -> D(-,G-) *)

 Section psi_ua_tau_def.

 Variable dxc : POb (Dual D) C.

 Definition PsiUA_arrow (f : F (Ob_l dxc) --> Ob_r dxc) :=
   CoUA_diese (UA_of (Ob_r dxc)) f.

 Lemma PsiUA_arrow_map_law : Map_law PsiUA_arrow.
 Proof.
(* Goal: @Map_law (@Hom C (@FOb D C F (@Ob_l (Dual D) C dxc)) (@Ob_r (Dual D) C dxc)) (@Hom D (@Ob_l (Dual D) C dxc) (@CoUA_ob D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc)))) PsiUA_arrow *)
 unfold Map_law, PsiUA_arrow in |- *.
(* Goal: forall (x y : Carrier (@Hom D (@OB_l C D dxc) (@FOb C D CoadjointUA (@Ob_r (Dual D) C dxc)))) (_ : @Equal (@Hom D (@OB_l C D dxc) (@FOb C D CoadjointUA (@Ob_r (Dual D) C dxc))) x y), @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 (@FOb C D CoadjointUA (@Ob_r (Dual D) C dxc))) (@Ob_r (Dual D) C dxc) (@FMor D C F (@OB_l C D dxc) (@FOb C D CoadjointUA (@Ob_r (Dual D) C dxc)) x) (@CoUA_mor D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc)))) (@Comp C (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C dxc))) (@Ob_r (Dual D) C dxc) (@FMor D C F (@OB_l C D dxc) (@FOb C D CoadjointUA (@Ob_r (Dual D) C dxc)) y) (@CoUA_mor D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc)))) *)
 intros f g H.
(* Goal: @Equal (@Hom D (@Ob_l (Dual D) C dxc) (@CoUA_ob D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc)))) (@CoUA_diese D C (@Ob_r (Dual D) C dxc) F (@CoUA_ob D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc))) (@CoUA_mor D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc))) (@Prf_IsCoUA D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc))) (@Ob_l (Dual D) C dxc) f) (@CoUA_diese D C (@Ob_r (Dual D) C dxc) F (@CoUA_ob D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc))) (@CoUA_mor D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc))) (@Prf_IsCoUA D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc))) (@Ob_l (Dual D) C dxc) g) *)
 apply (Codiese_map (UA_of (Ob_r dxc)) (x:=f) (y:=g)).
(* Goal: @Equal (@Hom C (@FOb D C F (@Ob_l (Dual D) C dxc)) (@Ob_r (Dual D) C dxc)) f g *)
 assumption.
 Qed.

 Canonical Structure PsiUA_tau := Build_Map PsiUA_arrow_map_law.

 End psi_ua_tau_def.

Lemma PsiUA_tau_nt_law :
 NT_law (F:=FunSET2_r F) (G:=FunSET2_l CoadjointUA) PsiUA_tau.
Proof.
(* Goal: @NT_law (PROD (Dual D) C) SET (@FunSET2_r C D F) (@FunSET2_l C D CoadjointUA) PsiUA_tau *)
unfold NT_law, PsiUA_tau, PsiUA_arrow in |- *; simpl in |- *.
(* Goal: @Ext (@FunSET2_r_ob C D F dxc) (@FunSET2_r_ob C D F dxc) (@Comp SET (@FunSET2_r_ob C D F dxc) (@FunSET2_l_ob C D CoadjointUA dxc) (@FunSET2_r_ob C D F dxc) (PsiUA_tau dxc) (PsiUA_1_tau dxc)) (Id_SET (@FunSET2_r_ob C D F dxc)) *)
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 CoadjointUA a)), @Equal (@FunSET2_r_ob C D F b) (@Comp C (@FOb D C F (@OB_l C D b)) (@FOb D C F (CoadjointUA_ob (@Ob_r (Dual D) C b))) (@Ob_r (Dual D) C b) (@FMor D C F (@OB_l C D b) (CoadjointUA_ob (@Ob_r (Dual D) C b)) (@FunSET2_l_mor1 C D CoadjointUA a b f x)) (@CoUA_mor D C (@Ob_r (Dual D) C b) F (UA_of (@Ob_r (Dual D) C b)))) (@FunSET2_r_mor1 C D F a b f (@Comp C (@FOb D C F (@OB_l C D a)) (@FOb D C F (CoadjointUA_ob (@Ob_r (Dual D) C a))) (@Ob_r (Dual D) C a) (@FMor D C F (@OB_l C D a) (CoadjointUA_ob (@Ob_r (Dual D) C a)) x) (@CoUA_mor D C (@Ob_r (Dual D) C a) F (UA_of (@Ob_r (Dual D) C a))))) *)
intros d1xc1 d2xc2 fxg h.
unfold FunSET2_r_mor1, FunSET2_l_mor1, FunSET2_l_ob in |- *; simpl in |- *;
 unfold CoadjointUA_ob in |- *.
(* Goal: @Equal (@Hom D (@OB_l C D d2xc2) (@CoUA_ob D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2)))) (@CoUA_diese D C (@Ob_r (Dual D) C d2xc2) F (@CoUA_ob D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))) (@Prf_IsCoUA D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))) (@Ob_l (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)) h) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@Comp D (@OB_l C D d2xc2) (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@CoUA_ob D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@HOM_l C D d1xc1 d2xc2 fxg) (@CoUA_diese D C (@Ob_r (Dual D) C d1xc1) F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@Prf_IsCoUA D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@Ob_l (Dual D) C d1xc1) h)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) *)
apply CoUA_unic1.
(* *) apply
       Trans
        with
          ((FMor F (HOM_l fxg o CoUA_diese (UA_of (Ob_r d1xc1)) h)
            o FMor F (FMor CoadjointUA (Hom_r fxg)))
           o CoUA_mor (UA_of (Ob_r d2xc2))).
(* Goal: @Equal (@Hom C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)))) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@FMor D C F (@OB_l C D d2xc2) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 fxg) h)) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)))) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h)) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@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 (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h)) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply Comp_r; apply FComp.
(* *) apply
       Trans
        with
          (((FMor F (HOM_l fxg) o FMor F (CoUA_diese (UA_of (Ob_r d1xc1)) h))
            o FMor F (FMor CoadjointUA (Hom_r fxg)))
           o CoUA_mor (UA_of (Ob_r d2xc2))).
(* Goal: @Equal (@Hom C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)))) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@FMor D C F (@OB_l C D d2xc2) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 fxg) h)) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)))) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h)) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@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 (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h)) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply Comp_r; apply Comp_r; apply FComp.
(* *) apply
       Trans
        with
          ((FMor F (HOM_l fxg) o FMor F (CoUA_diese (UA_of (Ob_r d1xc1)) h))
           o FMor F (FMor CoadjointUA (Hom_r fxg))
             o CoUA_mor (UA_of (Ob_r d2xc2))).
(* 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 (@FOb C D CoadjointUA (@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)) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h)) (@Comp C (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@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 D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2)))))) *)
(* 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 D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply Ass1.
(* *) apply
       Trans
        with
          (FMor F (HOM_l fxg)
           o FMor F (CoUA_diese (UA_of (Ob_r d1xc1)) h)
             o FMor F (FMor CoadjointUA (Hom_r fxg))
               o CoUA_mor (UA_of (Ob_r d2xc2))).
(* 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 (@FOb C D CoadjointUA (@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)) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h)) (@Comp C (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@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 D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2)))))) *)
(* 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 D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply Ass1.
(* 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 D C F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1)))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@CoUA_diese D C (@Ob_r (Dual D) C d1xc1) F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@Prf_IsCoUA D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@OB_l C D d1xc1) h)) (@Comp C (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@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)) h) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
(* *) apply Trans with (FMor F (HOM_l fxg) o h 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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))))) (@Comp C (@FOb D C F (@OB_l C D d1xc1)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1)))) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1)))) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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)) (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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)) (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply Comp_l.
(* *) apply
       Trans
        with
          (FMor F (CoUA_diese (UA_of (Ob_r d1xc1)) h)
           o CoUA_mor (UA_of (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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))))) (@Comp C (@FOb D C F (@OB_l C D d1xc1)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1)))) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1)))) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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)) (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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)) (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply Comp_l.
unfold FMor at 2 in |- *; simpl in |- *;
(* Goal: forall a : Ob C, @Equal (@Hom D (CoadjointUA_ob a) (CoadjointUA_ob a)) (@CoadjointUA_mor a a (@Id C a)) (@Id D (CoadjointUA_ob a)) *)
 unfold CoadjointUA_mor, CoadjointUA_ob in |- *.
(* Goal: @Equal (@Hom C (@FOb D C F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1)))) (@Ob_r (Dual D) C d2xc2)) (@Comp C (@FOb D C F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1)))) (@FOb D C F (@CoUA_ob D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2)))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@CoUA_ob D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))) (@CoUA_diese D C (@Ob_r (Dual D) C d2xc2) F (@CoUA_ob D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))) (@Prf_IsCoUA D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))) (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@Comp C (@FOb D C F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1)))) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2)))) (@Comp C (@FOb D C F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1)))) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1)))) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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)) (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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)) (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply CoUA_diag.
(* *) apply
       Trans
        with
          ((FMor F (CoUA_diese (UA_of (Ob_r d1xc1)) h)
            o CoUA_mor (UA_of (Ob_r d1xc1))) o Hom_r 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)) (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply Ass.
(* 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)) (@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 (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1)))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@CoUA_diese D C (@Ob_r (Dual D) C d1xc1) F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@Prf_IsCoUA D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@OB_l C D d1xc1) h)) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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)) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) h (@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)) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) h (@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)) h) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply Comp_r; apply CoUA_diag.
(* 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)) (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply Ass.
Qed.

Canonical Structure PsiUA := Build_NT PsiUA_tau_nt_law.
               
(* PsiUA_1 *)

 Section psi_ua_1_tau_def.

 Variable dxc : POb (Dual D) C.

 Definition PsiUA_1_arrow (f : OB_l dxc --> CoadjointUA (Ob_r dxc)) :=
   FMor F f o CoUA_mor (UA_of (Ob_r dxc)).

 Lemma PsiUA_1_arrow_map_law : Map_law PsiUA_1_arrow.                     
 Proof.
(* Goal: @Map_law (@Hom D (@OB_l C D dxc) (@FOb C D CoadjointUA (@Ob_r (Dual D) C dxc))) (@Hom C (@FOb D C F (@OB_l C D dxc)) (@Ob_r (Dual D) C dxc)) PsiUA_1_arrow *)
 unfold Map_law, PsiUA_1_arrow in |- *.
(* Goal: forall (x y : Carrier (@Hom D (@OB_l C D dxc) (@FOb C D CoadjointUA (@Ob_r (Dual D) C dxc)))) (_ : @Equal (@Hom D (@OB_l C D dxc) (@FOb C D CoadjointUA (@Ob_r (Dual D) C dxc))) x y), @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 (@FOb C D CoadjointUA (@Ob_r (Dual D) C dxc))) (@Ob_r (Dual D) C dxc) (@FMor D C F (@OB_l C D dxc) (@FOb C D CoadjointUA (@Ob_r (Dual D) C dxc)) x) (@CoUA_mor D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc)))) (@Comp C (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C dxc))) (@Ob_r (Dual D) C dxc) (@FMor D C F (@OB_l C D dxc) (@FOb C D CoadjointUA (@Ob_r (Dual D) C dxc)) y) (@CoUA_mor D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc)))) *)
 intros f g H.
(* Goal: @Equal (@Hom C (@FOb D C F (@Ob_l (Dual D) C dxc)) (@Ob_r (Dual D) C dxc)) f g *)
 apply Comp_r; apply FPres; assumption. 
 Qed.

 Canonical Structure PsiUA_1_tau := Build_Map PsiUA_1_arrow_map_law.
 
 End psi_ua_1_tau_def.
      
Lemma PsiUA_1_tau_nt_law :
 NT_law (F:=FunSET2_l CoadjointUA) (G:=FunSET2_r F) PsiUA_1_tau.
Proof.
(* Goal: @NT_law (PROD (Dual D) C) SET (@FunSET2_l C D CoadjointUA) (@FunSET2_r C D F) PsiUA_1_tau *)
unfold NT_law, PsiUA_1_tau, PsiUA_1_arrow in |- *; simpl in |- *.
(* Goal: @Ext (@FunSET2_r_ob C D F dxc) (@FunSET2_r_ob C D F dxc) (@Comp SET (@FunSET2_r_ob C D F dxc) (@FunSET2_l_ob C D CoadjointUA dxc) (@FunSET2_r_ob C D F dxc) (PsiUA_tau dxc) (PsiUA_1_tau dxc)) (Id_SET (@FunSET2_r_ob C D F dxc)) *)
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 CoadjointUA a)), @Equal (@FunSET2_r_ob C D F b) (@Comp C (@FOb D C F (@OB_l C D b)) (@FOb D C F (CoadjointUA_ob (@Ob_r (Dual D) C b))) (@Ob_r (Dual D) C b) (@FMor D C F (@OB_l C D b) (CoadjointUA_ob (@Ob_r (Dual D) C b)) (@FunSET2_l_mor1 C D CoadjointUA a b f x)) (@CoUA_mor D C (@Ob_r (Dual D) C b) F (UA_of (@Ob_r (Dual D) C b)))) (@FunSET2_r_mor1 C D F a b f (@Comp C (@FOb D C F (@OB_l C D a)) (@FOb D C F (CoadjointUA_ob (@Ob_r (Dual D) C a))) (@Ob_r (Dual D) C a) (@FMor D C F (@OB_l C D a) (CoadjointUA_ob (@Ob_r (Dual D) C a)) x) (@CoUA_mor D C (@Ob_r (Dual D) C a) F (UA_of (@Ob_r (Dual D) C a))))) *)
intros d1xc1 d2xc2 fxg h.
(* Goal: @Equal (@FunSET2_r_ob C D F d2xc2) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (CoadjointUA_ob (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d2xc2) (CoadjointUA_ob (@Ob_r (Dual D) C d2xc2)) (@FunSET2_l_mor1 C D CoadjointUA d1xc1 d2xc2 fxg h)) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2)))) (@FunSET2_r_mor1 C D F d1xc1 d2xc2 fxg (@Comp C (@FOb D C F (@OB_l C D d1xc1)) (@FOb D C F (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) *)
unfold 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 (CoadjointUA_ob (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d2xc2) (CoadjointUA_ob (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 fxg) h) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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 FMor F h)
            o FMor F (FMor CoadjointUA (Hom_r fxg)))
           o CoUA_mor (UA_of (Ob_r d2xc2))).
(* Goal: @Equal (@Hom C (@FOb D C F (@OB_l C D d2xc2)) (@Ob_r (Dual D) C d2xc2)) (@Comp C ((let (FOb, FMap, _, _) := F in FOb) (@OB_l C D d2xc2)) (@FOb D C F (CoadjointUA_ob (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d2xc2) (CoadjointUA_ob (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) (CoadjointUA_ob (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 fxg) h) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2)))) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h)) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2)))) *)
(* 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 (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h)) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply Comp_r.
(* *) apply
       Trans
        with (FMor F (HOM_l fxg o h) o FMor F (FMor CoadjointUA (Hom_r fxg))).
(* Goal: @Equal (@Hom C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)))) (@FMor D C F (@OB_l C D d2xc2) (CoadjointUA_ob (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) (CoadjointUA_ob (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 fxg) h) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)))) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@FMor D C F (@OB_l C D d2xc2) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 fxg) h)) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)))) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)))) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@FMor D C F (@OB_l C D d2xc2) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 fxg) h)) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)))) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h)) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@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 (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h)) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply FComp.
(* Goal: @Equal (@Hom C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)))) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@FMor D C F (@OB_l C D d2xc2) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 fxg) h)) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)))) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h)) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@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 (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@Comp C (@FOb D C F (@OB_l C D d2xc2)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h)) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply Comp_r; apply FComp.
(* *) apply
       Trans
        with
          ((FMor F (HOM_l fxg) o FMor F h)
           o FMor F (FMor CoadjointUA (Hom_r fxg))
             o CoUA_mor (UA_of (Ob_r d2xc2))).
(* 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 (@FOb C D CoadjointUA (@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)) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h)) (@Comp C (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@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 D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2)))))) *)
(* 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 D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply Ass1.
(* *) apply
       Trans
        with
          (FMor F (HOM_l fxg)
           o FMor F h
             o FMor F (FMor CoadjointUA (Hom_r fxg))
               o CoUA_mor (UA_of (Ob_r d2xc2))).
(* 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 (@FOb C D CoadjointUA (@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)) (@FOb D C F (@FOb C D CoadjointUA (@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)) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h)) (@Comp C (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@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 D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2)))))) *)
(* 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 D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply Ass1.
(* *) apply
       Trans
        with
          (FMor F (HOM_l fxg)
           o (FMor F h o CoUA_mor (UA_of (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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))))) (@Comp C (@FOb D C F (@OB_l C D d1xc1)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1)))) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1)))) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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)) (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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)) (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))))) (@Comp C (@FOb D C F (@OB_l C D d1xc1)) (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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)) (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
(* *) apply Trans with (FMor F h o CoUA_mor (UA_of (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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d2xc2)) (@FMor C D CoadjointUA (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))))) (@Comp C (@FOb D C F (@OB_l C D d1xc1)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1)))) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1)))) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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)) (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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)) (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply Comp_l.
unfold FMor at 2 in |- *; simpl in |- *;
(* Goal: forall a : Ob C, @Equal (@Hom D (CoadjointUA_ob a) (CoadjointUA_ob a)) (@CoadjointUA_mor a a (@Id C a)) (@Id D (CoadjointUA_ob a)) *)
 unfold CoadjointUA_mor, CoadjointUA_ob in |- *.
(* Goal: @Equal (@Hom C (@FOb D C F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1)))) (@Ob_r (Dual D) C d2xc2)) (@Comp C (@FOb D C F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1)))) (@FOb D C F (@CoUA_ob D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2)))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@CoUA_ob D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))) (@CoUA_diese D C (@Ob_r (Dual D) C d2xc2) F (@CoUA_ob D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))) (@Prf_IsCoUA D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2))) (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@Comp C (@FOb D C F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1)))) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)))) (@CoUA_mor D C (@Ob_r (Dual D) C d2xc2) F (UA_of (@Ob_r (Dual D) C d2xc2)))) (@Comp C (@FOb D C F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1)))) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@Comp C (@FOb D C F (@CoUA_ob D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1)))) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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)) (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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)) (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply CoUA_diag.
(* 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)) (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply Ass.
(* 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)) (@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 CoadjointUA (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (@FOb C D CoadjointUA (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@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 (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1))) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@OB_l C D d1xc1) (CoadjointUA_ob (@Ob_r (Dual D) C d1xc1)) h) (@CoUA_mor D C (@Ob_r (Dual D) C d1xc1) F (UA_of (@Ob_r (Dual D) C d1xc1))))) (@Hom_r (Dual D) C d1xc1 d2xc2 fxg)) *)
apply Ass.
Qed.

Canonical Structure PsiUA_1 := Build_NT PsiUA_1_tau_nt_law.

(* PsiUA et PsiUA_1 sont iso *)

 Section psi_ua_iso.

 Variable dxc : POb (Dual D) C.

 Lemma PsiUA_1_o_PsiUA : AreIsos (PsiUA dxc) (PsiUA_1 dxc).
 Proof.
(* Goal: @AreIsos SET (@FOb (PROD (Dual D) C) SET (@FunSET2_r C D F) dxc) (@FOb (PROD (Dual D) C) SET (@FunSET2_l C D CoadjointUA) dxc) (@ApNT (PROD (Dual D) C) SET (@FunSET2_r C D F) (@FunSET2_l C D CoadjointUA) PsiUA dxc) (@ApNT (PROD (Dual D) C) SET (@FunSET2_l C D CoadjointUA) (@FunSET2_r C D F) PsiUA_1 dxc) *)
 unfold AreIsos, RIso_law in |- *; simpl in |- *; split.
(* Goal: @Ext (@FunSET2_r_ob C D F dxc) (@FunSET2_r_ob C D F dxc) (@Comp SET (@FunSET2_r_ob C D F dxc) (@FunSET2_l_ob C D CoadjointUA dxc) (@FunSET2_r_ob C D F dxc) (PsiUA_tau dxc) (PsiUA_1_tau dxc)) (Id_SET (@FunSET2_r_ob C D F dxc)) *)
 unfold Ext in |- *; simpl in |- *.
(* Goal: forall x : Carrier (@FunSET2_r_ob C D F dxc), @Equal (@FunSET2_r_ob C D F dxc) (@PsiUA_1_arrow dxc (@PsiUA_arrow dxc x)) (@Id_fun (@FunSET2_r_ob C D F dxc) x) *)
 unfold PsiUA_arrow, Id_fun, PsiUA_1_arrow 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 CoadjointUA (@Ob_r (Dual D) C dxc))) (@Ob_r (Dual D) C dxc) (@FMor D C F (@OB_l C D dxc) (@FOb C D CoadjointUA (@Ob_r (Dual D) C dxc)) (@CoUA_diese D C (@Ob_r (Dual D) C dxc) F (@CoUA_ob D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc))) (@CoUA_mor D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc))) (@Prf_IsCoUA D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc))) (@Ob_l (Dual D) C dxc) x)) (@CoUA_mor D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc)))) x *)
 intro f.
(* Goal: @Equal (@FunSET2_l_ob C D CoadjointUA dxc) (@CoUA_diese D C (@Ob_r (Dual D) C dxc) F (@CoUA_ob D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc))) (@CoUA_mor D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc))) (@Prf_IsCoUA D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc))) (@Ob_l (Dual D) C dxc) (@Comp C (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@FOb C D CoadjointUA (@Ob_r (Dual D) C dxc))) (@Ob_r (Dual D) C dxc) (@FMor D C F (@OB_l C D dxc) (@FOb C D CoadjointUA (@Ob_r (Dual D) C dxc)) f) (@CoUA_mor D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc))))) f *)
(* Goal: @Ext (@FunSET2_r_ob C D F dxc) (@FunSET2_r_ob C D F dxc) (@Comp SET (@FunSET2_r_ob C D F dxc) (@FunSET2_l_ob C D CoadjointUA dxc) (@FunSET2_r_ob C D F dxc) (PsiUA_tau dxc) (PsiUA_1_tau dxc)) (Id_SET (@FunSET2_r_ob C D F dxc)) *)
 unfold FunSET2_l_ob in |- *; simpl in |- *; unfold CoadjointUA_ob in |- *.
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@CoUA_ob D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc)))) (@CoUA_diese D C (@Ob_r (Dual D) C dxc) F (@CoUA_ob D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc))) (@CoUA_mor D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc))) (@Prf_IsCoUA D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc))) (@Ob_l (Dual D) C dxc) (@Comp C (@FOb D C F (@OB_l C D dxc)) (@FOb D C F (@CoUA_ob D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc)))) (@Ob_r (Dual D) C dxc) (@FMor D C F (@OB_l C D dxc) (@CoUA_ob D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc))) f) (@CoUA_mor D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc))))) f *)
(* Goal: @Ext (@FunSET2_r_ob C D F dxc) (@FunSET2_r_ob C D F dxc) (@Comp SET (@FunSET2_r_ob C D F dxc) (@FunSET2_l_ob C D CoadjointUA dxc) (@FunSET2_r_ob C D F dxc) (PsiUA_tau dxc) (PsiUA_1_tau dxc)) (Id_SET (@FunSET2_r_ob C D F dxc)) *)
 apply CoUA_unic1; apply Refl.
 (**)
(* Goal: @Ext (@FunSET2_r_ob C D F dxc) (@FunSET2_r_ob C D F dxc) (@Comp SET (@FunSET2_r_ob C D F dxc) (@FunSET2_l_ob C D CoadjointUA dxc) (@FunSET2_r_ob C D F dxc) (PsiUA_tau dxc) (PsiUA_1_tau dxc)) (Id_SET (@FunSET2_r_ob C D F dxc)) *)
 unfold Ext in |- *; simpl in |- *.
(* Goal: forall x : Carrier (@FunSET2_r_ob C D F dxc), @Equal (@FunSET2_r_ob C D F dxc) (@PsiUA_1_arrow dxc (@PsiUA_arrow dxc x)) (@Id_fun (@FunSET2_r_ob C D F dxc) x) *)
 unfold PsiUA_arrow, Id_fun, PsiUA_1_arrow 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 CoadjointUA (@Ob_r (Dual D) C dxc))) (@Ob_r (Dual D) C dxc) (@FMor D C F (@OB_l C D dxc) (@FOb C D CoadjointUA (@Ob_r (Dual D) C dxc)) (@CoUA_diese D C (@Ob_r (Dual D) C dxc) F (@CoUA_ob D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc))) (@CoUA_mor D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc))) (@Prf_IsCoUA D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc))) (@Ob_l (Dual D) C dxc) x)) (@CoUA_mor D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc)))) x *)
 intro f.
(* Goal: @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 CoadjointUA (@Ob_r (Dual D) C dxc))) (@Ob_r (Dual D) C dxc) (@FMor D C F (@OB_l C D dxc) (@FOb C D CoadjointUA (@Ob_r (Dual D) C dxc)) (@CoUA_diese D C (@Ob_r (Dual D) C dxc) F (@CoUA_ob D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc))) (@CoUA_mor D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc))) (@Prf_IsCoUA D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc))) (@Ob_l (Dual D) C dxc) f)) (@CoUA_mor D C (@Ob_r (Dual D) C dxc) F (UA_of (@Ob_r (Dual D) C dxc)))) f *)
 unfold FunSET2_r_ob in |- *; apply (CoUA_diag (UA_of (Ob_r dxc))). 
 Qed.

 End psi_ua_iso.

Definition CoAdjUA := Build_Adj (NT_Iso PsiUA_1_o_PsiUA).

Canonical Structure RightAdjUA := Build_RightAdj CoAdjUA.

End ua_to_radj.
