(*********************************************************************************************************************************) (* WeakFunctorCategory: *) (* *) (* A category whose morphisms are functors, identified up to natural isomorphism (not equality). This pulls most of the *) (* heavy lifting out of ReificationsEquivalentToGeneralizedArrows, since the definitions in that context cause Coq to bog *) (* down and run unbearably slowly *) (* *) (*********************************************************************************************************************************) Generalizable All Variables. Require Import Preamble. Require Import General. Require Import Categories_ch1_3. Require Import Functors_ch1_4. Require Import Isomorphisms_ch1_5. Require Import ProductCategories_ch1_6_1. Require Import OppositeCategories_ch1_6_2. Require Import Enrichment_ch2_8. Require Import Subcategories_ch7_1. Require Import NaturalTransformations_ch7_4. Require Import NaturalIsomorphisms_ch7_5. Require Import MonoidalCategories_ch7_8. Require Import Coherence_ch7_8. (*Require Import Enrichment_ch2_8.*) (*Require Import RepresentableStructure_ch7_2.*) Section WeakFunctorCategory. (* We can't handle categories directly due to size issues. * Therefore, we ask the user to supply two types "Cat" and "Mor" * which index the "small categories"; we then construct a large * category relative to those. *) Structure SmallCategories := { small_cat : Type ; small_ob : small_cat -> Type ; small_hom : forall c:small_cat, small_ob c -> small_ob c -> Type ; small_cat_cat : forall c:small_cat, Category (small_ob c) (small_hom c) }. Context {sc:SmallCategories}. Structure SmallFunctors := { small_func : small_cat sc -> small_cat sc -> Type ; small_func_fobj : forall {c1}{c2}, small_func c1 c2 -> (small_ob sc c1 -> small_ob sc c2) ; small_func_func : forall {c1}{c2}(f:small_func c1 c2), Functor (small_cat_cat sc c1) (small_cat_cat sc c2) (small_func_fobj f) (* proof that our chosen indexing contains identity functors and is closed under composition *) ; small_func_id : forall c1 , small_func c1 c1 ; small_func_id_id : forall {c1}, small_func_func (small_func_id c1) ≃ functor_id (small_cat_cat sc c1) ; small_func_comp : forall {c1}{c2}{c3}, small_func c1 c2 -> small_func c2 c3 -> small_func c1 c3 ; small_func_comp_comp : forall {c1}{c2}{c3}(f:small_func c1 c2)(g:small_func c2 c3), small_func_func (small_func_comp f g) ≃ small_func_func f >>>> small_func_func g }. Instance WeakFunctorCategory `(sf:SmallFunctors) : Category (small_cat sc) (small_func sf) := { id := fun a => small_func_id sf a ; comp := fun a b c f g => small_func_comp sf f g ; eqv := fun a b f g => small_func_func sf f ≃ small_func_func sf g }. intros; simpl. apply Build_Equivalence. unfold Reflexive; simpl; intros; apply if_id. unfold Symmetric; simpl; intros; apply if_inv; auto. unfold Transitive; simpl; intros; eapply if_comp. apply H. apply H0. intros; simpl. unfold Proper; unfold respectful; simpl; intros. eapply if_comp. apply small_func_comp_comp. eapply if_inv. eapply if_comp. apply small_func_comp_comp. eapply if_respects. apply if_inv. apply H. apply if_inv. apply H0. intros; simpl. eapply if_comp. apply small_func_comp_comp. eapply if_comp; [ idtac | apply if_left_identity ]. eapply if_respects; try apply if_id. apply small_func_id_id. intros; simpl. eapply if_comp. apply small_func_comp_comp. eapply if_comp; [ idtac | apply if_right_identity ]. eapply if_respects; try apply if_id. apply small_func_id_id. intros; simpl. eapply if_comp. eapply if_comp ; [ idtac | apply small_func_comp_comp ]. apply if_id. apply if_inv. eapply if_comp. eapply if_comp ; [ idtac | apply small_func_comp_comp ]. apply if_id. eapply if_comp. eapply if_respects. eapply if_id. eapply small_func_comp_comp. apply if_inv. eapply if_comp. eapply if_respects. eapply small_func_comp_comp. eapply if_id. set (@if_associativity) as q. apply (q _ _ _ _ _ _ _ _ _ _ _ _ _ (small_func_func sf f) _ (small_func_func sf g) _ (small_func_func sf h)). Defined. End WeakFunctorCategory. 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 F1 F2. apply Build_IsomorphicCategories. 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.