From 107e8eb4dc6e893c3dd93535c5343eba204659a8 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sat, 26 Mar 2011 00:06:26 -0700 Subject: [PATCH] add Retraction, SMME, make Enrichment a parameter --- src/Enrichment_ch2_8.v | 12 ++++----- src/Functors_ch1_4.v | 2 -- src/NaturalIsomorphisms_ch7_5.v | 10 ++++++++ src/RepresentableStructure_ch7_2.v | 48 +++++++++++++++++++++++++++--------- 4 files changed, 52 insertions(+), 20 deletions(-) diff --git a/src/Enrichment_ch2_8.v b/src/Enrichment_ch2_8.v index 32a7701..b821599 100644 --- a/src/Enrichment_ch2_8.v +++ b/src/Enrichment_ch2_8.v @@ -374,14 +374,14 @@ Structure Enrichment := Coercion enr_c : Enrichment >-> ECategory. (* an enrichment for which every object of the enriching category is the tensor of finitely many hom-objects *) -Structure SurjectiveEnrichment := -{ se_enr : Enrichment -; se_decomp : @treeDecomposition (enr_v se_enr) (option ((enr_c_obj se_enr)*(enr_c_obj se_enr))) +Structure SurjectiveEnrichment (e:Enrichment) := +{ se_enr := e +; se_decomp : @treeDecomposition (enr_v e) (option ((enr_c_obj e)*(enr_c_obj e))) (fun t => match t with - | None => enr_v_i se_enr - | Some x => match x with pair y z => enr_c_hom se_enr y z end + | None => enr_v_i e + | Some x => match x with pair y z => enr_c_hom e y z end end) - (fun d1 d2:enr_v se_enr => enr_v_fobj se_enr (pair_obj d1 d2)) + (fun d1 d2:enr_v e => enr_v_fobj e (pair_obj d1 d2)) }. Coercion se_enr : SurjectiveEnrichment >-> Enrichment. diff --git a/src/Functors_ch1_4.v b/src/Functors_ch1_4.v index 78f4b59..176563c 100644 --- a/src/Functors_ch1_4.v +++ b/src/Functors_ch1_4.v @@ -103,12 +103,10 @@ Definition EqualFunctors `{C1:Category}`{C2:Category}{F1obj}(F1:Functor C1 C2 F1 forall a b (f f':a~~{C1}~~>b), f~~f' -> heq_morphisms (F1 \ f) (F2 \ f'). Notation "f ~~~~ g" := (EqualFunctors f g) (at level 45). -(* Class IsomorphicCategories `(C:Category)`(D:Category){Fobj}{Gobj}(F:Functor C D Fobj)(G:Functor D C Gobj) := { ic_forward : F >>>> G ~~~~ functor_id C ; ic_backward : G >>>> F ~~~~ functor_id D }. -*) (* this causes Coq to die: *) (* Definition IsomorphicCategories := Isomorphic (CategoryOfCategories). *) diff --git a/src/NaturalIsomorphisms_ch7_5.v b/src/NaturalIsomorphisms_ch7_5.v index 3371671..90ce326 100644 --- a/src/NaturalIsomorphisms_ch7_5.v +++ b/src/NaturalIsomorphisms_ch7_5.v @@ -251,3 +251,13 @@ Section ni_prod_comp. split; reflexivity. Defined. End ni_prod_comp. + +Structure Retraction `{C:Category} `{D:Category} := +{ retraction_section_fobj : C -> D +; retraction_section : Functor C D retraction_section_fobj +; retraction_retraction_fobj : D -> C +; retraction_retraction : Functor D C retraction_retraction_fobj +; retraction_composes : retraction_section >>>> retraction_retraction ≃ functor_id _ +}. +Implicit Arguments Retraction [ [Ob] [Hom] [Ob0] [Hom0] ]. +Coercion retraction_section : Retraction >-> Functor. diff --git a/src/RepresentableStructure_ch7_2.v b/src/RepresentableStructure_ch7_2.v index 3dd7b78..10f9bdd 100644 --- a/src/RepresentableStructure_ch7_2.v +++ b/src/RepresentableStructure_ch7_2.v @@ -140,23 +140,47 @@ Section RepresentableStructure. End RepresentableStructure. Opaque RepresentableFunctor. -Structure MonoidalEnrichment := -{ me_enr : Enrichment -; me_fobj : prod_obj me_enr me_enr -> me_enr -; me_f : Functor (me_enr ×× me_enr) me_enr me_fobj -; me_i : me_enr -; me_mon : MonoidalCat me_enr me_fobj me_f me_i -; me_mf : MonoidalFunctor me_mon (enr_v_mon me_enr) (RepresentableFunctor me_enr me_i) +Structure MonoidalEnrichment {e:Enrichment} := +{ me_enr :=e +; me_fobj : prod_obj e e -> e +; 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) }. +Implicit Arguments MonoidalEnrichment [ ]. Coercion me_mon : MonoidalEnrichment >-> MonoidalCat. Coercion me_enr : MonoidalEnrichment >-> Enrichment. (* an enrichment for which hom(I,-) is monoidal, full, faithful, and conservative *) -Structure MonicMonoidalEnrichment := -{ ffme_enr : MonoidalEnrichment -; ffme_mf_full : FullFunctor (RepresentableFunctor ffme_enr (me_i ffme_enr)) -; ffme_mf_faithful : FaithfulFunctor (RepresentableFunctor ffme_enr (me_i ffme_enr)) -; ffme_mf_conservative : ConservativeFunctor (RepresentableFunctor ffme_enr (me_i ffme_enr)) +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)) }. +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. + +Structure SurjectiveMonicMonoidalEnrichment (e:Enrichment) := +{ smme_se : SurjectiveEnrichment e +; smme_monoidal : MonoidalEnrichment e +; smme_me : MonicMonoidalEnrichment _ smme_monoidal +}. +Coercion smme_se : SurjectiveMonicMonoidalEnrichment >-> SurjectiveEnrichment. +Coercion smme_me : SurjectiveMonicMonoidalEnrichment >-> MonicMonoidalEnrichment. + +(* like SurjectiveMonicMonoidalEnrichment, but the Enrichment is a field, not a parameter *) +Structure SMME := +{ smme_e : Enrichment +; smme_mon : MonoidalEnrichment smme_e +; smme_me : MonicMonoidalEnrichment smme_mon +}. +Coercion smme_e : SMME >-> Enrichment. +Coercion smme_mon : SMME >-> MonoidalEnrichment smme_e. +Coercion smme_me : SMME >-> MonicMonoidalEnrichment smme_mon. -- 1.7.10.4