+ 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 (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.
+ 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.
+
+ 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 (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.
+ simpl in q.
+ simpl in q.
+ apply q.
+ Qed.
+