From: Adam Megacz Date: Mon, 28 Mar 2011 00:22:10 +0000 (-0700) Subject: remove old code from WeakFunctorCategory X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=de9b7cba83ba98f30da7999cfe5ff0e4c1058e42 remove old code from WeakFunctorCategory --- diff --git a/src/WeakFunctorCategory.v b/src/WeakFunctorCategory.v index 85ade61..5e52faa 100644 --- a/src/WeakFunctorCategory.v +++ b/src/WeakFunctorCategory.v @@ -106,139 +106,3 @@ Coercion WeakFunctorCategory : SmallFunctors >-> Category. Coercion small_func_func : small_func >-> Functor. Coercion small_cat_cat : small_cat >-> Category. Coercion small_cat : SmallCategories >-> Sortclass. - -(* -Add Parametric Relation (Ob:Type)(Hom:Ob->Ob->Type)(C:Category Ob Hom)(a b:Ob) : (hom a b) (eqv a b) - reflexivity proved by (@Equivalence_Reflexive _ _ (eqv_equivalence a b)) - symmetry proved by (@Equivalence_Symmetric _ _ (eqv_equivalence a b)) - transitivity proved by (@Equivalence_Transitive _ _ (eqv_equivalence a b)) - as parametric_relation_eqv. - Add Parametric Morphism `(c:Category Ob Hom)(a b c:Ob) : (comp a b c) - with signature (eqv _ _ ==> eqv _ _ ==> eqv _ _) as parametric_morphism_comp. - auto. - Defined.*) - -Section WeakFunctorCategoryIsomorphism. - (* Here we sort of set up exactly the conditions needed to trigger - * the ReificationsAreGeneralizedArrows proof; again, I'm doing it here - * because the instant I import Reification or GeneralizedArrow, Coq - * becomes nearly unusable. *) - - (* same objects (SMME's) for both categories, and the functor is IIO *) - Context {SMMEs:SmallCategories}. - Context {GA:@SmallFunctors SMMEs}. - Context {RE:@SmallFunctors SMMEs}. - - Context (M1:forall c1 c2, (c1~~{GA}~~>c2) -> (c1~~{RE}~~>c2)). - Context (M2:forall c1 c2, (c1~~{RE}~~>c2) -> (c1~~{GA}~~>c2)). - Implicit Arguments M1 [[c1][c2]]. - Implicit Arguments M2 [[c1][c2]]. - - Section GeneralCase. - Context (m1_respects_eqv - : forall (c1 c2:SMMEs) (f:c1~~{GA}~~>c2) (g:c1~~{GA}~~>c2), - (small_func_func _ f) ≃ (small_func_func _ g) -> small_func_func RE (M1 f) ≃ small_func_func RE (M1 g)). - Context (m2_respects_eqv - : forall (c1 c2:SMMEs) (f:c1~~{RE}~~>c2) (g:c1~~{RE}~~>c2), - (small_func_func _ f) ≃ (small_func_func _ g) -> small_func_func GA (M2 f) ≃ small_func_func GA (M2 g)). - Context (m1_preserves_id - : forall c1, small_func_func _ (M1 (small_func_id GA c1)) ≃ small_func_id RE c1). - Context (m2_preserves_id - : forall c1, small_func_func _ (M2 (small_func_id RE c1)) ≃ small_func_id GA c1). - Context (m1_respects_comp : - forall (c1 c2 c3:SMMEs) (f:c1~~{GA}~~>c2) (g:c2~~{GA}~~>c3), - small_func_func _ (small_func_comp _ (M1 f) (M1 g)) ≃ - small_func_func _ ((M1 (small_func_comp _ f g)))). - Context (m2_respects_comp : - forall (c1 c2 c3:SMMEs) (f:c1~~{RE}~~>c2) (g:c2~~{RE}~~>c3), - small_func_func _ (small_func_comp _ (M2 f) (M2 g)) ≃ - small_func_func _ ((M2 (small_func_comp _ f g)))). - Context (m1_m2_id - : forall (c1 c2:SMMEs) (f:c1~~{GA}~~>c2), - small_func_func _ (M2 (M1 f)) ≃ small_func_func _ f). - Context (m2_m1_id - : forall (c1 c2:SMMEs) (f:c1~~{RE}~~>c2), - small_func_func _ (M1 (M2 f)) ≃ small_func_func _ f). - - Definition F1 : Functor GA RE (fun x => x). - refine {| fmor := fun a b f => M1 f |}. - intros. - unfold eqv; simpl. - apply m1_respects_eqv. - apply H. - intros. - unfold eqv; simpl; intros. - apply m1_preserves_id. - intros. - unfold eqv; simpl. - set m1_respects_comp as q. - unfold eqv in q. - apply q. - Defined. - - Definition F2 : Functor RE GA (fun x => x). - refine {| fmor := fun a b f => M2 f |}. - intros. - unfold eqv; simpl. - apply m2_respects_eqv. - apply H. - intros. - unfold eqv; simpl; intros. - apply m2_preserves_id. - intros. - unfold eqv; simpl. - set m2_respects_comp as q. - unfold eqv in q. - apply q. - Defined. - - 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. - apply H. - unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *. - eapply if_comp. - apply m2_m1_id. - apply H. - Qed. - - End GeneralCase. -(* - (* now, the special case we can really use: M1 and M2 each consist of post-composition *) - Section WeakFunctorCategoryPostCompositionIsomorphism. - - Context (M1_postcompose_obj : forall c1:SMMEs, c1 -> c1). - Context (M1_postcompose : forall c1:SMMEs, Functor c1 c1 (M1_postcompose_obj c1)). - - Context (M2_postcompose_obj : forall c1:SMMEs, c1 -> c1). - Context (M2_postcompose : forall c1:SMMEs, Functor c1 c1 (M1_postcompose_obj c1)). - - Context (M1_M2_id : forall c1:SMMEs, M1_postcompose c1 >>>> M2_postcompose c1 ≃ functor_id _). - Context (M2_M1_id : forall c1:SMMEs, M2_postcompose c1 >>>> M1_postcompose c1 ≃ functor_id _). - - Context (M1_postcompose_act : forall (c1 c2:SMMEs)(f:c1~~{GA}~~>c2), - small_func_func _ (M1 f) ≃ small_func_func _ f >>>> M1_postcompose c2). - Context (M2_postcompose_act : forall (c1 c2:SMMEs)(f:c1~~{RE}~~>c2), - small_func_func _ (M2 f) ≃ small_func_func _ f >>>> M2_postcompose c2). - - Definition F1' : Functor GA RE (fun x => x). - apply F1; intros; simpl. - eapply if_comp. - apply M1_postcompose_act. - apply if_inv. - eapply if_comp. - apply M1_postcompose_act. - apply if_respects; try apply if_id. - apply if_inv; auto. - apply (if_comp (M1_postcompose_act _ _ _)). - apply M1_postcompose_act. - - - Theorem WeakFunctorCategoryPostCompositionIsomorphism : IsomorphicCategories GA RE F1 F2 - End WeakFunctorCategoryPostCompositionIsomorphism. - *) -End WeakFunctorCategoryIsomorphism. - -