From: Adam Megacz Date: Sun, 27 Mar 2011 08:06:40 +0000 (-0700) Subject: checkpoint X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=e536cc4194f350ed6de5d465bcf53fda650b3d12;hp=3351499d7cb3d32c8df441426309ec6a1ef2a035 checkpoint --- diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index 05d059a..dbeb3cc 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -40,7 +40,7 @@ Require Import HaskProofCategory. (* Require Import HaskStrongCategory. *) -Require Import ReificationsEquivalentToGeneralizedArrows. +Require Import ReificationsIsomorphicToGeneralizedArrows. Open Scope string_scope. Extraction Language Haskell. diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v index e6d3cbd..f17caa5 100644 --- a/src/GeneralizedArrowFromReification.v +++ b/src/GeneralizedArrowFromReification.v @@ -107,6 +107,14 @@ Section GArrowFromReification. 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; @@ -124,6 +132,11 @@ Section GArrowFromReification. Definition garrow_from_reification : GeneralizedArrow K C. refine {| ga_functor := garrow_functor |}. + (* + unfold garrow_functor. + apply MonoidalFunctorsCompose. + apply MonoidalFunctorsCompose. + *) admit. Defined. diff --git a/src/PreCategory.v b/src/PreCategory.v new file mode 100644 index 0000000..7418261 --- /dev/null +++ b/src/PreCategory.v @@ -0,0 +1,93 @@ +(*********************************************************************************************************************************) +(* 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 +}. + + diff --git a/src/Reification.v b/src/Reification.v index a56ded8..2f2ba67 100644 --- a/src/Reification.v +++ b/src/Reification.v @@ -31,7 +31,7 @@ Structure Reification (K:Enrichment) (C:Enrichment) (CI:C) := ; 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. diff --git a/src/ReificationCategory.v b/src/ReificationCategory.v index b4d444a..f735679 100644 --- a/src/ReificationCategory.v +++ b/src/ReificationCategory.v @@ -30,14 +30,19 @@ 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. +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) : @@ -54,7 +59,28 @@ 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 @@ -70,7 +96,7 @@ 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. diff --git a/src/ReificationsIsomorphicToGeneralizedArrows.v b/src/ReificationsIsomorphicToGeneralizedArrows.v index db11897..dc2f6b0 100644 --- a/src/ReificationsIsomorphicToGeneralizedArrows.v +++ b/src/ReificationsIsomorphicToGeneralizedArrows.v @@ -30,6 +30,57 @@ Require Import GeneralizedArrowCategory. 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. diff --git a/src/WeakFunctorCategory.v b/src/WeakFunctorCategory.v index 49a5189..85ade61 100644 --- a/src/WeakFunctorCategory.v +++ b/src/WeakFunctorCategory.v @@ -192,8 +192,8 @@ Section WeakFunctorCategoryIsomorphism. 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.