src/ReificationCategory.v

   1 (*********************************************************************************************************************************)
   2 (* ReificationCategory:                                                                                                          *)
   3 (*                                                                                                                               *)
   4 (*   There is a category whose objects are surjective monic monoidal enrichments (SMME's) and whose morphisms                    *)
   5 (*   are reifications                                                                                                            *)
   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 Reification.
  26 Require Import WeakFunctorCategory.
  27 Require Import SmallSMMEs.
  28
  29 Inductive ReificationOrIdentity : SMMEs -> SMMEs -> Type :=
  30   | roi_id   : forall smme:SMMEs,                                  ReificationOrIdentity smme smme
  31   | roi_reif : forall s1 s2:SMMEs, Reification s1 s2 (mon_i s2) -> ReificationOrIdentity s1   s2.
  32
  33 Definition reificationOrIdentityFobj s1 s2 (f:ReificationOrIdentity s1 s2) : s1 -> s2 :=
  34   match f with
  35   | roi_id   s       => (fun x => x)
  36   | roi_reif s1 s2 f => reification_rstar_obj f
  37   end.
  38
  39 Definition reificationOrIdentityFunc
  40   : forall s1 s2 (f:ReificationOrIdentity s1 s2), Functor (enr_v s1) (enr_v s2) (reificationOrIdentityFobj s1 s2 f).
  41   intros.
  42   destruct f.
  43   apply functor_id.
  44   unfold reificationOrIdentityFobj.
  45   apply (reification_rstar_f r).
  46   Defined.
  47
  48 Definition compose_reifications (s0 s1 s2:SMMEs) :
  49   Reification s0 s1 (mon_i s1) -> Reification s1 s2 (mon_i s2) -> Reification s0 s2 (mon_i s2).
  50   intros.
  51   refine
  52     {| reification_rstar   := MonoidalFunctorsCompose _ _ _ _ _ (reification_rstar X) (reification_rstar X0)
  53      ; reification_r       := fun K => (reification_r X K) >>>> (reification_r X0 (mon_i s1))
  54     |}.
  55   intro K.
  56   set (ni_associativity (reification_r X K) (reification_r X0 (mon_i s1)) (RepresentableFunctor s2 (mon_i s2))) as q.
  57   eapply ni_comp.
  58   apply q.
  59   clear q.
  60   set (reification_commutes X K) as comm1.
  61   set (reification_commutes X0 (mon_i s1)) as comm2.
  62   set (RepresentableFunctor s0 K) as a in *.
  63   set (reification_rstar_f X) as a' in *.
  64   set (reification_rstar_f X0) as x in *.
  65   set (reification_r X K) as b in *.
  66   set (reification_r X0 (mon_i s1)) as c in *.
  67   set (RepresentableFunctor s2 (mon_i s2)) as c' in *.
  68   set (RepresentableFunctor s1 (mon_i s1)) as b' in *.
  69   apply (ni_comp(F2:=b >>>> (b' >>>> x))).
  70   apply (@ni_respects _ _ _ _ _ _ _ _ _ _ b _ b _ (c >>>> c') _ (b' >>>> x)).
  71   apply ni_id.
  72   apply comm2.
  73   eapply ni_comp.
  74   eapply ni_inv.
  75   apply (ni_associativity b b' x).
  76   eapply ni_inv.
  77   eapply ni_comp.
  78   eapply ni_inv.
  79   apply (ni_associativity a a' x).
  80   apply (@ni_respects _ _ _ _ _ _ _ _ _ _ (a >>>> a') _ (b >>>> b') _ x _ x).
  81   apply ni_inv.
  82   apply comm1.
  83   apply ni_id.
  84   Defined.
  85
  86 Definition reificationOrIdentityComp
  87   : forall s1 s2 s3, ReificationOrIdentity s1 s2 -> ReificationOrIdentity s2 s3 -> ReificationOrIdentity s1 s3.
  88   intros.
  89   destruct X.
  90     apply X0.
  91   destruct X0.
  92     apply (roi_reif _ _ r).
  93     apply (roi_reif _ _ (compose_reifications _ _ _ r r0)).
  94     Defined.
  95
  96 Definition MorphismsOfCategoryOfReifications : @SmallFunctors SMMEs.
  97   refine {| small_func      := ReificationOrIdentity
  98           ; small_func_id   := fun s => roi_id s
  99           ; small_func_func := fun smme1 smme2 f => reificationOrIdentityFunc _ _ f
 100           ; small_func_comp := reificationOrIdentityComp
 101          |}; intros; simpl.
 102   apply if_id.
 103   destruct f as [|fobj f]; simpl in *.
 104     apply if_inv.
 105     apply if_left_identity.
 106   destruct g as [|gobj g]; simpl in *.
 107     apply if_inv.
 108     apply if_right_identity.
 109   apply if_id.
 110   Defined.
 111
 112 Definition CategoryOfReifications :=
 113   WeakFunctorCategory MorphismsOfCategoryOfReifications.