Require Import Subcategories_ch7_1.
Require Import NaturalTransformations_ch7_4.
Require Import NaturalIsomorphisms_ch7_5.
+Require Import PreMonoidalCategories.
Require Import MonoidalCategories_ch7_8.
Require Import Coherence_ch7_8.
-Require Import Enrichment_ch2_8.
Require Import RepresentableStructure_ch7_2.
Require Import Reification.
Require Import GeneralizedArrow.
Require Import ReificationsAndGeneralizedArrows.
Require Import WeakFunctorCategory.
Require Import BijectionLemma.
+Require Import Enrichments.
Section ReificationsIsomorphicToGeneralizedArrows.
- Definition M1 {c1 c2 : SmallSMMEs.SMMEs} :
+ Definition M1 {c1 c2 : SMMEs} :
(c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) ->
(c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2).
intro GA.
destruct GA; [ apply roi_id | idtac ].
apply roi_reif.
- apply reification_from_garrow.
- apply g.
+ apply (reification_from_garrow s1 s2 g).
Defined.
(* I tried really hard to avoid this *)
apply if_id.
destruct g; simpl.
apply if_id.
- unfold mf_f; simpl.
+ simpl.
apply (if_associativity
- ((ga_functor g0 >>>> HomFunctor s0 (mon_i s0))) (ga_functor g) (HomFunctor s2 (me_i s2))).
+ ((ga_functor g0 >>>> HomFunctor s0 (enr_c_i s0))) (ga_functor g) (HomFunctor s2 (enr_c_i s2))).
Defined.
- Definition M2 (c1 c2 : SmallSMMEs.SMMEs) :
+ Definition M2 (c1 c2 : 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).
+ apply (garrow_from_reification s1 (smme_mee s2) s2 r).
Defined.
Lemma eqv1 a b (f : a ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> b)
(H : generalizedArrowOrIdentityFunc a b f ≃ generalizedArrowOrIdentityFunc a b f') :
generalizedArrowOrIdentityFunc a b (M2 a b (M1 f)) ≃ generalizedArrowOrIdentityFunc a b f'.
unfold hom in *.
- set (@roundtrip_garrow_to_garrow _ a _ _ b) as q.
+ set (@roundtrip_garrow_to_garrow a b (smme_mee b) (smme_mon 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:=HomFunctor s2 (mon_i s2))(G1:=HomFunctor s2 (mon_i s2))).
+ apply (if_respects
+ (ga_functor g)
+ (garrow_functor s1 (smme_mee s2) s2 (reification_from_garrow s1 s2 g))
+ (HomFunctor (senr_c s2) (senr_c_i s2))
+ (HomFunctor (senr_c s2) (senr_c_i s2))
+ ).
apply q.
apply if_id.
- Qed.
-
+ Qed.
Lemma eqv2 a b (f : a ~~{ MorphismsOfCategoryOfReifications }~~> b)
(f' : a ~~{ MorphismsOfCategoryOfReifications }~~> b)
(H : reificationOrIdentityFunc a b f ≃ reificationOrIdentityFunc a b f') :
reificationOrIdentityFunc _ _ (M1 (M2 _ _ f)) ≃ reificationOrIdentityFunc _ _ f'.
unfold hom in *.
- set (@roundtrip_reification_to_reification _ a _ _ b) as q.
+ set (@roundtrip_reification_to_reification a b (smme_mee b) (smme_mon 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.
+ Qed.
Lemma M2_respects :
forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b),
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).
+ 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.
+ eapply if_comp.
+ apply (step1_niso smme (smme_mee smme) (smme_mon smme) x).
+ apply if_inv.
+ set (roundtrip_lemma smme (smme_mee smme) (smme_mon smme) x) as q.
+ apply if_inv.
+ eapply if_comp.
+ apply (if_associativity (RestrictToImage x) (R' smme smme x) (FullImage_InclusionFunctor _)).
+ apply if_inv.
+ eapply if_comp.
+ apply (if_associativity (RestrictToImage x) ((R' smme smme x >>>>
+ ff_functor_section_functor me_homfunctor me_full me_faithful))
+ (HomFunctor (senr_c smme) (senr_c_i smme))).
+ apply (if_respects (RestrictToImage x) (RestrictToImage x)).
+ apply (if_id (RestrictToImage x)).
+ unfold mf_F.
+ unfold me_homfunctor in q.
+ unfold pmon_I.
+ apply q.
+
simpl in *.
destruct f'; simpl in *.
- apply if_inv.
+ simpl in *.
apply if_inv in H.
- apply (if_comp H).
+ eapply if_comp; [ idtac | eapply if_inv; apply 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).
+ eapply if_comp.
+ apply (step1_niso smme (smme_mee smme) (smme_mon smme) r).
+
+ rename r into x.
+ apply if_inv.
+ eapply if_comp.
+ apply (if_associativity (RestrictToImage x) ((R' smme smme x >>>>
+ ff_functor_section_functor me_homfunctor me_full me_faithful))
+ (HomFunctor (senr_c smme) (senr_c_i smme))).
+ apply if_inv.
+ eapply if_comp.
+ apply (if_associativity (RestrictToImage x) (R' smme smme x) (FullImage_InclusionFunctor _)).
+ apply (if_respects (RestrictToImage x) (RestrictToImage x)).
+ apply (if_id (RestrictToImage x)).
+
+ unfold mf_F.
+ set (roundtrip_lemma smme (smme_mee smme) (smme_mon smme) x) as q.
+ apply if_inv.
+ unfold me_homfunctor in q.
+ unfold pmon_I.
+ apply q.
+
simpl in *.
unfold garrow_functor.
unfold step2_functor.
- apply if_inv in H.
- apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r)).
+ set (step1_niso s1 (smme_mee s2) s2 r) as q.
+ apply if_inv in q.
+ eapply if_comp.
+ eapply if_comp; [ idtac | apply q ].
+
+ eapply if_comp.
+ apply (if_associativity
+ (RestrictToImage r)
+ (R' s1 s2 r >>>> ff_functor_section_functor me_homfunctor me_full me_faithful)
+ (HomFunctor (senr_c s2) (senr_c_i s2))).
+ apply if_inv.
+ eapply if_comp.
+ apply (if_associativity
+ (RestrictToImage r)
+ (R' s1 s2 r)
+ (FullImage_InclusionFunctor _)).
+ apply (if_respects
+ (RestrictToImage r)
+ (RestrictToImage r)
+ (R' s1 s2 r >>>> FullImage_InclusionFunctor _)
+ (((R' s1 s2 r >>>> ff_functor_section_functor me_homfunctor me_full me_faithful) >>>>
+ HomFunctor (senr_c s2) (senr_c_i s2)))).
+ apply (if_id _).
+ apply if_inv.
+ eapply if_comp.
+ apply (if_associativity
+ (R' s1 s2 r)
+ (ff_functor_section_functor me_homfunctor me_full me_faithful)
+ (HomFunctor (senr_c s2) (senr_c_i s2))).
+ apply if_inv.
+ apply (if_respects
+ (R' s1 s2 r)
+ (R' s1 s2 r)
+ (FullImage_InclusionFunctor _)
+ ((ff_functor_section_functor me_homfunctor me_full me_faithful >>>> HomFunctor _ _))
+ ).
+ apply (if_id _).
apply if_inv.
- apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r0)).
- apply (if_comp (if_inv (@step1_niso _ s1 _ _ s2 r0)) (if_comp H (@step1_niso _ s1 _ _ s2 r))).
+ apply (RestrictToImage_splits_niso (HomFunctor s2 (senr_c_i s2))).
Qed.
Definition M2_Functor : Functor MorphismsOfCategoryOfReifications MorphismsOfCategoryOfGeneralizedArrows (fun x => x).
projects / coq-hetmet.git / blobdiff