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 MonoidalCategories_ch7_8.
  22 Require Import Coherence_ch7_8.
  23 Require Import Enrichment_ch2_8.
  24 Require Import RepresentableStructure_ch7_2.
  25 Require Import GeneralizedArrow.
  26 Require Import WeakFunctorCategory.
  27 Require Import SmallSMMEs.
  28
  29 Inductive GeneralizedArrowOrIdentity : SMMEs -> SMMEs -> Type :=
  30   | gaoi_id   : forall smme:SMMEs,                             GeneralizedArrowOrIdentity smme smme
  31   | gaoi_ga : forall s1 s2:SMMEs, GeneralizedArrow s1 s2  -> GeneralizedArrowOrIdentity s1   s2.
  32
  33 Definition generalizedArrowOrIdentityFunc
  34   : forall s1 s2, GeneralizedArrowOrIdentity s1 s2 -> { fobj : _ & Functor s1 s2 fobj }.
  35   intros.
  36   destruct X.
  37   exists (fun x => x).
  38   apply functor_id.
  39   eapply existT.
  40   apply (g >>>> RepresentableFunctor s2 (mon_i s2)).
  41   Defined.
  42
  43 Definition compose_generalizedArrows (s0 s1 s2:SMMEs) :
  44   GeneralizedArrow s0 s1 -> GeneralizedArrow s1 s2 -> GeneralizedArrow s0 s2.
  45   intro g01.
  46   intro g12.
  47   refine
  48     {| ga_functor          := g01 >>>> RepresentableFunctor s1 (mon_i s1) >>>> g12 |}.
  49     apply MonoidalFunctorsCompose.
  50     apply MonoidalFunctorsCompose.
  51     apply (ga_functor_monoidal g01).
  52     apply (me_mf s1).
  53     apply (ga_functor_monoidal g12).
  54     Defined.
  55
  56 Definition generalizedArrowOrIdentityComp
  57   : forall s1 s2 s3, GeneralizedArrowOrIdentity s1 s2 -> GeneralizedArrowOrIdentity s2 s3 -> GeneralizedArrowOrIdentity s1 s3.
  58   intros.
  59   destruct X.
  60     apply X0.
  61   destruct X0.
  62     apply (gaoi_ga _ _ g).
  63     apply (gaoi_ga _ _ (compose_generalizedArrows _ _ _ g g0)).
  64     Defined.
  65
  66 Definition MorphismsOfCategoryOfGeneralizedArrows : @SmallFunctors SMMEs.
  67   refine {| small_func      := GeneralizedArrowOrIdentity
  68           ; small_func_id   := fun s => gaoi_id s
  69           ; small_func_func := fun smme1 smme2 f => projT2 (generalizedArrowOrIdentityFunc _ _ f)
  70           ; small_func_comp := generalizedArrowOrIdentityComp
  71          |}; intros; simpl.
  72   apply if_id.
  73   destruct f as [|fobj f]; simpl in *.
  74     apply if_inv.
  75     apply if_left_identity.
  76   destruct g as [|gobj g]; simpl in *.
  77     apply if_inv.
  78     apply if_right_identity.
  79   unfold mf_F.
  80   idtac.
  81   unfold mf_f.
  82   apply if_associativity.
  83   Defined.
  84
  85 Definition CategoryOfGeneralizedArrows :=
  86   WeakFunctorCategory MorphismsOfCategoryOfGeneralizedArrows.