apply (step1_niso K C (reification_from_garrow K C garrow)).
Qed.
- Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfReifications CategoryOfGeneralizedArrows.
+ (*
+ Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfReifications CategoryOfGeneralizedArrows.
admit.
- Qed.
+ Qed.*)
End ReificationsEquivalentToGeneralizedArrows.