Require Import Enrichment_ch2_8.
Require Import RepresentableStructure_ch7_2.
Require Import GeneralizedArrow.
+Require Import WeakFunctorCategory.
+Require Import SmallSMMEs.
-Definition CategoryOfGeneralizedArrows : Category SMME (fun x y => @GeneralizedArrow x _ y).
- admit.
- Qed.
+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 compose_generalizedArrows (s0 s1 s2:SMMEs) :
+ GeneralizedArrow s0 s1 -> GeneralizedArrow s1 s2 -> GeneralizedArrow s0 s2.
+ intro g01.
+ intro g12.
+ refine
+ {| ga_functor := g01 >>>> RepresentableFunctor s1 (mon_i s1) >>>> g12 |}.
+ apply MonoidalFunctorsCompose.
+ apply MonoidalFunctorsCompose.
+ apply (ga_functor_monoidal g01).
+ apply (me_mf s1).
+ apply (ga_functor_monoidal g12).
+ Defined.
+
+Definition generalizedArrowOrIdentityComp
+ : forall s1 s2 s3, GeneralizedArrowOrIdentity s1 s2 -> GeneralizedArrowOrIdentity s2 s3 -> GeneralizedArrowOrIdentity s1 s3.
+ intros.
+ destruct X.
+ apply X0.
+ destruct X0.
+ apply (gaoi_ga _ _ g).
+ apply (gaoi_ga _ _ (compose_generalizedArrows _ _ _ g g0)).
+ Defined.
+
+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_comp := generalizedArrowOrIdentityComp
+ |}; intros; simpl.
+ apply if_id.
+ destruct f as [|fobj f]; simpl in *.
+ apply if_inv.
+ apply if_left_identity.
+ destruct g as [|gobj g]; simpl in *.
+ apply if_inv.
+ apply if_right_identity.
+ unfold mf_F.
+ idtac.
+ unfold mf_f.
+ apply if_associativity.
+ Defined.
+
+Definition CategoryOfGeneralizedArrows :=
+ WeakFunctorCategory MorphismsOfCategoryOfGeneralizedArrows.
Require Import Enrichment_ch2_8.
Require Import RepresentableStructure_ch7_2.
Require Import Reification.
+Require Import WeakFunctorCategory.
+Require Import SmallSMMEs.
-Definition CategoryOfReifications : Category SMME (fun x y:SMME => Reification (smme_e x) (smme_e y) (mon_i (smme_mon y))).
+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 reificationOrIdentityFunc
+ : forall s1 s2, ReificationOrIdentity s1 s2 -> { fobj : _ & Functor s1 s2 fobj }.
+ intros.
+ destruct X.
+ exists (fun x => x).
+ apply functor_id.
+ exists (reification_rstar_obj r).
+ apply 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_r := fun K => (reification_r X K) >>>> (reification_r X0 (mon_i s1))
+ |}.
+ intro K.
+ set (ni_associativity (reification_r X K) (reification_r X0 (mon_i s1)) (RepresentableFunctor s2 (mon_i s2))) as q.
+ eapply ni_comp.
+ apply q.
+ clear q.
+ set (reification_commutes X K) as comm1.
+ set (reification_commutes X0 (mon_i s1)) as comm2.
admit.
- Qed.
\ No newline at end of file
+ Defined.
+
+Definition reificationOrIdentityComp
+ : forall s1 s2 s3, ReificationOrIdentity s1 s2 -> ReificationOrIdentity s2 s3 -> ReificationOrIdentity s1 s3.
+ intros.
+ destruct X.
+ apply X0.
+ destruct X0.
+ apply (roi_reif _ _ r).
+ apply (roi_reif _ _ (compose_reifications _ _ _ r r0)).
+ Defined.
+
+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_comp := reificationOrIdentityComp
+ |}; intros; simpl.
+ apply if_id.
+ destruct f as [|fobj f]; simpl in *.
+ apply if_inv.
+ apply if_left_identity.
+ destruct g as [|gobj g]; simpl in *.
+ apply if_inv.
+ apply if_right_identity.
+ apply if_id.
+ Defined.
+
+Definition CategoryOfReifications :=
+ WeakFunctorCategory MorphismsOfCategoryOfReifications.
--- /dev/null
+(*********************************************************************************************************************************)
+(* 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.
+
+