(*
Require Import HaskStrongCategory.
*)
-Require Import ReificationsEquivalentToGeneralizedArrows.
+Require Import ReificationsIsomorphicToGeneralizedArrows.
Open Scope string_scope.
Extraction Language Haskell.
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_from_reification : GeneralizedArrow K C.
refine {| ga_functor := garrow_functor |}.
+ (*
+ unfold garrow_functor.
+ apply MonoidalFunctorsCompose.
+ apply MonoidalFunctorsCompose.
+ *)
admit.
Defined.
--- /dev/null
+(*********************************************************************************************************************************)
+(* SemiCategory: *)
+(* *)
+(* Same as a category, but without identity maps. See *)
+(* *)
+(* http://ncatlab.org/nlab/show/semicategory *)
+(* *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+
+Class SemiCategory (Ob:Type)(Hom:Ob->Ob->Type) :=
+{ semi_hom := Hom
+; semi_ob := Ob
+; semi_comp : forall {a}{b}{c}, Hom a b -> Hom b c -> Hom a c
+; semi_eqv : forall a b, (Hom a b) -> (Hom a b) -> Prop
+; semi_eqv_equivalence : forall a b, Equivalence (semi_eqv a b)
+; semi_comp_respects : forall a b c, Proper (semi_eqv a b ==> semi_eqv b c ==> semi_eqv a c) (@semi_comp _ _ _)
+; semi_associativity :
+ forall `(f:Hom a b)`(g:Hom b c)`(h:Hom c d), semi_eqv _ _ (semi_comp (semi_comp f g) h) (semi_comp f (semi_comp g h))
+}.
+Coercion semi_ob : SemiCategory >-> Sortclass.
+
+Notation "a ~-> b" := (@semi_hom _ _ _ a b) (at level 70).
+Notation "f ~-~ g" := (@semi_eqv _ _ _ _ _ f g) (at level 54).
+Notation "f >>->> g" := (@semi_comp _ _ _ _ _ _ f g) (at level 45).
+
+Add Parametric Relation (Ob:Type)(Hom:Ob->Ob->Type)(C:SemiCategory Ob Hom)(a b:Ob) : (semi_hom a b) (semi_eqv a b)
+ reflexivity proved by (@Equivalence_Reflexive _ _ (semi_eqv_equivalence a b))
+ symmetry proved by (@Equivalence_Symmetric _ _ (semi_eqv_equivalence a b))
+ transitivity proved by (@Equivalence_Transitive _ _ (semi_eqv_equivalence a b))
+ as parametric_relation_semi_eqv.
+ Add Parametric Morphism `(c:SemiCategory Ob Hom)(a b c:Ob) : (@semi_comp _ _ _ a b c)
+ with signature (semi_eqv _ _ ==> semi_eqv _ _ ==> semi_eqv _ _) as parametric_morphism_semi_comp.
+ intros.
+ apply semi_comp_respects; auto.
+ Defined.
+
+Class SemiFunctor
+`( c1 : SemiCategory )
+`( c2 : SemiCategory )
+( fobj : c1 -> c2 ) :=
+{ semifunctor_fobj := fobj
+; semi_fmor : forall {a b}, (a~->b) -> (fobj a)~->(fobj b)
+; semi_fmor_respects : forall a b (f f':a~->b), (f ~-~ f') -> (semi_fmor f ~-~ semi_fmor f')
+; semi_fmor_preserves_comp : forall `(f:a~->b)`(g:b~->c), (semi_fmor f) >>->> (semi_fmor g) ~-~ semi_fmor (f >>->> g)
+}.
+Implicit Arguments semi_fmor [[Ob][Hom][c1][Ob0][Hom0][c2][fobj][a][b]].
+
+ (* register "fmor" so we can rewrite through it *)
+ Implicit Arguments semi_fmor [ Ob Hom Ob0 Hom0 c1 c2 fobj a b ].
+ Implicit Arguments semi_fmor_respects [ Ob Hom Ob0 Hom0 c1 c2 fobj a b ].
+ Implicit Arguments semi_fmor_preserves_comp [ Ob Hom Ob0 Hom0 c1 c2 fobj a b c ].
+ Notation "F \- f" := (semi_fmor F f) (at level 20) : category_scope.
+ Add Parametric Morphism `(C1:SemiCategory)`(C2:SemiCategory)
+ (Fobj:C1->C2)
+ (F:SemiFunctor C1 C2 Fobj)
+ (a b:C1)
+ : (@semi_fmor _ _ C1 _ _ C2 Fobj F a b)
+ with signature ((@semi_eqv C1 _ C1 a b) ==> (@semi_eqv C2 _ C2 (Fobj a) (Fobj b))) as parametric_morphism_semi_fmor'.
+ intros; apply (@semi_fmor_respects _ _ C1 _ _ C2 Fobj F a b x y); auto.
+ Defined.
+ Coercion semifunctor_fobj : SemiFunctor >-> Funclass.
+
+Definition semifunctor_comp
+ `(C1:SemiCategory)
+ `(C2:SemiCategory)
+ `(C3:SemiCategory)
+ `(F:@SemiFunctor _ _ C1 _ _ C2 Fobj)`(G:@SemiFunctor _ _ C2 _ _ C3 Gobj) : SemiFunctor C1 C3 (Gobj ○ Fobj).
+ intros. apply (Build_SemiFunctor _ _ _ _ _ _ _ (fun a b m => semi_fmor G (semi_fmor F m))).
+ intros.
+ setoid_rewrite H.
+ reflexivity.
+ intros.
+ setoid_rewrite semi_fmor_preserves_comp; auto.
+ setoid_rewrite semi_fmor_preserves_comp; auto.
+ reflexivity.
+ Defined.
+Notation "f >>>–>>> g" := (@semifunctor_comp _ _ _ _ _ _ _ _ _ _ f _ g) (at level 20) : category_scope.
+
+Class IsomorphicSemiCategories `(C:SemiCategory)`(D:SemiCategory) :=
+{ isc_f_obj : C -> D
+; isc_g_obj : D -> C
+; isc_f : SemiFunctor C D isc_f_obj
+; isc_g : SemiFunctor D C isc_g_obj
+; isc_forward : forall a b (f:a~->b), semi_fmor isc_f (semi_fmor isc_g f) ~-~ f
+}.
+; isc_backward : isc_g >>>> isc_f ~~~~ functor_id D
+}.
+
+
; reification_r : forall k:K, Functor K C (reification_r_obj k)
; reification_rstar_f : Functor (enr_v K) (enr_v C) reification_rstar_obj
; reification_rstar : MonoidalFunctor (enr_v_mon K) (enr_v_mon C) reification_rstar_f
-; reification_commutes : forall k, reification_r k >>>> RepresentableFunctor C CI <~~~> RepresentableFunctor K k >>>> reification_rstar_f
+; reification_commutes : ∀ k, reification_r k >>>> RepresentableFunctor C CI <~~~> RepresentableFunctor K k >>>> reification_rstar_f
}.
Transparent RepresentableFunctor.
Transparent functor_comp.
| roi_id : forall smme:SMMEs, ReificationOrIdentity smme smme
| roi_reif : forall s1 s2:SMMEs, Reification s1 s2 (mon_i s2) -> ReificationOrIdentity s1 s2.
+Definition reificationOrIdentityFobj s1 s2 (f:ReificationOrIdentity s1 s2) : s1 -> s2 :=
+ match f with
+ | roi_id s => (fun x => x)
+ | roi_reif s1 s2 f => reification_rstar_obj f
+ end.
+
Definition reificationOrIdentityFunc
- : forall s1 s2, ReificationOrIdentity s1 s2 -> { fobj : _ & Functor s1 s2 fobj }.
+ : forall s1 s2 (f:ReificationOrIdentity s1 s2), Functor (enr_v s1) (enr_v s2) (reificationOrIdentityFobj s1 s2 f).
intros.
- destruct X.
- exists (fun x => x).
+ destruct f.
apply functor_id.
- exists (reification_rstar_obj r).
- apply r.
+ unfold reificationOrIdentityFobj.
+ apply (reification_rstar_f r).
Defined.
Definition compose_reifications (s0 s1 s2:SMMEs) :
clear q.
set (reification_commutes X K) as comm1.
set (reification_commutes X0 (mon_i s1)) as comm2.
- admit.
+ set (RepresentableFunctor s0 K) as a in *.
+ set (reification_rstar_f X) as a' in *.
+ set (reification_rstar_f X0) as x in *.
+ set (reification_r X K) as b in *.
+ set (reification_r X0 (mon_i s1)) as c in *.
+ set (RepresentableFunctor s2 (mon_i s2)) as c' in *.
+ set (RepresentableFunctor s1 (mon_i s1)) as b' in *.
+ apply (ni_comp(F2:=b >>>> (b' >>>> x))).
+ apply (@ni_respects _ _ _ _ _ _ _ _ _ _ b _ b _ (c >>>> c') _ (b' >>>> x)).
+ apply ni_id.
+ apply comm2.
+ eapply ni_comp.
+ eapply ni_inv.
+ apply (ni_associativity b b' x).
+ eapply ni_inv.
+ eapply ni_comp.
+ eapply ni_inv.
+ apply (ni_associativity a a' x).
+ apply (@ni_respects _ _ _ _ _ _ _ _ _ _ (a >>>> a') _ (b >>>> b') _ x _ x).
+ apply ni_inv.
+ apply comm1.
+ apply ni_id.
Defined.
Definition reificationOrIdentityComp
Definition MorphismsOfCategoryOfReifications : @SmallFunctors SMMEs.
refine {| small_func := ReificationOrIdentity
; small_func_id := fun s => roi_id s
- ; small_func_func := fun smme1 smme2 f => projT2 (reificationOrIdentityFunc _ _ f)
+ ; small_func_func := fun smme1 smme2 f => reificationOrIdentityFunc _ _ f
; small_func_comp := reificationOrIdentityComp
|}; intros; simpl.
apply if_id.
Require Import ReificationsEquivalentToGeneralizedArrows.
Require Import WeakFunctorCategory.
+
Section ReificationsIsomorphicToGeneralizedArrows.
+ Definition M1 (c1 c2 : SmallSMMEs.SMMEs) :
+ (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) ->
+ (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2).
+ intro GA.
+ destruct GA; [ apply roi_id | idtac ].
+ apply roi_reif.
+ apply reification_from_garrow.
+ apply g.
+ Defined.
+
+ Definition M2 (c1 c2 : SmallSMMEs.SMMEs) :
+ (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2) ->
+ (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2).
+ intro RE.
+ destruct RE; [ apply gaoi_id | idtac ].
+ apply gaoi_ga.
+ apply (garrow_from_reification s1 s2 r).
+ Defined.
+
+ (*
+
+ * 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
+
+ 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.
+
End ReificationsIsomorphicToGeneralizedArrows.
apply q.
Defined.
- Theorem WeakFunctorCategoriesIsomorphic : IsomorphicCategories GA RE F1 F2.
- apply Build_IsomorphicCategories.
+ Theorem WeakFunctorCategoriesIsomorphic : IsomorphicCategories GA RE.
+ refine {| ic_f := F1 ; ic_g := F2 |}.
unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
eapply if_comp.
apply m1_m2_id.