(*********************************************************************************************************************************)
-(* ReificationsEquivalentToGeneralizedArrows: *)
+(* ReificationsIsomorphicToGeneralizedArrows: *)
(* *)
-(* The category of generalized arrows and the category of reifications are equivalent categories. *)
+(* The category of generalized arrows and the category of reifications are isomorphic categories. *)
(* *)
(*********************************************************************************************************************************)
Require Import ReificationFromGeneralizedArrow.
Require Import ReificationCategory.
Require Import GeneralizedArrowCategory.
-Require Import ReificationsEquivalentToGeneralizedArrows.
+Require Import ReificationCategory.
+Require Import ReificationsAndGeneralizedArrows.
Require Import WeakFunctorCategory.
+Require Import BijectionLemma.
Section ReificationsIsomorphicToGeneralizedArrows.
apply g.
Defined.
+ (* I tried really hard to avoid this *)
+ Require Import Coq.Logic.Eqdep.
+
+ Inductive Heq : forall {A}{B}, A -> B -> Prop :=
+ heq : forall {A} (a:A), Heq a a.
+
+ Lemma invert_ga' : forall (a b: SMME)
+ (f:a~~{MorphismsOfCategoryOfGeneralizedArrows}~~>b), a=b ->
+ (Heq f (gaoi_id a)) \/ (exists f', Heq f (gaoi_ga a b f')).
+ intros.
+ destruct f.
+ left; apply heq.
+ subst; right.
+ exists g.
+ apply heq.
+ Defined.
+
Lemma invert_ga : forall (a: SMME)
(f:a~~{MorphismsOfCategoryOfGeneralizedArrows}~~>a),
(f = gaoi_id _) \/ (exists f', f = gaoi_ga _ _ f').
- admit.
+ intros.
+ set (invert_ga' a a f (refl_equal a)) as q.
+ destruct q.
+ left.
+ inversion H.
+ apply inj_pairT2 in H2.
+ apply inj_pairT2 in H1.
+ subst; auto.
+ right.
+ destruct H.
+ exists x.
+ inversion H.
+ apply inj_pairT2 in H2.
+ apply inj_pairT2 in H1.
+ subst; auto.
Qed.
+ Lemma invert_reif' : forall (a b: SMME)
+ (f:a~~{MorphismsOfCategoryOfReifications}~~>b), a=b ->
+ (Heq f (roi_id a)) \/ (exists f', Heq f (roi_reif a b f')).
+ intros.
+ destruct f.
+ left; apply heq.
+ subst; right.
+ exists r.
+ apply heq.
+ Defined.
+
Lemma invert_reif : forall (a: SMME)
(f:a~~{MorphismsOfCategoryOfReifications}~~>a),
(f = roi_id _) \/ (exists f', f = roi_reif _ _ f').
- admit.
+ intros.
+ set (invert_reif' a a f (refl_equal a)) as q.
+ destruct q.
+ left.
+ inversion H.
+ apply inj_pairT2 in H2.
+ apply inj_pairT2 in H1.
+ subst; auto.
+ right.
+ destruct H.
+ exists x.
+ inversion H.
+ apply inj_pairT2 in H2.
+ apply inj_pairT2 in H1.
+ subst; auto.
Qed.
Definition M1_Functor : Functor MorphismsOfCategoryOfGeneralizedArrows MorphismsOfCategoryOfReifications (fun x => x).
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))).
+ ((ga_functor g0 >>>> HomFunctor s0 (mon_i s0))) (ga_functor g) (HomFunctor s2 (me_i s2))).
Defined.
Definition M2 (c1 c2 : SmallSMMEs.SMMEs) :
apply (garrow_from_reification s1 s2 r).
Defined.
+ Lemma eqv1 a b (f : a ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> 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.
+ 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 q.
+ apply if_id.
+ 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.
+ 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.
+
Lemma M2_respects :
forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b),
f ~~ f' ->
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'.
+ apply (if_comp (if_inv (@step1_niso _ s1 _ _ s2 r0)) (if_comp H (@step1_niso _ s1 _ _ s2 r))).
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.
+ intros; apply (@bijection_lemma _ _ _ _ _ M1_Functor M2); intros.
+ apply M2_respects; auto.
+ unfold fmor; simpl.
+ apply (@eqv1 _ _ f0 f0).
+ apply if_id.
+ unfold fmor; simpl.
+ apply (@eqv2 _ _ f0 f0).
+ apply if_id.
+ 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.
-
+ apply (eqv1 _ _ f f'); auto.
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.
+ apply (eqv2 _ _ f f'); auto.
+ Qed.
End ReificationsIsomorphicToGeneralizedArrows.
projects / coq-hetmet.git / blobdiff