From: Adam Megacz Date: Sun, 27 Mar 2011 19:37:04 +0000 (+0000) Subject: Merge branch 'master' of http://git.megacz.com/coq-hetmet X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=50e3c41de96cf699e3617e702c426b5725173657;hp=d7e72f54b8097cb188e4fc9cb284e585c4d63514 Merge branch 'master' of git.megacz.com/coq-hetmet --- diff --git a/Makefile b/Makefile index 2d65894..d8bc76a 100644 --- a/Makefile +++ b/Makefile @@ -6,7 +6,7 @@ default: build/CoqPass.hs build/CoqPass.hs: $(allfiles) make build/Makefile.coq - cd build; make -f Makefile.coq OPTS=-dont-load-proofs ExtractionMain.vo + cd build; make -f Makefile.coq OPT=-dont-load-proofs ExtractionMain.vo cd build; make -f Makefile.coq Extraction.vo cat src/Extraction-prefix.hs > build/CoqPass.hs cat build/Extraction.hs | grep -v '^module' | grep -v '^import' >> build/CoqPass.hs 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/GeneralizedArrowCategory.v b/src/GeneralizedArrowCategory.v index a9bedbb..3ec6660 100644 --- a/src/GeneralizedArrowCategory.v +++ b/src/GeneralizedArrowCategory.v @@ -26,19 +26,36 @@ Require Import GeneralizedArrow. 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. @@ -66,7 +83,7 @@ Definition generalizedArrowOrIdentityComp 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. diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v index e6d3cbd..627aa22 100644 --- a/src/GeneralizedArrowFromReification.v +++ b/src/GeneralizedArrowFromReification.v @@ -122,9 +122,29 @@ Section GArrowFromReification. Definition garrow_functor := step1_functor >>>> step2_functor. - Definition garrow_from_reification : GeneralizedArrow K C. - refine {| ga_functor := garrow_functor |}. + 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. 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..0227f60 100644 --- a/src/ReificationCategory.v +++ b/src/ReificationCategory.v @@ -26,25 +26,44 @@ Require Import Reification. 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. +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) : 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. @@ -54,7 +73,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 +110,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..5163c26 100644 --- a/src/ReificationsIsomorphicToGeneralizedArrows.v +++ b/src/ReificationsIsomorphicToGeneralizedArrows.v @@ -32,4 +32,162 @@ 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. + + 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). + intro RE. + destruct RE; [ apply gaoi_id | idtac ]. + apply gaoi_ga. + 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. + + 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. + 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. 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. diff --git a/src/categories b/src/categories index cc0b469..1ab46a0 160000 --- a/src/categories +++ b/src/categories @@ -1 +1 @@ -Subproject commit cc0b4696c2cfc23bdff6ded347478510ccf014c9 +Subproject commit 1ab46a0e579ec1964ae0ab3cadb64f6a77db8d30