From 00b060e4854e5a1ba01746be44ac9deb49d7fbf5 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Tue, 29 Mar 2011 04:37:57 -0700 Subject: [PATCH] rename RepresentableFunctor to HomFunctor --- src/Adjoints_ch9.v | 4 +-- src/Main.v | 2 +- src/RepresentableStructure_ch7_2.v | 64 +++++++++++++++++++----------------- src/Yoneda_ch8.v | 2 +- 4 files changed, 38 insertions(+), 34 deletions(-) diff --git a/src/Adjoints_ch9.v b/src/Adjoints_ch9.v index df870eb..8d947b7 100644 --- a/src/Adjoints_ch9.v +++ b/src/Adjoints_ch9.v @@ -26,8 +26,8 @@ Notation "'η'" := (adj_unit _). (* Lemma homset_adjunction `(C:ECategory(V:=V))`(D:ECategory(V:=V))(L:Func C D)(R:Func D C) : (L -| R) - -> RepresentableFunctorºᑭ _ _ >>>> YonedaBiFunctor D ≃ - RepresentableFunctorºᑭ _ _ >>>> YonedaBiFunctor C. + -> HomFunctorºᑭ _ _ >>>> YonedaBiFunctor D ≃ + HomFunctorºᑭ _ _ >>>> YonedaBiFunctor C. *) (* adjuncts are unique up to natural iso *) (* adjuncts compose *) diff --git a/src/Main.v b/src/Main.v index 5ef4f55..962ed6d 100644 --- a/src/Main.v +++ b/src/Main.v @@ -35,7 +35,7 @@ Require Import Adjoints_ch9. (*Require Import CoqCategory.*) (*Require Import NaturalDeduction.*) (*Require Import NaturalDeductionCategories.*) -(*Require Import CartesianEnrichmentsHaveMonoidalRepresentableFunctors.*) +(*Require Import CartesianEnrichmentsHaveMonoidalHomFunctors.*) (*Require Import Reification.*) (*Require Import GeneralizedArrow.*) (*Require Import ReificationFromGArrow.*) diff --git a/src/RepresentableStructure_ch7_2.v b/src/RepresentableStructure_ch7_2.v index 05da4ee..da3f519 100644 --- a/src/RepresentableStructure_ch7_2.v +++ b/src/RepresentableStructure_ch7_2.v @@ -7,6 +7,7 @@ Require Import Preamble. Require Import Categories_ch1_3. Require Import Functors_ch1_4. Require Import Isomorphisms_ch1_5. +Require Import EpicMonic_ch2_1. Require Import ProductCategories_ch1_6_1. Require Import OppositeCategories_ch1_6_2. Require Import Enrichment_ch2_8. @@ -16,8 +17,6 @@ Require Import NaturalIsomorphisms_ch7_5. Require Import MonoidalCategories_ch7_8. Require Import Coherence_ch7_8. -(* FIXME: an object is a Generator if its covariant representable functor is faithful *) - Section RepresentableStructure. Context `(ec:ECategory(mn:=mn)(V:=V)). @@ -35,24 +34,13 @@ Section RepresentableStructure. apply qq. Qed. - Lemma hom_contravariant_distributes {a b c:ec}{x}(f:a~~{ec}~~>b)(g:b~~{ec}~~>c) - : hom_contravariant (f >>> g) ~~ (hom_contravariant g) >>> (hom_contravariant (a:=x) f). - set (f >>> g) as fg; simpl in fg; unfold fg; clear fg. - unfold hom_contravariant. - repeat setoid_rewrite associativity. - etransitivity; [ idtac | symmetry; apply associativity ]. - apply comp_respects; try reflexivity. - set (@ecomp_is_functorial _ _ _ _ _ _ _ _ _ _ _ _ _ x f g) as qq. - setoid_rewrite juggle2 in qq. - admit. - Qed. - + (* Lemma hom_swap {a b c d:ec}(f:a~~{ec}~~>b)(g:c~~{ec}~~>d) : hom_covariant f >>> hom_contravariant g ~~ hom_contravariant g >>> hom_covariant f. etransitivity. unfold hom_covariant. unfold hom_contravariant. - Admitted. + Defined. Definition YonedaBiFunctor_fmor (a b:ec⁽ºᑭ⁾ ×× ec)(f:a~~{ec⁽ºᑭ⁾ ×× ec}~~>b) : ((fst_obj _ _ a)~~>(snd_obj _ _ a))~~{V}~~>((fst_obj _ _ b)~~>(snd_obj _ _ b)). @@ -94,11 +82,31 @@ Section RepresentableStructure. reflexivity). Defined. - Definition RepresentableFunctorºᑭ (X:ec) : Functor ec⁽ºᑭ⁾ V (fun a => a~~>X) := func_rlecnac X >>>> YonedaBiFunctor. - Definition RepresentableFunctor (X:ec) : Functor ec V (fun a => X~~>a) := - func_llecnac(C:=ec⁽ºᑭ⁾)(D:=ec) X >>>> YonedaBiFunctor. - - Lemma undo_homfunctor `(f:a~~{ec}~~>b) : f ~~ eid _ >>> (RepresentableFunctor a \ f). + Definition HomFunctorºᑭ (X:ec) : Functor ec⁽ºᑭ⁾ V (fun a => a~~>X) := func_rlecnac X >>>> YonedaBiFunctor. + *) + + Definition HomFunctor (X:ec) : Functor ec V (ehom X). + refine {| fmor := @hom_covariant X |}. + intros. + unfold hom_covariant. + apply comp_respects; try reflexivity. + apply comp_respects; try reflexivity. + apply fmor_respects; auto. + intros. + unfold hom_covariant. + apply (epic _ (iso_epic ((pmon_cancelr mn) (X ~~> a)))). + setoid_rewrite <- associativity. + setoid_rewrite <- associativity. + setoid_rewrite iso_comp1. + setoid_rewrite left_identity. + setoid_rewrite right_identity. + apply (@eright_identity). + intros. + symmetry. + apply hom_covariant_distributes. + Defined. + + Lemma undo_homfunctor `(f:a~~{ec}~~>b) : f ~~ eid _ >>> (HomFunctor a \ f). simpl. setoid_rewrite <- associativity. unfold hom_contravariant. @@ -138,7 +146,7 @@ Section RepresentableStructure. End RepresentableStructure. -Opaque RepresentableFunctor. +Opaque HomFunctor. Structure MonoidalEnrichment {e:Enrichment} := { me_enr :=e @@ -146,7 +154,7 @@ Structure MonoidalEnrichment {e:Enrichment} := ; me_f : Functor (e ×× e) e me_fobj ; me_i : e ; me_mon : MonoidalCat e me_fobj me_f me_i -; me_mf : MonoidalFunctor me_mon (enr_v_mon e) (RepresentableFunctor e me_i) +; me_mf : MonoidalFunctor me_mon (enr_v_mon e) (HomFunctor e me_i) }. Implicit Arguments MonoidalEnrichment [ ]. Coercion me_mon : MonoidalEnrichment >-> MonoidalCat. @@ -155,17 +163,13 @@ Coercion me_enr : MonoidalEnrichment >-> Enrichment. (* an enrichment for which hom(I,-) is monoidal, full, faithful, and conservative *) Structure MonicMonoidalEnrichment {e}{me:MonoidalEnrichment e} := { ffme_enr := me -; ffme_mf_full : FullFunctor (RepresentableFunctor e (me_i me)) -; ffme_mf_faithful : FaithfulFunctor (RepresentableFunctor e (me_i me)) -; ffme_mf_conservative : ConservativeFunctor (RepresentableFunctor e (me_i me)) +; ffme_mf_full : FullFunctor (HomFunctor e (me_i me)) +; ffme_mf_faithful : FaithfulFunctor (HomFunctor e (me_i me)) +; ffme_mf_conservative : ConservativeFunctor (HomFunctor e (me_i me)) }. Implicit Arguments MonicMonoidalEnrichment [ ]. Coercion ffme_enr : MonicMonoidalEnrichment >-> MonoidalEnrichment. -Transparent RepresentableFunctor. - -Lemma CartesianEnrMonoidal (e:Enrichment) `(C:CartesianCat(Ob:= _)(Hom:= _)(C:=Underlying (enr_c e))) : MonoidalEnrichment e. - admit. - Defined. +Transparent HomFunctor. Structure SurjectiveMonicMonoidalEnrichment (e:Enrichment) := { smme_se : SurjectiveEnrichment e diff --git a/src/Yoneda_ch8.v b/src/Yoneda_ch8.v index 045c427..d7652da 100644 --- a/src/Yoneda_ch8.v +++ b/src/Yoneda_ch8.v @@ -3,5 +3,5 @@ (*******************************************************************************) (* - Lemma YonedaLemma : forall (A B:ec), (CategoryOfNaturalTransformations (RepresentableFunctor A) (RepresentableFunctor B)) ≅ (B~~>A) + Lemma YonedaLemma : forall (A B:ec), (CategoryOfNaturalTransformations (HomFunctor A) (HomFunctor B)) ≅ (B~~>A) *) -- 1.7.10.4