src/GeneralizedArrowCategory.v

   1 (*********************************************************************************************************************************)
   2 (* CategoryOfGeneralizedArrows:                                                                                                  *)
   3 (*                                                                                                                               *)
   4 (*   There is a category whose objects are surjective monic monoidal enrichments (SMME's) and whose morphisms                    *)
   5 (*   are generalized  Arrows                                                                                                     *)
   6 (*                                                                                                                               *)
   7 (*********************************************************************************************************************************)
   8
   9 Generalizable All Variables.
  10 Require Import Preamble.
  11 Require Import General.
  12 Require Import Categories_ch1_3.
  13 Require Import Functors_ch1_4.
  14 Require Import Isomorphisms_ch1_5.
  15 Require Import ProductCategories_ch1_6_1.
  16 Require Import OppositeCategories_ch1_6_2.
  17 Require Import Enrichment_ch2_8.
  18 Require Import Subcategories_ch7_1.
  19 Require Import NaturalTransformations_ch7_4.
  20 Require Import NaturalIsomorphisms_ch7_5.
  21 Require Import BinoidalCategories.
  22 Require Import PreMonoidalCategories.
  23 Require Import MonoidalCategories_ch7_8.
  24 Require Import Coherence_ch7_8.
  25 Require Import Enrichment_ch2_8.
  26 Require Import RepresentableStructure_ch7_2.
  27 Require Import GeneralizedArrow.
  28 Require Import WeakFunctorCategory.
  29 Require Import SmallSMMEs.
  30
  31 (*
  32  * Technically reifications form merely a *semicategory* (no identity
  33  * maps), but one can always freely adjoin identity maps (and nothing
  34  * else) to a semicategory to get a category whose non-identity-map
  35  * portion is identical to the original semicategory
  36  *
  37  * Also, technically this category has ALL enrichments (not just the
  38  * surjective monic monoidal ones), though there maps OUT OF only the
  39  * surjective enrichments and INTO only the monic monoidal
  40  * enrichments.  It's a big pain to do this in Coq, but sort of might
  41  * matter in real life: a language with really severe substructural
  42  * restrictions might fail to be monoidally enriched, meaning we can't
  43  * use it as a host language.  But that's for the next paper...
  44  *)
  45 Inductive GeneralizedArrowOrIdentity : SMMEs -> SMMEs -> Type :=
  46   | gaoi_id   : forall smme:SMMEs,                             GeneralizedArrowOrIdentity smme smme
  47   | gaoi_ga : forall s1 s2:SMMEs, GeneralizedArrow s1 s2  -> GeneralizedArrowOrIdentity s1   s2.
  48
  49 Definition generalizedArrowOrIdentityFobj (s1 s2:SMMEs) (f:GeneralizedArrowOrIdentity s1 s2) : s1 -> s2 :=
  50   match f in GeneralizedArrowOrIdentity S1 S2 return S1 -> S2 with
  51   | gaoi_id  s       => fun x => x
  52   | gaoi_ga s1 s2 f  => fun a => ehom(ECategory:=s2) (mon_i (smme_mon s2)) (ga_functor_obj f a)
  53   end.
  54
  55 Definition generalizedArrowOrIdentityFunc s1 s2 (f:GeneralizedArrowOrIdentity s1 s2)
  56   : Functor s1 s2 (generalizedArrowOrIdentityFobj _ _ f) :=
  57   match f with
  58   | gaoi_id  s       => functor_id _
  59   | gaoi_ga s1 s2 f  => ga_functor f >>>> HomFunctor s2 (mon_i s2)
  60   end.
  61
  62 Definition compose_generalizedArrows (s0 s1 s2:SMMEs) :
  63   GeneralizedArrow s0 s1 -> GeneralizedArrow s1 s2 -> GeneralizedArrow s0 s2.
  64   intro g01.
  65   intro g12.
  66   refine
  67     {| ga_functor          := g01 >>>> HomFunctor s1 (mon_i s1) >>>> g12 |}.
  68     apply MonoidalFunctorsCompose.
  69     apply MonoidalFunctorsCompose.
  70     apply (ga_functor_monoidal g01).
  71     apply (me_mf s1).
  72     apply (ga_functor_monoidal g12).
  73     Defined.
  74
  75 Definition generalizedArrowOrIdentityComp
  76   : forall s1 s2 s3, GeneralizedArrowOrIdentity s1 s2 -> GeneralizedArrowOrIdentity s2 s3 -> GeneralizedArrowOrIdentity s1 s3.
  77   intros.
  78   destruct X.
  79     apply X0.
  80   destruct X0.
  81     apply (gaoi_ga _ _ g).
  82     apply (gaoi_ga _ _ (compose_generalizedArrows _ _ _ g g0)).
  83     Defined.
  84
  85 Definition MorphismsOfCategoryOfGeneralizedArrows : @SmallFunctors SMMEs.
  86   refine {| small_func      := GeneralizedArrowOrIdentity
  87           ; small_func_id   := fun s => gaoi_id s
  88           ; small_func_func := fun smme1 smme2 f => generalizedArrowOrIdentityFunc _ _ f
  89           ; small_func_comp := generalizedArrowOrIdentityComp
  90          |}; intros; simpl.
  91   apply if_id.
  92   destruct f as [|fobj f]; simpl in *.
  93     apply if_inv.
  94     apply if_left_identity.
  95   destruct g as [|gobj g]; simpl in *.
  96     apply if_inv.
  97     apply if_right_identity.
  98   unfold mf_F.
  99   idtac.
 100   unfold mf_f.
 101   apply if_associativity.
 102   Defined.
 103
 104 Definition CategoryOfGeneralizedArrows :=
 105   WeakFunctorCategory MorphismsOfCategoryOfGeneralizedArrows.