+ unfold hom in *.
+ 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.
+ eapply if_comp.
+ apply (step1_niso smme (smme_mee smme) (smme_mon smme) x).
+ apply if_inv.
+ 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.
+ eapply if_comp.
+ apply (if_associativity (R' smme smme x) (ff_functor_section_functor me_homfunctor me_full me_faithful)
+ (HomFunctor (senr_c smme) (senr_c_i smme))).
+ set (roundtrip_lemma (me_full(MonicEnrichment:=smme_mee smme))) as q.
+ set (R' smme smme x) as f.
+ set (me_faithful(MonicEnrichment:=smme_mee smme)) as ff.
+ unfold HomFunctor_fullimage in f.
+ unfold mf_F in f.
+ set (q ff _ _ (FullImage x) _ f) as q'.
+ unfold me_homfunctor in q'.
+ exact q'.
+
+ simpl in *.
+ destruct f'; simpl in *.
+ simpl in *.
+ apply if_inv in H.
+ eapply if_comp; [ idtac | eapply if_inv; apply H ].
+ clear H.
+ unfold garrow_functor.
+ unfold step2_functor.
+ apply if_inv.
+ 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.
+ apply if_inv.
+
+ eapply if_comp.
+ apply (if_associativity (R' smme smme x) (ff_functor_section_functor me_homfunctor me_full me_faithful)
+ (HomFunctor (senr_c smme) (senr_c_i smme))).
+ set (roundtrip_lemma (me_full(MonicEnrichment:=smme_mee smme))) as q.
+ set (R' smme smme x) as f.
+ set (me_faithful(MonicEnrichment:=smme_mee smme)) as ff.
+ unfold HomFunctor_fullimage in f.
+ unfold mf_F in f.
+ set (q ff _ _ (FullImage x) _ f) as q'.
+ unfold me_homfunctor in q'.
+ exact q'.
+
+ simpl in *.
+ unfold garrow_functor.
+ unfold step2_functor.
+ 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 roundtrip_lemma.
+
+ apply if_inv.
+ set (step1_niso s1 (smme_mee s2) s2 r0) as q'.
+ apply if_inv in q'.
+ eapply if_comp.
+ eapply if_comp; [ idtac | apply q' ].
+ eapply if_comp.
+ apply (if_associativity
+ (RestrictToImage r0)
+ (R' s1 s2 r0 >>>> 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 r0)
+ (R' s1 s2 r0)
+ (FullImage_InclusionFunctor _)).
+ apply (if_respects
+ (RestrictToImage r0)
+ (RestrictToImage r0)
+ (R' s1 s2 r0 >>>> FullImage_InclusionFunctor _)
+ (((R' s1 s2 r0 >>>> 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 r0)
+ (ff_functor_section_functor me_homfunctor me_full me_faithful)
+ (HomFunctor (senr_c s2) (senr_c_i s2))).
+ apply roundtrip_lemma.
+ apply if_inv.
+ apply H.
+ 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; 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 *.
+ apply (eqv1 _ _ f f'); auto.
+ unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
+ apply (eqv2 _ _ f f'); auto.