+ (* 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').
+ 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').
+ 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).
+ refine {| fmor := fun a b f => M1 f |}.
+ intros.
+ unfold hom in *.
+ unfold eqv in *.
+ simpl in *.
+ destruct f.
+ set (invert_ga _ f') as q.
+ destruct q; subst.
+ apply if_id.
+ simpl in *.
+ destruct H0; subst.
+ apply H.
+ simpl in *.
+ destruct f'; simpl in *.
+ apply H.
+ apply H.
+ 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_associativity
+ ((ga_functor g0 >>>> HomFunctor s0 (mon_i s0))) (ga_functor g) (HomFunctor s2 (me_i s2))).
+ Defined.
+