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


(*****************************************************************************)
(*          Projet Coq - Calculus of Inductive Constructions V5.10           *)
(*****************************************************************************)
(*                                                                           *)
(*          Category Theory : Hom (Bi-)Functors (used in Adjunctions)        *)
(*                                                                           *)
(*          Amokrane Saibi May 1994                                          *)
(*                                                                           *)
(*****************************************************************************)


Require Export SET.
Require Export Dual.
Require Export PROD.
Require Export Functor.

Set Implicit Arguments.
Unset Strict Implicit.

(* C(-,G-) et D(F-,-) : D^o x C -> SET *)


(* C(F-,-) *)

Section FunSet2_r.

Variable C D : Category.

(* pour alle'ger les e'critures *)

 Section abrev.
 
 Definition OB_l (dxc : POb (Dual D) C) : D := Ob_l dxc.

 Variables (d1xc1 d2xc2 : POb (Dual D) C) (foxg : Pmor d1xc1 d2xc2).

 Definition HOM_l : OB_l d2xc2 --> OB_l d1xc1 := Hom_l foxg.

 Definition Build_POb1 (d : D) (c : C) := Build_POb (A:=Dual D) (B:=C) d c.

 Definition Build_Pmor1 (c c' : C) (d d' : D) (f : d' --> d)
   (g : c --> c') := Build_Pmor (u:=Build_POb1 d c) (t:=Build_POb1 d' c') f g.

 End abrev.

(* *)

Variable F : Functor D C.

Definition FunSET2_r_ob (dxc : POb (Dual D) C) := F (OB_l dxc) --> Ob_r dxc.

 Section funset2_r_map_def.

 Variable d1xc1 d2xc2 : POb (Dual D) C.

  Section funset2_r_mor_def.

  Variable foxg : Pmor d1xc1 d2xc2.

  Definition FunSET2_r_mor1 (h : FunSET2_r_ob d1xc1) :=
    (FMor F (HOM_l foxg) o h) o Hom_r foxg.

  Lemma FunSET2_r_map_law1 : Map_law FunSET2_r_mor1.
  Proof.
(* Goal: @Map_law (FunSET2_r_ob d1xc1) (@Hom C (@FOb D C F (OB_l d2xc2)) (@Ob_r (Dual D) C d2xc2)) FunSET2_r_mor1 *)
  unfold Map_law, FunSET2_r_mor1 in |- *; simpl in |- *.
(* Goal: forall (x y : Carrier (FunSET2_l_ob d1xc1)) (_ : @Equal (FunSET2_l_ob d1xc1) x y), @Equal (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 foxg) x) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 foxg))) (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 foxg) y) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 foxg))) *)
  intros h1 h2 H.
(* Goal: @Equal (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 foxg) h1) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 foxg))) (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 foxg) h2) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 foxg))) *)
  apply Comp_r; apply Comp_l; assumption.
  Qed.

  Canonical Structure FunSET2_r_mor :
    Map (FunSET2_r_ob d1xc1) (FunSET2_r_ob d2xc2) := FunSET2_r_map_law1.

  End funset2_r_mor_def.
  
 Lemma FunSET2_r_map_law : Map_law FunSET2_r_mor.
 Proof.
(* Goal: @Map_law (@Prod_Hom (Dual D) C d1xc1 d2xc2) (Map_setoid (FunSET2_r_ob d1xc1) (FunSET2_r_ob d2xc2)) FunSET2_r_mor *)
 unfold Map_law, FunSET2_r_mor in |- *.
(* Goal: forall (x y : Carrier (@Prod_Hom (Dual D) C d1xc1 d2xc2)) (_ : @Equal (@Prod_Hom (Dual D) C d1xc1 d2xc2) x y), @Equal (Map_setoid (FunSET2_l_ob d1xc1) (FunSET2_l_ob d2xc2)) (@Build_Map (FunSET2_l_ob d1xc1) (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (FunSET2_l_mor1 x) (@FunSET2_l_map_law1 x)) (@Build_Map (FunSET2_l_ob d1xc1) (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (FunSET2_l_mor1 y) (@FunSET2_l_map_law1 y)) *)
 intros f1xg1 f2xg2; elim f1xg1; intros f1 g1. 
(* Goal: forall _ : @Equal (@Prod_Hom (Dual D) C d1xc1 d2xc2) (@Build_Pmor (Dual D) C d1xc1 d2xc2 f1 g1) f2xg2, @Equal (Map_setoid (FunSET2_l_ob d1xc1) (FunSET2_l_ob d2xc2)) (@Build_Map (FunSET2_l_ob d1xc1) (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (FunSET2_l_mor1 (@Build_Pmor (Dual D) C d1xc1 d2xc2 f1 g1)) (@FunSET2_l_map_law1 (@Build_Pmor (Dual D) C d1xc1 d2xc2 f1 g1))) (@Build_Map (FunSET2_l_ob d1xc1) (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (FunSET2_l_mor1 f2xg2) (@FunSET2_l_map_law1 f2xg2)) *)
 elim f2xg2; intros f2 g2; simpl in |- *.
(* Goal: forall _ : @Equal_Pmor (Dual D) C d1xc1 d2xc2 (@Build_Pmor (Dual D) C d1xc1 d2xc2 f1 g1) (@Build_Pmor (Dual D) C d1xc1 d2xc2 f2 g2), @Ext (FunSET2_l_ob d1xc1) (FunSET2_l_ob d2xc2) (@Build_Map (FunSET2_l_ob d1xc1) (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (FunSET2_l_mor1 (@Build_Pmor (Dual D) C d1xc1 d2xc2 f1 g1)) (@FunSET2_l_map_law1 (@Build_Pmor (Dual D) C d1xc1 d2xc2 f1 g1))) (@Build_Map (FunSET2_l_ob d1xc1) (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (FunSET2_l_mor1 (@Build_Pmor (Dual D) C d1xc1 d2xc2 f2 g2)) (@FunSET2_l_map_law1 (@Build_Pmor (Dual D) C d1xc1 d2xc2 f2 g2))) *)
 unfold Ext in |- *; simpl in |- *.
(* Goal: forall (_ : @Equal_Pmor (Dual D) C d1xc1 d2xc2 (@Build_Pmor (Dual D) C d1xc1 d2xc2 f1 g1) (@Build_Pmor (Dual D) C d1xc1 d2xc2 f2 g2)) (x : Carrier (FunSET2_l_ob d1xc1)), @Equal (FunSET2_l_ob d2xc2) (FunSET2_l_mor1 (@Build_Pmor (Dual D) C d1xc1 d2xc2 f1 g1) x) (FunSET2_l_mor1 (@Build_Pmor (Dual D) C d1xc1 d2xc2 f2 g2) x) *)
 unfold Equal_Pmor in |- *; simpl in |- *.
(* Goal: forall (a : POb (Dual D) C) (x : Carrier (FunSET2_r_ob a)), @Equal (FunSET2_r_ob a) (@FunSET2_r_mor1 a a (@Id_PROD (Dual D) C a) x) (@Id_fun (FunSET2_r_ob a) x) *)
 unfold FunSET2_r_mor1 in |- *; simpl in |- *.
(* Goal: forall (_ : and (@Equal (@DHom D (@Ob_l (Dual D) C d1xc1) (@Ob_l (Dual D) C d2xc2)) f1 f2) (@Equal (@Hom C (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2)) g1 g2)) (x : Carrier (FunSET2_r_ob d1xc1)), @Equal (FunSET2_r_ob d2xc2) (@Comp C (@FOb D C F (OB_l d2xc2)) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Comp C (@FOb D C F (OB_l d2xc2)) (@FOb D C F (OB_l d1xc1)) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (OB_l d2xc2) (OB_l d1xc1) f1) x) g1) (@Comp C (@FOb D C F (OB_l d2xc2)) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Comp C (@FOb D C F (OB_l d2xc2)) (@FOb D C F (OB_l d1xc1)) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (OB_l d2xc2) (OB_l d1xc1) f2) x) g2) *)
 unfold FunSET2_r_ob in |- *.
(* Goal: forall (_ : and (@Equal (@DHom D (@Ob_l (Dual D) C d1xc1) (@Ob_l (Dual D) C d2xc2)) f1 f2) (@Equal (@Hom C (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2)) g1 g2)) (x : Carrier (@Hom D (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)))), @Equal (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 x) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f2 x) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g2)) *)
 intro H; elim H; intros H1 H2 h.
(* Goal: @Equal (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f2 h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g2)) *)
 apply Comp_lr.
(* Goal: @Equal (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1))) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f2 h) *)
(* Goal: @Equal (@Hom D (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g2) *)
 apply Comp_r; trivial.
(* Goal: @Equal (@Hom C (@FOb D C F (OB_l d2xc2)) (@FOb D C F (OB_l d1xc1))) (@FMor D C F (OB_l d2xc2) (OB_l d1xc1) f1) (@FMor D C F (OB_l d2xc2) (OB_l d1xc1) f2) *)
(* Goal: @Equal (@Hom C (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2)) g1 g2 *)
 apply FPres; assumption.
(* Goal: @Equal (@Hom C (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2)) g1 g2 *)
 assumption.
 Qed.

 Canonical Structure FunSET2_r_map := Build_Map FunSET2_r_map_law.

 End funset2_r_map_def.

Lemma Fun2_r_comp_law : Fcomp_law FunSET2_r_map.
Proof.
(* Goal: @Fcomp_law (PROD (Dual D) C) SET FunSET2_r_ob FunSET2_r_map *)
unfold Fcomp_law, FunSET2_r_map in |- *; simpl in |- *.
(* Goal: forall (a b c : POb (Dual D) C) (f : @Pmor (Dual D) C a b) (g : @Pmor (Dual D) C b c), @Ext (FunSET2_r_ob a) (FunSET2_r_ob c) (@FunSET2_r_mor a c (@Comp (PROD (Dual D) C) a b c f g)) (@Comp SET (FunSET2_r_ob a) (FunSET2_r_ob b) (FunSET2_r_ob c) (@FunSET2_r_mor a b f) (@FunSET2_r_mor b c g)) *)
unfold FunSET2_r_mor, Ext in |- *; simpl in |- *.
(* Goal: forall (a b c : POb (Dual D) C) (f : @Pmor (Dual D) C a b) (g : @Pmor (Dual D) C b c) (x : Carrier (FunSET2_r_ob a)), @Equal (FunSET2_r_ob c) (@FunSET2_r_mor1 a c (@Comp (PROD (Dual D) C) a b c f g) x) (@FunSET2_r_mor1 b c g (@FunSET2_r_mor1 a b f x)) *)
unfold FunSET2_r_mor1, FunSET2_r_ob in |- *; simpl in |- *.
(* Goal: forall (a b c : POb (Dual D) C) (f : @Pmor (Dual D) C a b) (g : @Pmor (Dual D) C b c) (x : Carrier (@Hom D (@OB_l C D a) (@FOb C D G (@Ob_r (Dual D) C a)))), @Equal (@Hom D (@OB_l C D c) (@FOb C D G (@Ob_r (Dual D) C c))) (@Comp D (@OB_l C D c) (@FOb C D G (@Ob_r (Dual D) C a)) (@FOb C D G (@Ob_r (Dual D) C c)) (@Comp D (@OB_l C D c) (@OB_l C D a) (@FOb C D G (@Ob_r (Dual D) C a)) (@Comp (Dual D) (@Ob_l (Dual D) C a) (@Ob_l (Dual D) C b) (@Ob_l (Dual D) C c) (@Hom_l (Dual D) C a b f) (@Hom_l (Dual D) C b c g)) x) (@FMor C D G (@Ob_r (Dual D) C a) (@Ob_r (Dual D) C c) (@Comp C (@Ob_r (Dual D) C a) (@Ob_r (Dual D) C b) (@Ob_r (Dual D) C c) (@Hom_r (Dual D) C a b f) (@Hom_r (Dual D) C b c g)))) (@Comp D (@OB_l C D c) (@FOb C D G (@Ob_r (Dual D) C b)) (@FOb C D G (@Ob_r (Dual D) C c)) (@Comp D (@OB_l C D c) (@OB_l C D b) (@FOb C D G (@Ob_r (Dual D) C b)) (@HOM_l C D b c g) (@Comp D (@OB_l C D b) (@FOb C D G (@Ob_r (Dual D) C a)) (@FOb C D G (@Ob_r (Dual D) C b)) (@Comp D (@OB_l C D b) (@OB_l C D a) (@FOb C D G (@Ob_r (Dual D) C a)) (@HOM_l C D a b f) x) (@FMor C D G (@Ob_r (Dual D) C a) (@Ob_r (Dual D) C b) (@Hom_r (Dual D) C a b f)))) (@FMor C D G (@Ob_r (Dual D) C b) (@Ob_r (Dual D) C c) (@Hom_r (Dual D) C b c g))) *)
intros d1xc1 d2xc2 d3xc3 f1xg1 f2xg2 h.
(* Goal: @Equal (@Hom D (@OB_l C D d3xc3) (@FOb C D G (@Ob_r (Dual D) C d3xc3))) (@Comp D (@OB_l C D d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@OB_l C D d3xc3) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp (Dual D) (@Ob_l (Dual D) C d1xc1) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d3xc3) (@Hom_l (Dual D) C d1xc1 d2xc2 f1xg1) (@Hom_l (Dual D) C d2xc2 d3xc3 f2xg2)) h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d3xc3) (@Comp C (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) (@Hom_r (Dual D) C d1xc1 d2xc2 f1xg1) (@Hom_r (Dual D) C d2xc2 d3xc3 f2xg2)))) (@Comp D (@OB_l C D d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@OB_l C D d3xc3) (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@HOM_l C D d2xc2 d3xc3 f2xg2) (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 f1xg1) h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 f1xg1)))) (@FMor C D G (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) (@Hom_r (Dual D) C d2xc2 d3xc3 f2xg2))) *)
elim f1xg1; simpl in |- *; unfold DHom in |- *; intros f1 g1.
(* Goal: @Equal (@Hom D (@OB_l C D d3xc3) (@FOb C D G (@Ob_r (Dual D) C d3xc3))) (@Comp D (@OB_l C D d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@OB_l C D d3xc3) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp (Dual D) (@Ob_l (Dual D) C d1xc1) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d3xc3) f1 (@Hom_l (Dual D) C d2xc2 d3xc3 f2xg2)) h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d3xc3) (@Comp C (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g1 (@Hom_r (Dual D) C d2xc2 d3xc3 f2xg2)))) (@Comp D (@OB_l C D d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@OB_l C D d3xc3) (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@HOM_l C D d2xc2 d3xc3 f2xg2) (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1))) (@FMor C D G (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) (@Hom_r (Dual D) C d2xc2 d3xc3 f2xg2))) *)
elim f2xg2; simpl in |- *; unfold DHom in |- *; intros f2 g2; simpl in |- *.
(* Goal: @Equal (@Hom C (@FOb D C F (OB_l d3xc3)) (@Ob_r (Dual D) C d3xc3)) (@Comp C (@FOb D C F (OB_l d3xc3)) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d3xc3) (@Comp C (@FOb D C F (OB_l d3xc3)) (@FOb D C F (OB_l d1xc1)) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (OB_l d3xc3) (OB_l d1xc1) (@Comp (Dual D) (@Ob_l (Dual D) C d1xc1) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d3xc3) f1 f2)) h) (@Comp C (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g1 g2)) (@Comp C (@FOb D C F (OB_l d3xc3)) (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) (@Comp C (@FOb D C F (OB_l d3xc3)) (@FOb D C F (OB_l d2xc2)) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (OB_l d3xc3) (OB_l d2xc2) f2) (@Comp C (@FOb D C F (OB_l d2xc2)) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Comp C (@FOb D C F (OB_l d2xc2)) (@FOb D C F (OB_l d1xc1)) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (OB_l d2xc2) (OB_l d1xc1) f1) h) g1)) g2) *)
(* *) apply Trans with (((FMor F (f2 o f1) o h) o g1) o g2).
(* Goal: @Equal (@Hom D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d3xc3))) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) f2 f1) h) (@Comp D (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1) (@FMor C D G (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g2))) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) f2 f1) h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) (@FMor C D G (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g2)) *)
(* Goal: @Equal (@Hom D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d3xc3))) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) f2 f1) h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) (@FMor C D G (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g2)) (@Comp D (@OB_l C D d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@OB_l C D d3xc3) (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) f2 (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1))) (@FMor C D G (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g2)) *)
apply Ass.
(* Goal: @Equal (@Hom D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) f2 f1) h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f2 (@Comp D (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h)) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) *)
(* Goal: @Equal (@Hom D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f2 (@Comp D (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h)) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) (@Comp D (@OB_l C D d3xc3) (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) f2 (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1))) *)
apply Comp_r.
(* Goal: @Equal (@Hom C (@FOb D C F (OB_l d3xc3)) (@Ob_r (Dual D) C d2xc2)) (@Comp C (@FOb D C F (@Ob_l (Dual D) C d3xc3)) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Comp C (@FOb D C F (@Ob_l (Dual D) C d3xc3)) (@FOb D C F (@Ob_l (Dual D) C d1xc1)) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d1xc1) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) f2 f1)) h) g1) (@Comp C (@FOb D C F (OB_l d3xc3)) (@FOb D C F (OB_l d2xc2)) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (OB_l d3xc3) (OB_l d2xc2) f2) (@Comp C (@FOb D C F (OB_l d2xc2)) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Comp C (@FOb D C F (OB_l d2xc2)) (@FOb D C F (OB_l d1xc1)) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (OB_l d2xc2) (OB_l d1xc1) f1) h) g1)) *)
(* *) apply Trans with ((FMor F f2 o FMor F f1 o h) o g1).
(* Goal: @Equal (@Hom D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) f2 f1) h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f2 (@Comp D (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h)) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) *)
(* Goal: @Equal (@Hom D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f2 (@Comp D (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h)) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) (@Comp D (@OB_l C D d3xc3) (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) f2 (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1))) *)
apply Comp_r.
(* Goal: @Equal (@Hom C (@FOb D C F (@Ob_l (Dual D) C d3xc3)) (@Ob_r (Dual D) C d1xc1)) (@Comp C (@FOb D C F (@Ob_l (Dual D) C d3xc3)) (@FOb D C F (@Ob_l (Dual D) C d1xc1)) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d1xc1) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) f2 f1)) h) (@Comp C (@FOb D C F (@Ob_l (Dual D) C d3xc3)) (@FOb D C F (@Ob_l (Dual D) C d2xc2)) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) f2) (@Comp C (@FOb D C F (@Ob_l (Dual D) C d2xc2)) (@FOb D C F (@Ob_l (Dual D) C d1xc1)) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) f1) h)) *)
(* Goal: @Equal (@Hom C (@FOb D C F (@Ob_l (Dual D) C d3xc3)) (@Ob_r (Dual D) C d2xc2)) (@Comp C (@FOb D C F (@Ob_l (Dual D) C d3xc3)) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Comp C (@FOb D C F (@Ob_l (Dual D) C d3xc3)) (@FOb D C F (@Ob_l (Dual D) C d2xc2)) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) f2) (@Comp C (@FOb D C F (@Ob_l (Dual D) C d2xc2)) (@FOb D C F (@Ob_l (Dual D) C d1xc1)) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) f1) h)) g1) (@Comp C (@FOb D C F (OB_l d3xc3)) (@FOb D C F (OB_l d2xc2)) (@Ob_r (Dual D) C d2xc2) (@FMor D C F (OB_l d3xc3) (OB_l d2xc2) f2) (@Comp C (@FOb D C F (OB_l d2xc2)) (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Comp C (@FOb D C F (OB_l d2xc2)) (@FOb D C F (OB_l d1xc1)) (@Ob_r (Dual D) C d1xc1) (@FMor D C F (OB_l d2xc2) (OB_l d1xc1) f1) h) g1)) *)
(* *) apply Trans with ((FMor F f2 o FMor F f1) o h).
(* Goal: @Equal (@Hom D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) f2 f1) h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f2 (@Comp D (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h)) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) *)
(* Goal: @Equal (@Hom D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f2 (@Comp D (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h)) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) (@Comp D (@OB_l C D d3xc3) (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) f2 (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1))) *)
apply Comp_r.
(* Goal: @Equal (@Hom D (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d3xc3))) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d3xc3) (@Comp C (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g1 g2)) (@Comp D (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1) (@FMor C D G (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g2)) *)
(* Goal: @Equal (@Hom D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d3xc3))) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) f2 f1) h) (@Comp D (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1) (@FMor C D G (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g2))) (@Comp D (@OB_l C D d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@OB_l C D d3xc3) (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) f2 (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1))) (@FMor C D G (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g2)) *)
apply FComp.
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Comp D (@OB_l C D dxc) (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Id D (@Ob_l (Dual D) C dxc)) f) (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc)))) (@Comp D (@OB_l C D dxc) (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Id D (@OB_l C D dxc)) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) f (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc))))) *)
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Id D (@OB_l C D dxc)) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) f (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc))))) f *)
apply Ass1.
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Comp D (@OB_l C D dxc) (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Id D (@Ob_l (Dual D) C dxc)) f) (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc)))) (@Comp D (@OB_l C D dxc) (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Id D (@OB_l C D dxc)) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) f (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc))))) *)
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Id D (@OB_l C D dxc)) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) f (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc))))) f *)
apply Ass1.
Qed.

Lemma Fun2_r_id_law : Fid_law FunSET2_r_map.
Proof.
(* Goal: @Fid_law (PROD (Dual D) C) SET FunSET2_r_ob FunSET2_r_map *)
unfold Fid_law, FunSET2_r_map, FunSET2_r_mor in |- *; simpl in |- *.
(* Goal: forall a : POb (Dual D) C, @Ext (FunSET2_l_ob a) (FunSET2_l_ob a) (@Build_Map (FunSET2_l_ob a) (@Hom D (@OB_l C D a) (@FOb C D G (@Ob_r (Dual D) C a))) (@FunSET2_l_mor1 a a (@Id_PROD (Dual D) C a)) (@FunSET2_l_map_law1 a a (@Id_PROD (Dual D) C a))) (Id_SET (FunSET2_l_ob a)) *)
unfold Ext, Id_SET in |- *; simpl in |- *.
(* Goal: forall (a : POb (Dual D) C) (x : Carrier (FunSET2_r_ob a)), @Equal (FunSET2_r_ob a) (@FunSET2_r_mor1 a a (@Id_PROD (Dual D) C a) x) (@Id_fun (FunSET2_r_ob a) x) *)
unfold FunSET2_r_mor1 in |- *; simpl in |- *.
(* Goal: forall (a : POb (Dual D) C) (x : Carrier (FunSET2_r_ob a)), @Equal (FunSET2_r_ob a) (@Comp C (@FOb D C F (OB_l a)) (@Ob_r (Dual D) C a) (@Ob_r (Dual D) C a) (@Comp C (@FOb D C F (OB_l a)) (@FOb D C F (OB_l a)) (@Ob_r (Dual D) C a) (@FMor D C F (OB_l a) (OB_l a) (@Id D (@Ob_l (Dual D) C a))) x) (@Id C (@Ob_r (Dual D) C a))) (@Id_fun (FunSET2_r_ob a) x) *)
unfold FunSET2_r_ob in |- *; intros dxc f.
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Comp D (@OB_l C D dxc) (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Id D (@Ob_l (Dual D) C dxc)) f) (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc)))) (@Id_fun (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) f) *)
unfold Id_fun in |- *.
(* Goal: @Equal (@Hom C (@FOb D C F (OB_l dxc)) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (OB_l dxc)) (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Comp C (@FOb D C F (OB_l dxc)) (@FOb D C F (OB_l dxc)) (@Ob_r (Dual D) C dxc) (@FMor D C F (OB_l dxc) (OB_l dxc) (@Id D (@Ob_l (Dual D) C dxc))) f) (@Id C (@Ob_r (Dual D) C dxc))) f *)
(* *) apply Trans with (FMor F (Id (OB_l dxc)) o f).
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) f (@Id D (@FOb C D G (@Ob_r (Dual D) C dxc)))) f *)
apply Idr1.
(* Goal: @Equal (@Hom C (@FOb D C F (OB_l dxc)) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (OB_l dxc)) (@FOb D C F (OB_l dxc)) (@Ob_r (Dual D) C dxc) (@FMor D C F (OB_l dxc) (OB_l dxc) (@Id D (OB_l dxc))) f) f *)
(* *) apply Trans with (Id (F (OB_l dxc)) o f).
(* Goal: @Equal (@Hom D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) f2 f1) h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f2 (@Comp D (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h)) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) *)
(* Goal: @Equal (@Hom D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f2 (@Comp D (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h)) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) (@Comp D (@OB_l C D d3xc3) (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) f2 (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1))) *)
apply Comp_r.
(* Goal: @Equal (@Hom C (@FOb D C F (OB_l dxc)) (@FOb D C F (OB_l dxc))) (@FMor D C F (OB_l dxc) (OB_l dxc) (@Id D (OB_l dxc))) (@Id C (@FOb D C F (OB_l dxc))) *)
(* Goal: @Equal (@Hom C (@FOb D C F (OB_l dxc)) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (OB_l dxc)) (@FOb D C F (OB_l dxc)) (@Ob_r (Dual D) C dxc) (@Id C (@FOb D C F (OB_l dxc))) f) f *)
apply FId.
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Id D (@OB_l C D dxc)) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) f (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc))))) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) f (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc)))) *)
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) f (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc)))) f *)
apply Idl.
Qed.

Canonical Structure FunSET2_r := Build_Functor Fun2_r_comp_law Fun2_r_id_law.

End FunSet2_r.


Section FunSet2_l.

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

(* D(-,G-) *)

Definition FunSET2_l_ob (dxc : POb (Dual D) C) := OB_l dxc --> G (Ob_r dxc).

 Section funset2_l_map_def.

 Variable d1xc1 d2xc2 : POb (Dual D) C.

  Section funset2_l_mor_def.

  Variable foxg : Pmor d1xc1 d2xc2.

  Definition FunSET2_l_mor1 (h : FunSET2_l_ob d1xc1) :=
    (HOM_l foxg o h) o FMor G (Hom_r foxg).

  Lemma FunSET2_l_map_law1 : Map_law FunSET2_l_mor1.
  Proof.
(* Goal: @Map_law (FunSET2_l_ob d1xc1) (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) FunSET2_l_mor1 *)
  unfold Map_law, FunSET2_l_mor1 in |- *; simpl in |- *.
(* Goal: forall (x y : Carrier (FunSET2_l_ob d1xc1)) (_ : @Equal (FunSET2_l_ob d1xc1) x y), @Equal (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 foxg) x) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 foxg))) (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 foxg) y) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 foxg))) *)
  intros h1 h2 H.
(* Goal: @Equal (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 foxg) h1) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 foxg))) (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 foxg) h2) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 foxg))) *)
  apply Comp_r; apply Comp_l; assumption.
  Qed.

  Canonical Structure FunSET2_l_mor :
    Map (FunSET2_l_ob d1xc1) (FunSET2_l_ob d2xc2) := FunSET2_l_map_law1.

  End funset2_l_mor_def.

 Lemma FunSET2_l_map_law : Map_law FunSET2_l_mor.
 Proof.
(* Goal: @Map_law (@Prod_Hom (Dual D) C d1xc1 d2xc2) (Map_setoid (FunSET2_l_ob d1xc1) (FunSET2_l_ob d2xc2)) FunSET2_l_mor *)
 unfold Map_law, FunSET2_l_mor in |- *.
(* Goal: forall (x y : Carrier (@Prod_Hom (Dual D) C d1xc1 d2xc2)) (_ : @Equal (@Prod_Hom (Dual D) C d1xc1 d2xc2) x y), @Equal (Map_setoid (FunSET2_l_ob d1xc1) (FunSET2_l_ob d2xc2)) (@Build_Map (FunSET2_l_ob d1xc1) (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (FunSET2_l_mor1 x) (@FunSET2_l_map_law1 x)) (@Build_Map (FunSET2_l_ob d1xc1) (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (FunSET2_l_mor1 y) (@FunSET2_l_map_law1 y)) *)
 intros f1xg1 f2xg2; elim f1xg1; intros f1 g1. 
(* Goal: forall _ : @Equal (@Prod_Hom (Dual D) C d1xc1 d2xc2) (@Build_Pmor (Dual D) C d1xc1 d2xc2 f1 g1) f2xg2, @Equal (Map_setoid (FunSET2_l_ob d1xc1) (FunSET2_l_ob d2xc2)) (@Build_Map (FunSET2_l_ob d1xc1) (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (FunSET2_l_mor1 (@Build_Pmor (Dual D) C d1xc1 d2xc2 f1 g1)) (@FunSET2_l_map_law1 (@Build_Pmor (Dual D) C d1xc1 d2xc2 f1 g1))) (@Build_Map (FunSET2_l_ob d1xc1) (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (FunSET2_l_mor1 f2xg2) (@FunSET2_l_map_law1 f2xg2)) *)
 elim f2xg2; intros f2 g2; simpl in |- *.
(* Goal: forall _ : @Equal_Pmor (Dual D) C d1xc1 d2xc2 (@Build_Pmor (Dual D) C d1xc1 d2xc2 f1 g1) (@Build_Pmor (Dual D) C d1xc1 d2xc2 f2 g2), @Ext (FunSET2_l_ob d1xc1) (FunSET2_l_ob d2xc2) (@Build_Map (FunSET2_l_ob d1xc1) (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (FunSET2_l_mor1 (@Build_Pmor (Dual D) C d1xc1 d2xc2 f1 g1)) (@FunSET2_l_map_law1 (@Build_Pmor (Dual D) C d1xc1 d2xc2 f1 g1))) (@Build_Map (FunSET2_l_ob d1xc1) (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (FunSET2_l_mor1 (@Build_Pmor (Dual D) C d1xc1 d2xc2 f2 g2)) (@FunSET2_l_map_law1 (@Build_Pmor (Dual D) C d1xc1 d2xc2 f2 g2))) *)
 unfold Ext in |- *; simpl in |- *.
(* Goal: forall (_ : @Equal_Pmor (Dual D) C d1xc1 d2xc2 (@Build_Pmor (Dual D) C d1xc1 d2xc2 f1 g1) (@Build_Pmor (Dual D) C d1xc1 d2xc2 f2 g2)) (x : Carrier (FunSET2_l_ob d1xc1)), @Equal (FunSET2_l_ob d2xc2) (FunSET2_l_mor1 (@Build_Pmor (Dual D) C d1xc1 d2xc2 f1 g1) x) (FunSET2_l_mor1 (@Build_Pmor (Dual D) C d1xc1 d2xc2 f2 g2) x) *)
 unfold Equal_Pmor in |- *; simpl in |- *.
(* Goal: forall (a : POb (Dual D) C) (x : Carrier (FunSET2_l_ob a)), @Equal (FunSET2_l_ob a) (@FunSET2_l_mor1 a a (@Id_PROD (Dual D) C a) x) (@Id_fun (FunSET2_l_ob a) x) *)
 unfold FunSET2_l_mor1 in |- *; simpl in |- *.
(* Goal: forall (_ : and (@Equal (@DHom D (@Ob_l (Dual D) C d1xc1) (@Ob_l (Dual D) C d2xc2)) f1 f2) (@Equal (@Hom C (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2)) g1 g2)) (x : Carrier (FunSET2_l_ob d1xc1)), @Equal (FunSET2_l_ob d2xc2) (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 x) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f2 x) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g2)) *)
 unfold FunSET2_l_ob in |- *.
(* Goal: forall (_ : and (@Equal (@DHom D (@Ob_l (Dual D) C d1xc1) (@Ob_l (Dual D) C d2xc2)) f1 f2) (@Equal (@Hom C (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2)) g1 g2)) (x : Carrier (@Hom D (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)))), @Equal (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 x) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f2 x) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g2)) *)
 intro H; elim H; intros H1 H2 h.
(* Goal: @Equal (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f2 h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g2)) *)
 apply Comp_lr.
(* Goal: @Equal (@Hom D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1))) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f2 h) *)
(* Goal: @Equal (@Hom D (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g2) *)
 apply Comp_r; trivial.
(* Goal: @Equal (@Hom D (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g2) *)
 apply FPres. 
(* Goal: @Equal (@Hom C (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2)) g1 g2 *)
 assumption.
 Qed.

 Canonical Structure FunSET2_l_map := Build_Map FunSET2_l_map_law.

 End funset2_l_map_def.
 
Lemma Fun2_l_comp_law : Fcomp_law FunSET2_l_map.
Proof.
(* Goal: @Fcomp_law (PROD (Dual D) C) SET FunSET2_l_ob FunSET2_l_map *)
unfold Fcomp_law, FunSET2_l_map in |- *; simpl in |- *.
(* Goal: forall (a b c : POb (Dual D) C) (f : @Pmor (Dual D) C a b) (g : @Pmor (Dual D) C b c), @Ext (FunSET2_l_ob a) (FunSET2_l_ob c) (@FunSET2_l_mor a c (@Comp (PROD (Dual D) C) a b c f g)) (@Comp SET (FunSET2_l_ob a) (FunSET2_l_ob b) (FunSET2_l_ob c) (@FunSET2_l_mor a b f) (@FunSET2_l_mor b c g)) *)
unfold FunSET2_l_mor, Ext in |- *; simpl in |- *.
(* Goal: forall (a b c : POb (Dual D) C) (f : @Pmor (Dual D) C a b) (g : @Pmor (Dual D) C b c) (x : Carrier (FunSET2_l_ob a)), @Equal (FunSET2_l_ob c) (@FunSET2_l_mor1 a c (@Comp (PROD (Dual D) C) a b c f g) x) (@FunSET2_l_mor1 b c g (@FunSET2_l_mor1 a b f x)) *)
unfold FunSET2_l_mor1, FunSET2_l_ob in |- *; simpl in |- *.
(* Goal: forall (a b c : POb (Dual D) C) (f : @Pmor (Dual D) C a b) (g : @Pmor (Dual D) C b c) (x : Carrier (@Hom D (@OB_l C D a) (@FOb C D G (@Ob_r (Dual D) C a)))), @Equal (@Hom D (@OB_l C D c) (@FOb C D G (@Ob_r (Dual D) C c))) (@Comp D (@OB_l C D c) (@FOb C D G (@Ob_r (Dual D) C a)) (@FOb C D G (@Ob_r (Dual D) C c)) (@Comp D (@OB_l C D c) (@OB_l C D a) (@FOb C D G (@Ob_r (Dual D) C a)) (@Comp (Dual D) (@Ob_l (Dual D) C a) (@Ob_l (Dual D) C b) (@Ob_l (Dual D) C c) (@Hom_l (Dual D) C a b f) (@Hom_l (Dual D) C b c g)) x) (@FMor C D G (@Ob_r (Dual D) C a) (@Ob_r (Dual D) C c) (@Comp C (@Ob_r (Dual D) C a) (@Ob_r (Dual D) C b) (@Ob_r (Dual D) C c) (@Hom_r (Dual D) C a b f) (@Hom_r (Dual D) C b c g)))) (@Comp D (@OB_l C D c) (@FOb C D G (@Ob_r (Dual D) C b)) (@FOb C D G (@Ob_r (Dual D) C c)) (@Comp D (@OB_l C D c) (@OB_l C D b) (@FOb C D G (@Ob_r (Dual D) C b)) (@HOM_l C D b c g) (@Comp D (@OB_l C D b) (@FOb C D G (@Ob_r (Dual D) C a)) (@FOb C D G (@Ob_r (Dual D) C b)) (@Comp D (@OB_l C D b) (@OB_l C D a) (@FOb C D G (@Ob_r (Dual D) C a)) (@HOM_l C D a b f) x) (@FMor C D G (@Ob_r (Dual D) C a) (@Ob_r (Dual D) C b) (@Hom_r (Dual D) C a b f)))) (@FMor C D G (@Ob_r (Dual D) C b) (@Ob_r (Dual D) C c) (@Hom_r (Dual D) C b c g))) *)
intros d1xc1 d2xc2 d3xc3 f1xg1 f2xg2 h.
(* Goal: @Equal (@Hom D (@OB_l C D d3xc3) (@FOb C D G (@Ob_r (Dual D) C d3xc3))) (@Comp D (@OB_l C D d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@OB_l C D d3xc3) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp (Dual D) (@Ob_l (Dual D) C d1xc1) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d3xc3) (@Hom_l (Dual D) C d1xc1 d2xc2 f1xg1) (@Hom_l (Dual D) C d2xc2 d3xc3 f2xg2)) h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d3xc3) (@Comp C (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) (@Hom_r (Dual D) C d1xc1 d2xc2 f1xg1) (@Hom_r (Dual D) C d2xc2 d3xc3 f2xg2)))) (@Comp D (@OB_l C D d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@OB_l C D d3xc3) (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@HOM_l C D d2xc2 d3xc3 f2xg2) (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@HOM_l C D d1xc1 d2xc2 f1xg1) h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Hom_r (Dual D) C d1xc1 d2xc2 f1xg1)))) (@FMor C D G (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) (@Hom_r (Dual D) C d2xc2 d3xc3 f2xg2))) *)
elim f1xg1; simpl in |- *; unfold DHom in |- *; intros f1 g1.
(* Goal: @Equal (@Hom D (@OB_l C D d3xc3) (@FOb C D G (@Ob_r (Dual D) C d3xc3))) (@Comp D (@OB_l C D d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@OB_l C D d3xc3) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp (Dual D) (@Ob_l (Dual D) C d1xc1) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d3xc3) f1 (@Hom_l (Dual D) C d2xc2 d3xc3 f2xg2)) h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d3xc3) (@Comp C (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g1 (@Hom_r (Dual D) C d2xc2 d3xc3 f2xg2)))) (@Comp D (@OB_l C D d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@OB_l C D d3xc3) (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@HOM_l C D d2xc2 d3xc3 f2xg2) (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1))) (@FMor C D G (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) (@Hom_r (Dual D) C d2xc2 d3xc3 f2xg2))) *)
elim f2xg2; simpl in |- *; unfold DHom in |- *; intros f2 g2; simpl in |- *.

(* Goal: @Equal (@Hom D (@OB_l C D d3xc3) (@FOb C D G (@Ob_r (Dual D) C d3xc3))) (@Comp D (@OB_l C D d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@OB_l C D d3xc3) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp (Dual D) (@Ob_l (Dual D) C d1xc1) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d3xc3) f1 f2) h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d3xc3) (@Comp C (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g1 g2))) (@Comp D (@OB_l C D d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@OB_l C D d3xc3) (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) f2 (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1))) (@FMor C D G (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g2)) *)
(* *) apply Trans with (((f2 o f1) o h) o FMor G g1 o FMor G g2).
(* Goal: @Equal (@Hom D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d3xc3))) (@Comp D (@OB_l C D d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@OB_l C D d3xc3) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp (Dual D) (@Ob_l (Dual D) C d1xc1) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d3xc3) f1 f2) h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d3xc3) (@Comp C (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g1 g2))) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) f2 f1) h) (@Comp D (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1) (@FMor C D G (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g2))) *)
(* Goal: @Equal (@Hom D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d3xc3))) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) f2 f1) h) (@Comp D (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1) (@FMor C D G (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g2))) (@Comp D (@OB_l C D d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@OB_l C D d3xc3) (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) f2 (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1))) (@FMor C D G (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g2)) *)
apply Comp_l.
(* Goal: @Equal (@Hom D (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d3xc3))) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d3xc3) (@Comp C (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g1 g2)) (@Comp D (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1) (@FMor C D G (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g2)) *)
(* Goal: @Equal (@Hom D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d3xc3))) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) f2 f1) h) (@Comp D (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1) (@FMor C D G (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g2))) (@Comp D (@OB_l C D d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@OB_l C D d3xc3) (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) f2 (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1))) (@FMor C D G (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g2)) *)
apply FComp.
(* Goal: @Equal (@Hom D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d3xc3))) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) f2 f1) h) (@Comp D (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1) (@FMor C D G (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g2))) (@Comp D (@OB_l C D d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@OB_l C D d3xc3) (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) f2 (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1))) (@FMor C D G (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g2)) *)
(* *) apply Trans with ((((f2 o f1) o h) o FMor G g1) o FMor G g2).
(* Goal: @Equal (@Hom D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d3xc3))) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) f2 f1) h) (@Comp D (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1) (@FMor C D G (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g2))) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) f2 f1) h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) (@FMor C D G (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g2)) *)
(* Goal: @Equal (@Hom D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d3xc3))) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) f2 f1) h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) (@FMor C D G (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g2)) (@Comp D (@OB_l C D d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@FOb C D G (@Ob_r (Dual D) C d3xc3)) (@Comp D (@OB_l C D d3xc3) (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) f2 (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1))) (@FMor C D G (@Ob_r (Dual D) C d2xc2) (@Ob_r (Dual D) C d3xc3) g2)) *)
apply Ass.
(* Goal: @Equal (@Hom D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) f2 f1) h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f2 (@Comp D (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h)) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) *)
(* Goal: @Equal (@Hom D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f2 (@Comp D (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h)) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) (@Comp D (@OB_l C D d3xc3) (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) f2 (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1))) *)
apply Comp_r.
(* Goal: @Equal (@Hom D (@OB_l C D d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) f2 f1) h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) (@Comp D (@OB_l C D d3xc3) (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) f2 (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1))) *)
(* *) apply Trans with ((f2 o f1 o h) o FMor G g1).
(* Goal: @Equal (@Hom D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) f2 f1) h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f2 (@Comp D (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h)) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) *)
(* Goal: @Equal (@Hom D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d2xc2))) (@Comp D (@Ob_l (Dual D) C d3xc3) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@Ob_l (Dual D) C d3xc3) (@Ob_l (Dual D) C d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f2 (@Comp D (@Ob_l (Dual D) C d2xc2) (@Ob_l (Dual D) C d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h)) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1)) (@Comp D (@OB_l C D d3xc3) (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) f2 (@Comp D (@OB_l C D d2xc2) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) (@FOb C D G (@Ob_r (Dual D) C d2xc2)) (@Comp D (@OB_l C D d2xc2) (@OB_l C D d1xc1) (@FOb C D G (@Ob_r (Dual D) C d1xc1)) f1 h) (@FMor C D G (@Ob_r (Dual D) C d1xc1) (@Ob_r (Dual D) C d2xc2) g1))) *)
apply Comp_r.
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Comp D (@OB_l C D dxc) (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Id D (@Ob_l (Dual D) C dxc)) f) (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc)))) (@Comp D (@OB_l C D dxc) (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Id D (@OB_l C D dxc)) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) f (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc))))) *)
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Id D (@OB_l C D dxc)) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) f (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc))))) f *)
apply Ass1.
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Comp D (@OB_l C D dxc) (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Id D (@Ob_l (Dual D) C dxc)) f) (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc)))) (@Comp D (@OB_l C D dxc) (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Id D (@OB_l C D dxc)) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) f (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc))))) *)
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Id D (@OB_l C D dxc)) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) f (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc))))) f *)
apply Ass1.
Qed.

Lemma Fun2_l_id_law : Fid_law FunSET2_l_map.
Proof.
(* Goal: @Fid_law (PROD (Dual D) C) SET FunSET2_l_ob FunSET2_l_map *)
unfold Fid_law, FunSET2_l_map, FunSET2_l_mor in |- *; simpl in |- *.
(* Goal: forall a : POb (Dual D) C, @Ext (FunSET2_l_ob a) (FunSET2_l_ob a) (@Build_Map (FunSET2_l_ob a) (@Hom D (@OB_l C D a) (@FOb C D G (@Ob_r (Dual D) C a))) (@FunSET2_l_mor1 a a (@Id_PROD (Dual D) C a)) (@FunSET2_l_map_law1 a a (@Id_PROD (Dual D) C a))) (Id_SET (FunSET2_l_ob a)) *)
unfold Ext, Id_SET in |- *; simpl in |- *.
(* Goal: forall (a : POb (Dual D) C) (x : Carrier (FunSET2_l_ob a)), @Equal (FunSET2_l_ob a) (@FunSET2_l_mor1 a a (@Id_PROD (Dual D) C a) x) (@Id_fun (FunSET2_l_ob a) x) *)
unfold FunSET2_l_mor1 in |- *; simpl in |- *.
(* Goal: forall (a : POb (Dual D) C) (x : Carrier (FunSET2_l_ob a)), @Equal (FunSET2_l_ob a) (@Comp D (@OB_l C D a) (@FOb C D G (@Ob_r (Dual D) C a)) (@FOb C D G (@Ob_r (Dual D) C a)) (@Comp D (@OB_l C D a) (@OB_l C D a) (@FOb C D G (@Ob_r (Dual D) C a)) (@Id D (@Ob_l (Dual D) C a)) x) (@FMor C D G (@Ob_r (Dual D) C a) (@Ob_r (Dual D) C a) (@Id C (@Ob_r (Dual D) C a)))) (@Id_fun (FunSET2_l_ob a) x) *)
unfold FunSET2_l_ob in |- *; simpl in |- *; intros dxc f.
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Comp D (@OB_l C D dxc) (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Id D (@Ob_l (Dual D) C dxc)) f) (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc)))) (@Id_fun (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) f) *)
unfold Id_fun in |- *.
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Comp D (@OB_l C D dxc) (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Id D (@Ob_l (Dual D) C dxc)) f) (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc)))) f *)
(* *) apply Trans with (Id (OB_l dxc) o f o FMor G (Id (Ob_r dxc))).
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Comp D (@OB_l C D dxc) (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Id D (@Ob_l (Dual D) C dxc)) f) (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc)))) (@Comp D (@OB_l C D dxc) (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Id D (@OB_l C D dxc)) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) f (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc))))) *)
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Id D (@OB_l C D dxc)) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) f (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc))))) f *)
apply Ass1.
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Id D (@OB_l C D dxc)) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) f (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc))))) f *)
(* *) apply Trans with (f o FMor G (Id (Ob_r dxc))).
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@Id D (@OB_l C D dxc)) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) f (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc))))) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) f (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc)))) *)
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) f (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc)))) f *)
apply Idl.
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) f (@FMor C D G (@Ob_r (Dual D) C dxc) (@Ob_r (Dual D) C dxc) (@Id C (@Ob_r (Dual D) C dxc)))) f *)
(* *) apply Trans with (f o Id (G (Ob_r dxc))).
(* Goal: @Equal (@Hom C (@FOb D C F (OB_l dxc)) (@FOb D C F (OB_l dxc))) (@FMor D C F (OB_l dxc) (OB_l dxc) (@Id D (OB_l dxc))) (@Id C (@FOb D C F (OB_l dxc))) *)
(* Goal: @Equal (@Hom C (@FOb D C F (OB_l dxc)) (@Ob_r (Dual D) C dxc)) (@Comp C (@FOb D C F (OB_l dxc)) (@FOb D C F (OB_l dxc)) (@Ob_r (Dual D) C dxc) (@Id C (@FOb D C F (OB_l dxc))) f) f *)
apply Comp_l; apply FId.
(* Goal: @Equal (@Hom D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc))) (@Comp D (@OB_l C D dxc) (@FOb C D G (@Ob_r (Dual D) C dxc)) (@FOb C D G (@Ob_r (Dual D) C dxc)) f (@Id D (@FOb C D G (@Ob_r (Dual D) C dxc)))) f *)
apply Idr1.
Qed.

Canonical Structure FunSET2_l := Build_Functor Fun2_l_comp_law Fun2_l_id_law.

End FunSet2_l.


