Require Import WeakFunctorCategory.
Require Import SmallSMMEs.
+(*
+ * Technically reifications form merely a *semicategory* (no identity
+ * maps), but one can always freely adjoin identity maps (and nothing
+ * else) to a semicategory to get a category whose non-identity-map
+ * portion is identical to the original semicategory
+ *
+ * Also, technically this category has ALL enrichments (not just the
+ * surjective monic monoidal ones), though there maps OUT OF only the
+ * surjective enrichments and INTO only the monic monoidal
+ * enrichments. It's a big pain to do this in Coq, but sort of might
+ * matter in real life: a language with really severe substructural
+ * restrictions might fail to be monoidally enriched, meaning we can't
+ * use it as a host language. But that's for the next paper...
+ *)
Inductive GeneralizedArrowOrIdentity : SMMEs -> SMMEs -> Type :=
| gaoi_id : forall smme:SMMEs, GeneralizedArrowOrIdentity smme smme
| gaoi_ga : forall s1 s2:SMMEs, GeneralizedArrow s1 s2 -> GeneralizedArrowOrIdentity s1 s2.
-Definition generalizedArrowOrIdentityFunc
- : forall s1 s2, GeneralizedArrowOrIdentity s1 s2 -> { fobj : _ & Functor s1 s2 fobj }.
- intros.
- destruct X.
- exists (fun x => x).
- apply functor_id.
- eapply existT.
- apply (g >>>> RepresentableFunctor s2 (mon_i s2)).
- Defined.
+Definition generalizedArrowOrIdentityFobj (s1 s2:SMMEs) (f:GeneralizedArrowOrIdentity s1 s2) : s1 -> s2 :=
+ match f in GeneralizedArrowOrIdentity S1 S2 return S1 -> S2 with
+ | gaoi_id s => fun x => x
+ | gaoi_ga s1 s2 f => fun a => ehom(ECategory:=s2) (mon_i (smme_mon s2)) (ga_functor_obj f a)
+ end.
+
+Definition generalizedArrowOrIdentityFunc s1 s2 (f:GeneralizedArrowOrIdentity s1 s2)
+ : Functor s1 s2 (generalizedArrowOrIdentityFobj _ _ f) :=
+ match f with
+ | gaoi_id s => functor_id _
+ | gaoi_ga s1 s2 f => ga_functor f >>>> RepresentableFunctor s2 (mon_i s2)
+ end.
Definition compose_generalizedArrows (s0 s1 s2:SMMEs) :
GeneralizedArrow s0 s1 -> GeneralizedArrow s1 s2 -> GeneralizedArrow s0 s2.
Definition MorphismsOfCategoryOfGeneralizedArrows : @SmallFunctors SMMEs.
refine {| small_func := GeneralizedArrowOrIdentity
; small_func_id := fun s => gaoi_id s
- ; small_func_func := fun smme1 smme2 f => projT2 (generalizedArrowOrIdentityFunc _ _ f)
+ ; small_func_func := fun smme1 smme2 f => generalizedArrowOrIdentityFunc _ _ f
; small_func_comp := generalizedArrowOrIdentityComp
|}; intros; simpl.
apply if_id.
apply (fmor_preserves_comp reification)).
Defined.
-(*
- Definition FullImage_Monoidal
- `(F:@Functor Cobj CHom C1 Dobj DHom D1 Fobj) `(mc:MonoidalCat D1 Mobj MF) : MonoidalCat (FullImage F) Mobj.
-
- Definition step1_functor_monoidal : MonoidalFunctor (enr_v_mon K) step1_functor.
- admit.
- Defined.
-*)
Definition step1_niso : reification ≃ step1_functor >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C))).
exists (fun c1 => homset_tensor_iso c1).
abstract (intros;
Definition garrow_functor := step1_functor >>>> step2_functor.
- Definition garrow_from_reification : GeneralizedArrow K C.
- refine {| ga_functor := garrow_functor |}.
- (*
- unfold garrow_functor.
- apply MonoidalFunctorsCompose.
- apply MonoidalFunctorsCompose.
- *)
+ Lemma garrow_functor_monoidal_niso
+ : (garrow_functor **** garrow_functor) >>>> (mon_f C) <~~~> (mon_f (enr_v_mon K)) >>>> garrow_functor.
+ admit.
+ Defined.
+ Lemma garrow_functor_monoidal_iso
+ : mon_i C ≅ garrow_functor (mon_i (enr_v_mon K)).
+ admit.
+ Defined.
+
+ Instance garrow_functor_monoidal : MonoidalFunctor (enr_v_mon K) C garrow_functor :=
+ { mf_coherence := garrow_functor_monoidal_niso
+ ; mf_id := garrow_functor_monoidal_iso
+ }.
+ admit.
+ admit.
admit.
Defined.
+ Definition garrow_from_reification : GeneralizedArrow K C.
+ refine
+ {| ga_functor := garrow_functor
+ ; ga_functor_monoidal := garrow_functor_monoidal
+ |}.
+ Defined.
+
End GArrowFromReification.
Opaque homset_tensor_iso.
Require Import WeakFunctorCategory.
Require Import SmallSMMEs.
+(* Technically reifications form merely a *semicategory* (no identity
+ * maps), but one can always freely adjoin identity maps (and nothing
+ * else) to a semicategory to get a category whose non-identity-map
+ * portion is identical to the original semicategory
+ *
+ * Also, technically this category has ALL enrichments (not just the
+ * surjective monic monoidal ones), though there maps OUT OF only the
+ * surjective enrichments and INTO only the monic monoidal
+ * enrichments. It's a big pain to do this in Coq, but sort of might
+ * matter in real life: a language with really severe substructural
+ * restrictions might fail to be monoidally enriched, meaning we can't
+ * use it as a host language. But that's for the next paper...
+ *)
Inductive ReificationOrIdentity : SMMEs -> SMMEs -> Type :=
| roi_id : forall smme:SMMEs, ReificationOrIdentity smme smme
| roi_reif : forall s1 s2:SMMEs, Reification s1 s2 (mon_i s2) -> ReificationOrIdentity s1 s2.
Reification s0 s1 (mon_i s1) -> Reification s1 s2 (mon_i s2) -> Reification s0 s2 (mon_i s2).
intros.
refine
- {| reification_rstar := MonoidalFunctorsCompose _ _ _ _ _ (reification_rstar X) (reification_rstar X0)
+ {| reification_rstar_f := reification_rstar_f X >>>> reification_rstar_f X0
+ ; reification_rstar := MonoidalFunctorsCompose _ _ _ _ _ (reification_rstar X) (reification_rstar X0)
; reification_r := fun K => (reification_r X K) >>>> (reification_r X0 (mon_i s1))
|}.
intro K.
Require Import ReificationsEquivalentToGeneralizedArrows.
Require Import WeakFunctorCategory.
-
Section ReificationsIsomorphicToGeneralizedArrows.
- Definition M1 (c1 c2 : SmallSMMEs.SMMEs) :
+ Definition M1 {c1 c2 : SmallSMMEs.SMMEs} :
(c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) ->
(c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2).
intro GA.
apply g.
Defined.
+ Lemma invert_ga : forall (a: SMME)
+ (f:a~~{MorphismsOfCategoryOfGeneralizedArrows}~~>a),
+ (f = gaoi_id _) \/ (exists f', f = gaoi_ga _ _ f').
+ admit.
+ Qed.
+
+ Lemma invert_reif : forall (a: SMME)
+ (f:a~~{MorphismsOfCategoryOfReifications}~~>a),
+ (f = roi_id _) \/ (exists f', f = roi_reif _ _ f').
+ admit.
+ Qed.
+
+ Definition M1_Functor : Functor MorphismsOfCategoryOfGeneralizedArrows MorphismsOfCategoryOfReifications (fun x => x).
+ refine {| fmor := fun a b f => M1 f |}.
+ intros.
+ unfold hom in *.
+ unfold eqv in *.
+ simpl in *.
+ destruct f.
+ set (invert_ga _ f') as q.
+ destruct q; subst.
+ apply if_id.
+ simpl in *.
+ destruct H0; subst.
+ apply H.
+ simpl in *.
+ destruct f'; simpl in *.
+ apply H.
+ apply H.
+ intros; simpl.
+ apply if_id.
+ intros.
+ simpl.
+ destruct f; simpl.
+ apply if_id.
+ destruct g; simpl.
+ apply if_id.
+ unfold mf_f; simpl.
+ apply (if_associativity
+ ((ga_functor g0 >>>> RepresentableFunctor s0 (mon_i s0))) (ga_functor g) (RepresentableFunctor s2 (me_i s2))).
+ Defined.
+
Definition M2 (c1 c2 : SmallSMMEs.SMMEs) :
(c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2) ->
(c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2).
apply (garrow_from_reification s1 s2 r).
Defined.
- (*
+ Lemma M2_respects :
+ forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b),
+ f ~~ f' ->
+ M2 a b f ~~ M2 a b f'.
+ intros.
+ unfold hom in *.
+ unfold eqv in *.
+ simpl in *.
+ destruct f.
+ set (invert_reif _ f') as q.
+ destruct q; subst.
+ apply if_id.
+ simpl in *.
+ destruct H0; subst.
+ simpl in *.
+ unfold garrow_functor.
+ unfold step2_functor.
+ apply (if_comp H).
+ clear H.
+ apply (if_comp (@step1_niso _ smme _ _ smme x)).
+ apply if_inv.
+ apply (@roundtrip_lemma _ smme _ _ smme x).
+ simpl in *.
+ destruct f'; simpl in *.
+ apply if_inv.
+ apply if_inv in H.
+ apply (if_comp H).
+ clear H.
+ unfold garrow_functor.
+ unfold step2_functor.
+ apply (if_comp (@step1_niso _ smme _ _ smme r)).
+ apply if_inv.
+ apply (@roundtrip_lemma _ smme _ _ smme r).
+ simpl in *.
+ unfold garrow_functor.
+ unfold step2_functor.
+ apply if_inv in H.
+ set (if_comp H (@step1_niso _ s1 _ _ s2 r)) as yy.
+ set (if_comp (if_inv (@step1_niso _ s1 _ _ s2 r0)) yy) as yy'.
+ apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r)).
+ apply if_inv.
+ apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r0)).
+ apply yy'.
+ Qed.
- * Oh my, this is massively embarrassing. In the paper I claim
- * that Generalized Arrows form a category and Reifications form a
- * category, when in fact they form merely a SEMIcategory (see
- * http://ncatlab.org/nlab/show/semicategory) since we cannot be sure that the identity functor on the
+ Definition M2_Functor : Functor MorphismsOfCategoryOfReifications MorphismsOfCategoryOfGeneralizedArrows (fun x => x).
+ refine {| fmor := fun a b f => M2 _ _ f |}.
+ apply M2_respects.
+ intros; simpl; apply if_id.
+ intros.
+ simpl.
+ destruct f; simpl.
+ apply if_id.
+ destruct g; simpl.
+ apply if_id.
+ unfold mf_f; simpl.
+ apply (if_respects
+ (F0:=((garrow_functor s1 s0 r >>>> RepresentableFunctor s0 (mon_i s0)) >>>> garrow_functor s0 s2 r0))
+ (F1:=(garrow_functor s1 s2 (compose_reifications s1 s0 s2 r r0)))
+ (G0:=(RepresentableFunctor s2 (mon_i s2)))
+ (G1:=(RepresentableFunctor s2 (mon_i s2))));
+ [ idtac | apply if_id ].
+ admit.
+ Defined.
Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfGeneralizedArrows CategoryOfReifications.
- apply WeakFunctorCategoriesIsomorphic with (M1:=M1) (M2:=M2).
- destruct g.
- intros.
- simpl.
- simpl in H.
- split f.
- destruct f.
- dependent destruction f.
- intros until g.
- destruct f.
- simpl.
- inversion g.
- destruct f as [ ] _eqn.
- destruct g as [ ] _eqn.
- destruct g.
- subst.
- simpl.
- case g.
- simpl.
- inversion g; subst; intros.
- destruct g.
- Qed.
+ refine {| ic_f := M1_Functor ; ic_g := M2_Functor |}.
+ unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
+ unfold hom in *.
+ set (@roundtrip_garrow_to_garrow _ a _ _ b) as q.
+ destruct f; simpl in *.
+ apply H.
+ apply if_inv.
+ apply (if_comp (if_inv H)).
+ clear H.
+ unfold mf_f in q.
+ apply (if_respects(F0:=ga_functor g)(F1:=garrow_functor s1 s2 (reification_from_garrow s1 s2 g))
+ (G0:=RepresentableFunctor s2 (mon_i s2))(G1:=RepresentableFunctor s2 (mon_i s2))).
+ apply q.
+ apply if_id.
+
+ unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
+ unfold hom in *.
+ set (@roundtrip_reification_to_reification _ a _ _ b) as q.
+ destruct f; simpl.
+ apply H.
+ apply if_inv.
+ apply (if_comp (if_inv H)).
+ clear H.
+ simpl.
+ unfold mf_f; simpl.
+ simpl in q.
+ unfold mf_f in q.
+ simpl in q.
+ apply q.
+ Qed.
End ReificationsIsomorphicToGeneralizedArrows.