(* 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 : Yoneda's Functor                               *)
(*                                                                           *)
(*          Amokrane Saibi May 1994                                          *)
(*                                                                           *)
(*****************************************************************************)


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


Set Implicit Arguments.
Unset Strict Implicit.

(* Fonctor Y:C^o-->[C==>SET] *)

Section yoneda_functor.

Variable C : Category.

 Section funy_map_def.

 Variable a b : C.

 Lemma FunY_map_law : Map_law0'' (NtH (C:=C) (b:=a) (a:=b)).
 Proof.
(* Goal: @Map_law0'' (@Hom C b a) (@NT_setoid C SET (@FunSET C a) (@FunSET C b)) (@NtH C a b) *)
 unfold Map_law0'', NtH in |- *; simpl in |- *.
(* Goal: forall (a b : Ob C) (f g : Carrier (@DHom C a b)) (_ : @Equal_NT C SET (@FunSET C a) (@FunSET C b) (@FMor0'' (Dual C) (FUNCT C SET) FunY a b f) (@FMor0'' (Dual C) (FUNCT C SET) FunY a b g)), @Equal (@DHom C a b) f g *)
 unfold Equal_NT in |- *; simpl in |- *.
(* Goal: forall a0 : Ob C, @Ext (@FunSET_ob C a a0) (@FunSET_ob C b a0) (@ApNT C SET (@FunSET C a) (@FunSET C b) h a0) (@NtH_map C a b (@Ap (@FunSET_ob C a a) (@FunSET_ob C b a) (@ApNT C SET (@FunSET C a) (@FunSET C b) h a) (@Id C a)) a0) *)
 unfold Ext in |- *; simpl in |- *.
(* Goal: forall (a a0 : Ob C) (x : Carrier (@FunSET_ob C a a0)), @Equal (@FunSET_ob C a a0) (@NtH_arrow C a a (@Id C a) a0 x) (@Id_fun (@FunSET_ob C a a0) x) *)
 unfold NtH_arrow in |- *; simpl in |- *.
(* Goal: forall (x y : Carrier (@Hom C b a)) (_ : @Equal (@Hom C b a) x y) (a0 : Ob C) (x0 : Carrier (@FunSET_ob C a a0)), @Equal (@FunSET_ob C b a0) (@Comp C b a a0 x x0) (@Comp C b a a0 y x0) *)
 unfold FunSET_ob in |- *; intros.
(* Goal: @Equal (@Hom C b a0) (@Comp C b a a0 x x0) (@Comp C b a a0 y x0) *)
 apply Comp_r; assumption.
 Qed.

 Canonical Structure FunY_map := Build_Map0'' FunY_map_law.

 End funy_map_def.

Lemma FunY_comp_law : Fcomp_law0'' (C:=Dual C) FunY_map.
Proof.
(* Goal: @Fcomp_law0'' (Dual C) (FUNCT C SET) (@FunSET C) FunY_map *)
unfold Fcomp_law0'' in |- *; simpl in |- *.
(* Goal: forall (a b : Ob C) (f g : Carrier (@DHom C a b)) (_ : @Equal_NT C SET (@FunSET C a) (@FunSET C b) (@FMor0'' (Dual C) (FUNCT C SET) FunY a b f) (@FMor0'' (Dual C) (FUNCT C SET) FunY a b g)), @Equal (@DHom C a b) f g *)
unfold Equal_NT in |- *; simpl in |- *.
(* Goal: forall a0 : Ob C, @Ext (@FunSET_ob C a a0) (@FunSET_ob C b a0) (@ApNT C SET (@FunSET C a) (@FunSET C b) h a0) (@NtH_map C a b (@Ap (@FunSET_ob C a a) (@FunSET_ob C b a) (@ApNT C SET (@FunSET C a) (@FunSET C b) h a) (@Id C a)) a0) *)
unfold Ext in |- *; simpl in |- *.
(* Goal: forall (a a0 : Ob C) (x : Carrier (@FunSET_ob C a a0)), @Equal (@FunSET_ob C a a0) (@NtH_arrow C a a (@Id C a) a0 x) (@Id_fun (@FunSET_ob C a a0) x) *)
unfold NtH_arrow in |- *; simpl in |- *.
(* Goal: forall (a b c : Ob C) (f : Carrier (@DHom C a b)) (g : Carrier (@DHom C b c)) (a0 : Ob C) (x : Carrier (@FunSET_ob C a a0)), @Equal (@FunSET_ob C c a0) (@Comp C c a a0 (@Comp (Dual C) a b c f g) x) (@Comp C c b a0 g (@Comp C b a a0 f x)) *)
unfold FunSET_ob, DHom in |- *.
(* Goal: forall (a b c : Ob C) (f : Carrier (@Hom C b a)) (g : Carrier (@Hom C c b)) (a0 : Ob C) (x : Carrier (@Hom C a a0)), @Equal (@Hom C c a0) (@Comp C c a a0 (@Comp (Dual C) a b c f g) x) (@Comp C c b a0 g (@Comp C b a a0 f x)) *)
intros a b c f g d h; apply Sym.
(* Goal: @Equal (@Hom C c d) (@Comp C c b d g (@Comp C b a d f h)) (@Comp C c a d (@Comp (Dual C) a b c f g) h) *)
exact (Prf_ass g f h).
Qed.

Lemma FunY_id_law : Fid_law0'' (C:=Dual C) FunY_map.
Proof.
(* Goal: @Fid_law0'' (Dual C) (FUNCT C SET) (@FunSET C) FunY_map *)
unfold Fid_law0'' in |- *; simpl in |- *.
(* Goal: forall (a b : Ob C) (f g : Carrier (@DHom C a b)) (_ : @Equal_NT C SET (@FunSET C a) (@FunSET C b) (@FMor0'' (Dual C) (FUNCT C SET) FunY a b f) (@FMor0'' (Dual C) (FUNCT C SET) FunY a b g)), @Equal (@DHom C a b) f g *)
unfold Equal_NT in |- *; simpl in |- *. 
(* Goal: forall a0 : Ob C, @Ext (@FunSET_ob C a a0) (@FunSET_ob C b a0) (@ApNT C SET (@FunSET C a) (@FunSET C b) h a0) (@NtH_map C a b (@Ap (@FunSET_ob C a a) (@FunSET_ob C b a) (@ApNT C SET (@FunSET C a) (@FunSET C b) h a) (@Id C a)) a0) *)
unfold Ext in |- *; simpl in |- *.
(* Goal: forall (a a0 : Ob C) (x : Carrier (@FunSET_ob C a a0)), @Equal (@FunSET_ob C a a0) (@NtH_arrow C a a (@Id C a) a0 x) (@Id_fun (@FunSET_ob C a a0) x) *)
unfold NtH_arrow in |- *; simpl in |- *.
(* Goal: forall (a b : Ob C) (f g : Carrier (@Hom C b a)) (_ : forall (a0 : Ob C) (x : Carrier (@FunSET_ob C a a0)), @Equal (@FunSET_ob C b a0) (@Comp C b a a0 f x) (@Comp C b a a0 g x)), @Equal (@Hom C b a) f g *)
unfold FunSET_ob in |- *.
(* Goal: forall (a a0 : Ob C) (x : Carrier (@Hom C a a0)), @Equal (@Hom C a a0) (@Comp C a a a0 (@Id C a) x) (@Id_fun (@Hom C a a0) x) *)
unfold Id_fun in |- *; simpl in |- *.
(* Goal: forall (a a0 : Ob C) (x : Carrier (@Hom C a a0)), @Equal (@Hom C a a0) (@Comp C a a a0 (@Id C a) x) x *)
intros a b f; unfold Comp in |- *; apply (Prf_idl (c:=C)).
Qed.

Canonical Structure FunY := Build_Functor0'' FunY_comp_law FunY_id_law.      

(* lemma : Y is full *)

Lemma Y_full :
 let f := fun (a b : C) (h : NT (FunSET a) (FunSET b)) => h a (Id a) in
 Full_law0'' (F:=FunY) f.
Proof.
(* Goal: let f := fun (a b : Ob C) (h : @NT C SET (@FunSET C a) (@FunSET C b)) => @Ap (@FOb C SET (@FunSET C a) a) (@FOb C SET (@FunSET C b) a) (@ApNT C SET (@FunSET C a) (@FunSET C b) h a) (@Id C a) in @Full_law0'' (Dual C) (FUNCT C SET) FunY f *)
unfold Full_law0'' in |- *; simpl in |- *; intros a b h.
(* Goal: forall (a b : Ob C) (f g : Carrier (@DHom C a b)) (_ : @Equal_NT C SET (@FunSET C a) (@FunSET C b) (@FMor0'' (Dual C) (FUNCT C SET) FunY a b f) (@FMor0'' (Dual C) (FUNCT C SET) FunY a b g)), @Equal (@DHom C a b) f g *)
unfold Equal_NT in |- *; simpl in |- *.
(* Goal: forall a0 : Ob C, @Ext (@FunSET_ob C a a0) (@FunSET_ob C b a0) (@ApNT C SET (@FunSET C a) (@FunSET C b) h a0) (@NtH_map C a b (@Ap (@FunSET_ob C a a) (@FunSET_ob C b a) (@ApNT C SET (@FunSET C a) (@FunSET C b) h a) (@Id C a)) a0) *)
unfold Ext in |- *; simpl in |- *.
(* Goal: forall (a b : Ob C) (f g : Carrier (@Hom C b a)) (_ : forall (a0 : Ob C) (x : Carrier (@FunSET_ob C a a0)), @Equal (@FunSET_ob C b a0) (@NtH_arrow C a b f a0 x) (@NtH_arrow C a b g a0 x)), @Equal (@Hom C b a) f g *)
unfold NtH_arrow in |- *.
(* Goal: forall (a b : Ob C) (f g : Carrier (@Hom C b a)) (_ : forall (a0 : Ob C) (x : Carrier (@FunSET_ob C a a0)), @Equal (@FunSET_ob C b a0) (@Comp C b a a0 f x) (@Comp C b a a0 g x)), @Equal (@Hom C b a) f g *)
unfold FunSET_ob in |- *.
(* Goal: forall (a0 : Ob C) (x : Carrier (@Hom C a a0)), @Equal (@Hom C b a0) (@Ap (@Hom C a a0) (@Hom C b a0) (@ApNT C SET (@FunSET C a) (@FunSET C b) h a0) x) (@Comp C b a a0 (@Ap (@Hom C a a) (@Hom C b a) (@ApNT C SET (@FunSET C a) (@FunSET C b) h a) (@Id C a)) x) *)
intros c f; simpl in |- *.
(* Goal: @Equal (@Hom C b c) (@Ap (@Hom C a c) (@Hom C b c) (@ApNT C SET (@FunSET C a) (@FunSET C b) h c) f) (@Comp C b a c (@Ap (@Hom C a a) (@Hom C b a) (@ApNT C SET (@FunSET C a) (@FunSET C b) h a) (@Id C a)) f) *)
(* *) apply Trans with (h c (Id a o f)).
(* Goal: @Equal (@FOb C SET (@FunSET C b) c) (@Ap (@Hom C a c) (@Hom C b c) (@ApNT C SET (@FunSET C a) (@FunSET C b) h c) f) (@Ap (@FOb C SET (@FunSET C a) c) (@FOb C SET (@FunSET C b) c) (@ApNT C SET (@FunSET C a) (@FunSET C b) h c) (@Comp C a a c (@Id C a) f)) *)
(* Goal: @Equal (@FOb C SET (@FunSET C b) c) (@Ap (@FOb C SET (@FunSET C a) c) (@FOb C SET (@FunSET C b) c) (@ApNT C SET (@FunSET C a) (@FunSET C b) h c) (@Comp C a a c (@Id C a) f)) (@Comp C b a c (@Ap (@Hom C a a) (@Hom C b a) (@ApNT C SET (@FunSET C a) (@FunSET C b) h a) (@Id C a)) f) *)
apply Pres1.
apply Sym; unfold Comp in |- *; simpl in |- *; unfold FunSET_ob in |- *;
 apply (Prf_idl (c:=C)).
(* Goal: @Equal (@FOb C SET (@FunSET C b) c) (@Ap (@FOb C SET (@FunSET C a) c) (@FOb C SET (@FunSET C b) c) (@ApNT C SET (@FunSET C a) (@FunSET C b) h c) (@Comp C a a c (@Id C a) f)) (@Comp C b a c (@Ap (@Hom C a a) (@Hom C b a) (@ApNT C SET (@FunSET C a) (@FunSET C b) h a) (@Id C a)) f) *)
apply (Prf_NT_law h f (Id a)).
Qed.

(* Y is faithful *)

Lemma Y_faithful : Faithful_law0'' FunY.
Proof.
(* Goal: @Faithful_law0'' (Dual C) (FUNCT C SET) FunY *)
unfold Faithful_law0'' in |- *; simpl in |- *.
(* Goal: forall (a b : Ob C) (f g : Carrier (@DHom C a b)) (_ : @Equal_NT C SET (@FunSET C a) (@FunSET C b) (@FMor0'' (Dual C) (FUNCT C SET) FunY a b f) (@FMor0'' (Dual C) (FUNCT C SET) FunY a b g)), @Equal (@DHom C a b) f g *)
unfold Equal_NT in |- *; simpl in |- *.
(* Goal: forall (a b : Ob C) (f g : Carrier (@DHom C a b)) (_ : forall a0 : Ob C, @Ext (@FunSET_ob C a a0) (@FunSET_ob C b a0) (@NtH_map C a b f a0) (@NtH_map C a b g a0)), @Equal (@DHom C a b) f g *)
unfold Ext in |- *; simpl in |- *; unfold DHom in |- *.
(* Goal: forall (a b : Ob C) (f g : Carrier (@Hom C b a)) (_ : forall (a0 : Ob C) (x : Carrier (@FunSET_ob C a a0)), @Equal (@FunSET_ob C b a0) (@NtH_arrow C a b f a0 x) (@NtH_arrow C a b g a0 x)), @Equal (@Hom C b a) f g *)
unfold NtH_arrow in |- *.
(* Goal: forall (a b : Ob C) (f g : Carrier (@Hom C b a)) (_ : forall (a0 : Ob C) (x : Carrier (@FunSET_ob C a a0)), @Equal (@FunSET_ob C b a0) (@Comp C b a a0 f x) (@Comp C b a a0 g x)), @Equal (@Hom C b a) f g *)
unfold FunSET_ob in |- *.
(* Goal: forall (a b : Ob C) (f g : Carrier (@Hom C b a)) (_ : forall (a0 : Ob C) (x : Carrier (@Hom C a a0)), @Equal (@Hom C b a0) (@Comp C b a a0 f x) (@Comp C b a a0 g x)), @Equal (@Hom C b a) f g *)
intros a b f g H.
(* Goal: @Equal (@Hom C b a) f g *)
(* *) apply Trans with (g o Id a).
(* Goal: @Equal (@Hom C b a) f (@Comp C b a a g (@Id C a)) *)
(* Goal: @Equal (@Hom C b a) (@Comp C b a a g (@Id C a)) g *)
(* *) apply Trans with (f o Id a).
(* Goal: @Equal (@Hom C b a) f (@Comp C b a a f (@Id C a)) *)
(* Goal: @Equal (@Hom C b a) (@Comp C b a a f (@Id C a)) (@Comp C b a a g (@Id C a)) *)
(* Goal: @Equal (@Hom C b a) (@Comp C b a a g (@Id C a)) g *)
apply Idr.
(* Goal: @Equal (@Hom C b a) (@Comp C b a a f (@Id C a)) (@Comp C b a a g (@Id C a)) *)
(* Goal: @Equal (@Hom C b a) (@Comp C b a a g (@Id C a)) g *)
apply H.
(* Goal: @Equal (@Hom C b a) (@Comp C b a a g (@Id C a)) g *)
apply Idr1.
Qed.

End yoneda_functor.


