(* 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        *)
(*****************************************************************************)
(*									     *)
(*	                    Yoneda's Lemma                     		     *)
(*									     *)
(*****************************************************************************)
(*									     *)
(*                           A.SAIBI   May 95				     *)
(*									     *)
(*****************************************************************************)


Require Export HomFunctor_NT.
Require Export CatFunct.
Require Export Functor_dup1.

Set Implicit Arguments.
Unset Strict Implicit.

Section yoneda_lemma.

Variable C : Category.

(* nous voulons de'finir un iso entre NatFun et Ev *)
(* Nous devons d'abord construire une NT YLphi : NatFun -> Ev *)
(* YLphi(a,F) : NaFtun(C(a,-),F) -> F(a) dans SET i.e. que c'est une Map *)

 Section ylphi_tau_def.

 Variables (a : C) (F : Functor C SET).

 Definition YLphi_arrow (T : NT (FunSET a) F) := T a (Id a).

 Lemma YLphi_arrow_map_law : Map_law''0 YLphi_arrow.
 Proof.
(* Goal: @Map_law''0 (@NT_setoid C SET (@FunSET C a) F) (@FOb C SET F a) YLphi_arrow *)
 unfold Map_law''0, YLphi_arrow in |- *; intros T1 T2 H; simpl in |- *.
(* Goal: @Equal (@FOb C SET F a) (@Ap (@FunSET_ob C a a) (@FOb C SET F a) (@ApNT C SET (@FunSET C a) F T1 a) (@Id C a)) (@Ap (@FunSET_ob C a a) (@FOb C SET F a) (@ApNT C SET (@FunSET C a) F T2 a) (@Id C a)) *)
 apply (H a (Id a)).
 Qed.

 Canonical Structure YLphi_tau := Build_Map''0 YLphi_arrow_map_law.

 End ylphi_tau_def.

(* de'montrer que YLphi_tau ve'rifie NT_law *)

Lemma YLphi_nt_law :
 forall (a a' : C) (g : a --> a') (F F' : Functor C SET) 
   (T : NT F F') (U : NT (FunSET a) F),
 YLphi_tau a' F' (NtH g o_NTv U o_NTv T) =_S
 (FMor F g o T a') (YLphi_tau a F U).
Proof.
(* Goal: forall (a a' : Ob C) (g : Carrier (@Hom C a a')) (F F' : Functor C SET) (T : @NT C SET F F') (U : @NT C SET (@FunSET C a) F), @Equal (@FOb C SET F' a') (@Ap''0 (@NT_setoid C SET (@FunSET C a') F') (@FOb C SET F' a') (YLphi_tau a' F') (@CompV_NT C SET (@FunSET C a') (@FunSET C a) F' (@NtH C a' a g) (@CompV_NT C SET (@FunSET C a) F F' U T))) (@Ap (@FOb C SET F a) (@FOb C SET F' a') (@Comp SET (@FOb C SET F a) (@FOb C SET F a') (@FOb C SET F' a') (@FMor C SET F a a' g) (@ApNT C SET F F' T a')) (@Ap''0 (@NT_setoid C SET (@FunSET C a) F) (@FOb C SET F a) (YLphi_tau a F) U)) *)
intros a a' g F F' T U.
unfold YLphi_tau in |- *; simpl in |- *; unfold YLphi_arrow in |- *;
 simpl in |- *. 
(* Goal: @Equal (@FOb C SET F' a') (@Comp_fun (@FunSET_ob C a a') (@FOb C SET F a') (@FOb C SET F' a') (@ApNT C SET (@FunSET C a) F U a') (@ApNT C SET F F' T a') (@NtH_arrow C a' a g a' (@Id C a'))) (@Comp_fun (@FOb C SET F a) (@FOb C SET F a') (@FOb C SET F' a') (@FMor C SET F a a' g) (@ApNT C SET F F' T a') (@Ap (@FunSET_ob C a a) (@FOb C SET F a) (@ApNT C SET (@FunSET C a) F U a) (@Id C a))) *)
unfold NtH_arrow, Comp_fun in |- *.
(* Goal: @Equal (@FOb C SET F a') (@Ap (@FunSET_ob C a a') (@FOb C SET F a') (@ApNT C SET (@FunSET C a) F U a') (@Comp C a a' a' g (@Id C a'))) (@Ap (@FOb C SET (@FunSET C a) a') (@FOb C SET F a') (@ApNT C SET (@FunSET C a) F U a') (@Comp C a a a' (@Id C a) g)) *)
(* Goal: @Equal (@FOb C SET F a') (@Ap (@FOb C SET (@FunSET C a) a') (@FOb C SET F a') (@ApNT C SET (@FunSET C a) F U a') (@Comp C a a a' (@Id C a) g)) (@Ap (@FOb C SET F a) (@FOb C SET F a') (@FMor C SET F a a' g) (@Ap (@FunSET_ob C a a) (@FOb C SET F a) (@ApNT C SET (@FunSET C a) F U a) (@Id C a))) *)
apply Pres1.
(* Goal: @Equal (@FOb C SET F a') (@Ap (@FunSET_ob C a a') (@FOb C SET F a') (@ApNT C SET (@FunSET C a) F U a') (@Comp C a a' a' g (@Id C a'))) (@Ap (@FOb C SET F a) (@FOb C SET F a') (@FMor C SET F a a' g) (@Ap (@FunSET_ob C a a) (@FOb C SET F a) (@ApNT C SET (@FunSET C a) F U a) (@Id C a))) *)
apply Trans with (U a' (Id a o g)).
(* Goal: @Equal (@FOb C SET F a') (@Ap (@FunSET_ob C a a') (@FOb C SET F a') (@ApNT C SET (@FunSET C a) F U a') (@Comp C a a' a' g (@Id C a'))) (@Ap (@FOb C SET (@FunSET C a) a') (@FOb C SET F a') (@ApNT C SET (@FunSET C a) F U a') (@Comp C a a a' (@Id C a) g)) *)
(* Goal: @Equal (@FOb C SET F a') (@Ap (@FOb C SET (@FunSET C a) a') (@FOb C SET F a') (@ApNT C SET (@FunSET C a) F U a') (@Comp C a a a' (@Id C a) g)) (@Ap (@FOb C SET F a) (@FOb C SET F a') (@FMor C SET F a a' g) (@Ap (@FunSET_ob C a a) (@FOb C SET F a) (@ApNT C SET (@FunSET C a) F U a) (@Id C a))) *)
apply Pres1.
(* Goal: @Equal (@FOb C SET (@FunSET C a) a') (@Comp C a a' a' g (@Id C a')) (@Comp C a a a' (@Id C a) g) *)
(* Goal: @Equal (@FOb C SET F a') (@Ap (@FOb C SET (@FunSET C a) a') (@FOb C SET F a') (@ApNT C SET (@FunSET C a) F U a') (@Comp C a a a' (@Id C a) g)) (@Ap (@FOb C SET F a) (@FOb C SET F a') (@FMor C SET F a a' g) (@Ap (@FunSET_ob C a a) (@FOb C SET F a) (@ApNT C SET (@FunSET C a) F U a) (@Id C a))) *)
simpl in |- *; unfold FunSET_ob in |- *.
(* Goal: @Equal (@Hom C a a') (@Comp C a a' a' g (@Id C a')) (@Comp C a a a' (@Id C a) g) *)
(* Goal: @Equal (@FOb C SET F a') (@Ap (@FOb C SET (@FunSET C a) a') (@FOb C SET F a') (@ApNT C SET (@FunSET C a) F U a') (@Comp C a a a' (@Id C a) g)) (@Ap (@FOb C SET F a) (@FOb C SET F a') (@FMor C SET F a a' g) (@Ap (@FunSET_ob C a a) (@FOb C SET F a) (@ApNT C SET (@FunSET C a) F U a) (@Id C a))) *)
apply Idrl.
(* Goal: @Equal (@FOb C SET F a') (@Ap (@FOb C SET (@FunSET C a) a') (@FOb C SET F a') (@ApNT C SET (@FunSET C a) F U a') (@Comp C a a a' (@Id C a) g)) (@Ap (@FOb C SET F a) (@FOb C SET F a') (@FMor C SET F a a' g) (@Ap (@FunSET_ob C a a) (@FOb C SET F a) (@ApNT C SET (@FunSET C a) F U a) (@Id C a))) *)
apply (Prf_NT_law U g (Id a)).
Qed.

(* Construisons YL_psi l'inverse de YLphi *)

(* YL_psi est une NT Ev-->NatFun *)

(* ((YL_psi<a,F>)x)b est une Map entre C(a,b) et F(b) *)

 Section ylpsi_tau_def.

 Variables (a : C) (F : Functor C SET).

  Section ylpsi_arrow_def.

  Variable x : F a.

   Section ylpsi_map1_def.

   Variable b : C.

   Definition YLpsi_arrow1 (f : a --> b) := FMor F f x.

   Lemma YLpsi_arrow1_map_law : Map_law YLpsi_arrow1.
   Proof.
(* Goal: @Map_law (@Hom C a b) (@FOb C SET F b) YLpsi_arrow1 *)
   unfold Map_law in |- *.
(* Goal: forall (x y : Carrier (@Hom C a b)) (_ : @Equal (@Hom C a b) x y), @Equal (@FOb C SET F b) (YLpsi_arrow1 x) (YLpsi_arrow1 y) *)
   intros y z H; unfold YLpsi_arrow1 in |- *.
(* Goal: @Equal (@FOb C SET F b) (@Ap (@FOb C SET F a) (@FOb C SET F b) (@FMor C SET F a b y) x) (@Ap (@FOb C SET F a) (@FOb C SET F b) (@FMor C SET F a b z) x) *)
   apply (Pres (FMap F a b) H x).
   Qed.

   Canonical Structure YLpsi_map1 :=
     Build_Map (A:=FunSET a b) YLpsi_arrow1_map_law.

   End ylpsi_map1_def.

(* (YLpsi<a,F>)x est une NT entre C(a,-) et F *)

  Lemma YLpsi_map1_nt_law : NT_law YLpsi_map1.
  Proof.
(* Goal: @NT_law C SET (@FunSET C a) F YLpsi_map1 *)
  unfold NT_law in |- *.
(* Goal: forall (a0 b : Ob C) (f : Carrier (@Hom C a0 b)), @Equal (@Hom SET (@FOb C SET (@FunSET C a) a0) (@FOb C SET F b)) (@Comp SET (@FOb C SET (@FunSET C a) a0) (@FOb C SET (@FunSET C a) b) (@FOb C SET F b) (@FMor C SET (@FunSET C a) a0 b f) (YLpsi_map1 b)) (@Comp SET (@FOb C SET (@FunSET C a) a0) (@FOb C SET F a0) (@FOb C SET F b) (YLpsi_map1 a0) (@FMor C SET F a0 b f)) *)
  intros b c f; unfold YLpsi_map1, YLpsi_arrow1 in |- *; simpl in |- *.
(* Goal: @Ext (@FunSET_ob C a b) (@FOb C SET F c) (@Comp SET (@FunSET_ob C a b) (@FunSET_ob C a c) (@FOb C SET F c) (@FMor C SET (@FunSET C a) b c f) (@Build_Map (@FunSET_ob C a c) (@FOb C SET F c) (fun f : Carrier (@Hom C a c) => @Ap (@FOb C SET F a) (@FOb C SET F c) (@FMor C SET F a c f) x) (@YLpsi_arrow1_map_law c))) (@Comp SET (@FunSET_ob C a b) (@FOb C SET F b) (@FOb C SET F c) (@Build_Map (@FunSET_ob C a b) (@FOb C SET F b) (fun f : Carrier (@Hom C a b) => @Ap (@FOb C SET F a) (@FOb C SET F b) (@FMor C SET F a b f) x) (@YLpsi_arrow1_map_law b)) (@FMor C SET F b c f)) *)
  unfold Ext, FunSET_ob in |- *; intro g; simpl in |- *.
(* Goal: @Equal (@FOb C SET F c) (@Ap (@FOb C SET F a) (@FOb C SET F c) (@FMor C SET F a c (@FunSET_mor1 C a b c f g)) x) (@Comp_fun (@Hom C a b) (@FOb C SET F b) (@FOb C SET F c) (@Build_Map (@Hom C a b) (@FOb C SET F b) (fun f : Carrier (@Hom C a b) => @Ap (@FOb C SET F a) (@FOb C SET F b) (@FMor C SET F a b f) x) (@YLpsi_arrow1_map_law b)) (@FMor C SET F b c f) g) *)
  unfold FunSET_mor, Comp_fun in |- *; simpl in |- *.
(* Goal: @Equal (@FOb C SET F c) (@Ap (@FOb C SET F a) (@FOb C SET F c) (@FMor C SET F a c (@FunSET_mor1 C a b c f g)) x) (@Ap (@FOb C SET F b) (@FOb C SET F c) (@FMor C SET F b c f) (@Ap (@FOb C SET F a) (@FOb C SET F b) (@FMor C SET F a b g) x)) *)
  apply (Prf_Fcomp_law F g f x).
  Qed.

  Canonical Structure YLpsi_arrow := Build_NT YLpsi_map1_nt_law.

  End ylpsi_arrow_def.

(* YLpsi<a,F> est une Map entre F(a) et NatFun(C(a,-),F) *)

 Lemma YLpsi_arrow_map_law : Map_law0'' YLpsi_arrow.
 Proof.
(* Goal: @Map_law0'' (@FOb C SET F a) (@NT_setoid C SET (@FunSET C a) F) YLpsi_arrow *)
 unfold Map_law0'', YLpsi_arrow in |- *. 
(* Goal: forall (x y : Carrier (@FOb C SET F a)) (_ : @Equal (@FOb C SET F a) x y), @Equal'' (@NT_setoid C SET (@FunSET C a) F) (@Build_NT C SET (@FunSET C a) F (YLpsi_map1 x) (@YLpsi_map1_nt_law x)) (@Build_NT C SET (@FunSET C a) F (YLpsi_map1 y) (@YLpsi_map1_nt_law y)) *)
 intros x y H.
 unfold YLpsi_map1, YLpsi_arrow1 in |- *; simpl in |- *;
  unfold Equal_NT in |- *; simpl in |- *.
(* Goal: forall a0 : Ob C, @Ext (@FunSET_ob C a a0) (@FOb C SET F a0) (@Build_Map (@FunSET_ob C a a0) (@FOb C SET F a0) (fun f : Carrier (@Hom C a a0) => @Ap (@FOb C SET F a) (@FOb C SET F a0) (@FMor C SET F a a0 f) x) (@YLpsi_arrow1_map_law x a0)) (@Build_Map (@FunSET_ob C a a0) (@FOb C SET F a0) (fun f : Carrier (@Hom C a a0) => @Ap (@FOb C SET F a) (@FOb C SET F a0) (@FMor C SET F a a0 f) y) (@YLpsi_arrow1_map_law y a0)) *)
 intro a0; unfold Ext in |- *; simpl in |- *; intro f.
(* Goal: @Equal (@FOb C SET F a0) (@Ap (@FOb C SET F a) (@FOb C SET F a0) (@FMor C SET F a a0 f) x) (@Ap (@FOb C SET F a) (@FOb C SET F a0) (@FMor C SET F a a0 f) y) *)
 apply Pres1; assumption.
 Qed.

 Canonical Structure YLpsi_tau : Map0'' (F a) (NT_setoid (FunSET a) F) :=
   YLpsi_arrow_map_law.

 End ylpsi_tau_def.

Lemma YLpsi_nt_law :
 forall (a a' : C) (g : a --> a') (F F' : Functor C SET) 
   (T : NT F F') (x : F a) (b : C) (f : a' --> b),
 YLpsi_tau a' F' ((FMor F g o T a') x) b f =_S
 (NtH g o_NTv YLpsi_tau a F x o_NTv T) b f.

Proof.
(* Goal: forall (a a' : Ob C) (g : Carrier (@Hom C a a')) (F F' : Functor C SET) (T : @NT C SET F F') (x : Carrier (@FOb C SET F a)) (b : Ob C) (f : Carrier (@Hom C a' b)), @Equal (@FOb C SET F' b) (@Ap (@FOb C SET (@FunSET C a') b) (@FOb C SET F' b) (@ApNT C SET (@FunSET C a') F' (@Ap0'' (@FOb C SET F' a') (@NT_setoid C SET (@FunSET C a') F') (YLpsi_tau a' F') (@Ap (@FOb C SET F a) (@FOb C SET F' a') (@Comp SET (@FOb C SET F a) (@FOb C SET F a') (@FOb C SET F' a') (@FMor C SET F a a' g) (@ApNT C SET F F' T a')) x)) b) f) (@Ap (@FOb C SET (@FunSET C a') b) (@FOb C SET F' b) (@ApNT C SET (@FunSET C a') F' (@CompV_NT C SET (@FunSET C a') (@FunSET C a) F' (@NtH C a' a g) (@CompV_NT C SET (@FunSET C a) F F' (@Ap0'' (@FOb C SET F a) (@NT_setoid C SET (@FunSET C a) F) (YLpsi_tau a F) x) T)) b) f) *)
intros a a' g F F' T x b f.
unfold YLpsi_tau in |- *; simpl in |- *; unfold Comp_fun in |- *;
 simpl in |- *.
(* Goal: @Equal (@FOb C SET F' b) (@YLpsi_arrow1 a' F' (@Ap (@FOb C SET F a') (@FOb C SET F' a') (@ApNT C SET F F' T a') (@Ap (@FOb C SET F a) (@FOb C SET F a') (@FMor C SET F a a' g) x)) b f) (@Ap (@FOb C SET F b) (@FOb C SET F' b) (@ApNT C SET F F' T b) (@YLpsi_arrow1 a F x b (@NtH_arrow C a' a g b f))) *)
unfold YLpsi_arrow1, NtH_arrow in |- *.
(* Goal: @Equal (@FOb C SET F' b) (@Ap (@FOb C SET F' a') (@FOb C SET F' b) (@FMor C SET F' a' b f) (@Ap (@FOb C SET F a') (@FOb C SET F' a') (@ApNT C SET F F' T a') (@Ap (@FOb C SET F a) (@FOb C SET F a') (@FMor C SET F a a' g) x))) (@Ap (@FOb C SET F b) (@FOb C SET F' b) (@ApNT C SET F F' T b) (@Ap (@FOb C SET F a) (@FOb C SET F b) (@FMor C SET F a b (@Comp C a a' b g f)) x)) *)
apply Trans with (T b (FMor F f (FMor F g x))).
(* Goal: @Equal (@FOb C SET F' b) (@Ap (@FOb C SET F' a') (@FOb C SET F' b) (@FMor C SET F' a' b f) (@Ap (@FOb C SET F a') (@FOb C SET F' a') (@ApNT C SET F F' T a') (@Ap (@FOb C SET F a) (@FOb C SET F a') (@FMor C SET F a a' g) x))) (@Ap (@FOb C SET F b) (@FOb C SET F' b) (@ApNT C SET F F' T b) (@Ap (@FOb C SET F a') (@FOb C SET F b) (@FMor C SET F a' b f) (@Ap (@FOb C SET F a) (@FOb C SET F a') (@FMor C SET F a a' g) x))) *)
(* Goal: @Equal (@FOb C SET F' b) (@Ap (@FOb C SET F b) (@FOb C SET F' b) (@ApNT C SET F F' T b) (@Ap (@FOb C SET F a') (@FOb C SET F b) (@FMor C SET F a' b f) (@Ap (@FOb C SET F a) (@FOb C SET F a') (@FMor C SET F a a' g) x))) (@Ap (@FOb C SET F b) (@FOb C SET F' b) (@ApNT C SET F F' T b) (@Ap (@FOb C SET F a) (@FOb C SET F b) (@FMor C SET F a b (@Comp C a a' b g f)) x)) *)
generalize (Prf_NT_law T f (FMor F g x)).
(* Goal: forall _ : @Equal (@FOb C SET F' b) (@Ap (@FOb C SET F a') (@FOb C SET F' b) (@Comp SET (@FOb C SET F a') (@FOb C SET F b) (@FOb C SET F' b) (@FMor C SET F a' b f) (@ApNT C SET F F' T b)) (@Ap (@FOb C SET F a) (@FOb C SET F a') (@FMor C SET F a a' g) x)) (@Ap (@FOb C SET F a') (@FOb C SET F' b) (@Comp SET (@FOb C SET F a') (@FOb C SET F' a') (@FOb C SET F' b) (@ApNT C SET F F' T a') (@FMor C SET F' a' b f)) (@Ap (@FOb C SET F a) (@FOb C SET F a') (@FMor C SET F a a' g) x)), @Equal (@FOb C SET F' b) (@Ap (@FOb C SET F' a') (@FOb C SET F' b) (@FMor C SET F' a' b f) (@Ap (@FOb C SET F a') (@FOb C SET F' a') (@ApNT C SET F F' T a') (@Ap (@FOb C SET F a) (@FOb C SET F a') (@FMor C SET F a a' g) x))) (@Ap (@FOb C SET F b) (@FOb C SET F' b) (@ApNT C SET F F' T b) (@Ap (@FOb C SET F a') (@FOb C SET F b) (@FMor C SET F a' b f) (@Ap (@FOb C SET F a) (@FOb C SET F a') (@FMor C SET F a a' g) x))) *)
(* Goal: @Equal (@FOb C SET F' b) (@Ap (@FOb C SET F b) (@FOb C SET F' b) (@ApNT C SET F F' T b) (@Ap (@FOb C SET F a') (@FOb C SET F b) (@FMor C SET F a' b f) (@Ap (@FOb C SET F a) (@FOb C SET F a') (@FMor C SET F a a' g) x))) (@Ap (@FOb C SET F b) (@FOb C SET F' b) (@ApNT C SET F F' T b) (@Ap (@FOb C SET F a) (@FOb C SET F b) (@FMor C SET F a b (@Comp C a a' b g f)) x)) *)
unfold NT_law in |- *; simpl in |- *; unfold Comp_fun in |- *; intro H. 
(* Goal: @Equal (@FOb C SET F' b) (@Ap (@FOb C SET F' a') (@FOb C SET F' b) (@FMor C SET F' a' b f) (@Ap (@FOb C SET F a') (@FOb C SET F' a') (@ApNT C SET F F' T a') (@Ap (@FOb C SET F a) (@FOb C SET F a') (@FMor C SET F a a' g) x))) (@Ap (@FOb C SET F b) (@FOb C SET F' b) (@ApNT C SET F F' T b) (@Ap (@FOb C SET F a') (@FOb C SET F b) (@FMor C SET F a' b f) (@Ap (@FOb C SET F a) (@FOb C SET F a') (@FMor C SET F a a' g) x))) *)
(* Goal: @Equal (@FOb C SET F' b) (@Ap (@FOb C SET F b) (@FOb C SET F' b) (@ApNT C SET F F' T b) (@Ap (@FOb C SET F a') (@FOb C SET F b) (@FMor C SET F a' b f) (@Ap (@FOb C SET F a) (@FOb C SET F a') (@FMor C SET F a a' g) x))) (@Ap (@FOb C SET F b) (@FOb C SET F' b) (@ApNT C SET F F' T b) (@Ap (@FOb C SET F a) (@FOb C SET F b) (@FMor C SET F a b (@Comp C a a' b g f)) x)) *)
apply Sym; apply H.
(* Goal: @Equal (@FOb C SET F c) (@Ap (@FOb C SET F a) (@FOb C SET F c) (@FMor C SET F a c (@FunSET_mor1 C a b c f g)) x) (@Ap (@FOb C SET F b) (@FOb C SET F c) (@FMor C SET F b c f) (@Ap (@FOb C SET F a) (@FOb C SET F b) (@FMor C SET F a b g) x)) *)
apply Pres1; apply Sym; apply (Prf_Fcomp_law F g f x).
Qed.

(* L'objectif final e'tant de prouver que YLphi et YLpsi sont iso *)
(* pour cela on va prouver d'abord que YLphi<a,F> et YLpsi<a,F> sont iso *)

Lemma YonedaLemma :
 forall (a : C) (F : Functor C SET),
 AreBij0'' (YLpsi_tau a F) (YLphi_tau a F).
Proof.
(* Goal: forall (a : Ob C) (F : Functor C SET), @AreBij0'' (@FOb C SET F a) (@NT_setoid C SET (@FunSET C a) F) (YLpsi_tau a F) (YLphi_tau a F) *)
intros a F; unfold AreBij0'' in |- *; split; simpl in |- *.
intro x; unfold YLphi_arrow in |- *; simpl in |- *;
 unfold YLpsi_arrow1 in |- *.
(* Goal: @Equal (@FOb C SET F a) (@Ap (@FOb C SET F a) (@FOb C SET F a) (@FMor C SET F a a (@Id C a)) x) x *)
(* Goal: forall b : @NT C SET (@FunSET C a) F, @Equal_NT C SET (@FunSET C a) F (@YLpsi_arrow a F (@YLphi_arrow a F b)) b *)
apply Trans with (Id (F a) x).
(* Goal: @Equal (@FOb C SET F a) (@Ap (@FOb C SET F a) (@FOb C SET F a) (@FMor C SET F a a (@Id C a)) x) (@Ap (@FOb C SET F a) (@FOb C SET F a) (@Id SET (@FOb C SET F a)) x) *)
(* Goal: @Equal (@FOb C SET F a) (@Ap (@FOb C SET F a) (@FOb C SET F a) (@Id SET (@FOb C SET F a)) x) x *)
(* Goal: forall b : @NT C SET (@FunSET C a) F, @Equal_NT C SET (@FunSET C a) F (@YLpsi_arrow a F (@YLphi_arrow a F b)) b *)
apply (Prf_Fid_law F a x).
(* Goal: @Equal (@FOb C SET F a) (@Ap (@FOb C SET F a) (@FOb C SET F a) (@Id SET (@FOb C SET F a)) x) x *)
(* Goal: forall b : @NT C SET (@FunSET C a) F, @Equal_NT C SET (@FunSET C a) F (@YLpsi_arrow a F (@YLphi_arrow a F b)) b *)
apply Refl.
(* Goal: forall b : @NT C SET (@FunSET C a) F, @Equal_NT C SET (@FunSET C a) F (@YLpsi_arrow a F (@YLphi_arrow a F b)) b *)
intro T; unfold YLpsi_arrow, Equal_NT in |- *; simpl in |- *.
(* Goal: forall a0 : Ob C, @Ext (@FunSET_ob C a a0) (@FOb C SET F a0) (@YLpsi_map1 a F (@YLphi_arrow a F T) a0) (@ApNT C SET (@FunSET C a) F T a0) *)
intro b; unfold YLpsi_map1, Ext in |- *; simpl in |- *.
(* Goal: forall x : Carrier (@FunSET_ob C a b), @Equal (@FOb C SET F b) (@YLpsi_arrow1 a F (@YLphi_arrow a F T) b x) (@Ap (@FunSET_ob C a b) (@FOb C SET F b) (@ApNT C SET (@FunSET C a) F T b) x) *)
unfold FunSET_ob in |- *; intro f.
(* Goal: @Equal (@FOb C SET F b) (@YLpsi_arrow1 a F (@YLphi_arrow a F T) b f) (@Ap (@Hom C a b) (@FOb C SET F b) (@ApNT C SET (@FunSET C a) F T b) f) *)
unfold YLpsi_arrow1, YLphi_arrow in |- *.
(* Goal: @Equal (@FOb C SET F b) (@Ap (@FOb C SET F a) (@FOb C SET F b) (@FMor C SET F a b f) (@Ap (@FOb C SET (@FunSET C a) a) (@FOb C SET F a) (@ApNT C SET (@FunSET C a) F T a) (@Id C a))) (@Ap (@Hom C a b) (@FOb C SET F b) (@ApNT C SET (@FunSET C a) F T b) f) *)
generalize (Prf_NT_law T f (Id a)).
simpl in |- *; unfold Comp_fun in |- *; simpl in |- *;
 unfold FunSET_mor1 in |- *; intro H.
(* Goal: @Equal (@FOb C SET F b) (@Ap (@FOb C SET F a) (@FOb C SET F b) (@FMor C SET F a b f) (@Ap (@FunSET_ob C a a) (@FOb C SET F a) (@ApNT C SET (@FunSET C a) F T a) (@Id C a))) (@Ap (@Hom C a b) (@FOb C SET F b) (@ApNT C SET (@FunSET C a) F T b) f) *)
apply Trans with (T b (Id a o f)).
(* Goal: @Equal (@FOb C SET F b) (@Ap (@FOb C SET F a) (@FOb C SET F b) (@FMor C SET F a b f) (@Ap (@FunSET_ob C a a) (@FOb C SET F a) (@ApNT C SET (@FunSET C a) F T a) (@Id C a))) (@Ap (@FOb C SET (@FunSET C a) b) (@FOb C SET F b) (@ApNT C SET (@FunSET C a) F T b) (@Comp C a a b (@Id C a) f)) *)
(* Goal: @Equal (@FOb C SET F b) (@Ap (@FOb C SET (@FunSET C a) b) (@FOb C SET F b) (@ApNT C SET (@FunSET C a) F T b) (@Comp C a a b (@Id C a) f)) (@Ap (@Hom C a b) (@FOb C SET F b) (@ApNT C SET (@FunSET C a) F T b) f) *)
apply Sym; exact H.
(* Goal: @Equal (@FOb C SET F b) (@Ap (@FOb C SET (@FunSET C a) b) (@FOb C SET F b) (@ApNT C SET (@FunSET C a) F T b) (@Comp C a a b (@Id C a) f)) (@Ap (@Hom C a b) (@FOb C SET F b) (@ApNT C SET (@FunSET C a) F T b) f) *)
apply Pres1; apply Idl.
Qed.

End yoneda_lemma.