add Retraction, SMME, make Enrichment a parameter

diff --git a/src/Enrichment_ch2_8.v b/src/Enrichment_ch2_8.v
index 32a7701..b821599 100644 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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.