+ apply (step1_niso K C CM (reification_from_garrow K CM garrow)).
+ Qed.
+
+ Lemma roundtrip_reification_to_reification
+ `(K:SurjectiveEnrichment) `(C:MonicEnrichment ce) (CM:MonoidalEnrichment ce) (reification : Reification K ce (enr_c_i ce))
+ : reification ≃ reification_from_garrow K CM (garrow_from_reification K C CM reification).
+
+ simpl.
+ unfold garrow_functor.
+
+ eapply if_comp.
+ apply (step1_niso K C CM reification).
+
+ unfold garrow_monoidal.
+ unfold mf_F.
+ apply if_inv.
+ eapply if_comp.
+ apply (if_associativity (RestrictToImage reification) (R' K CM reification >>>> step2_functor C)
+ (HomFunctor ce (pmon_I (enr_c_pm ce)))).
+ apply if_inv.
+ eapply if_comp.
+ apply (if_associativity (RestrictToImage reification) (R' K CM reification)
+ (FullImage_InclusionFunctor (HomFunctor ce (pmon_I (enr_c_pm ce))))).
+
+ apply (if_respects (RestrictToImage reification) (RestrictToImage reification) _ _ (if_id _)).
+ apply if_inv.
+ eapply if_comp.
+ apply (if_associativity (R' K CM reification) (step2_functor C) (HomFunctor ce _)).
+
+ set ((R' K CM reification)) as f.
+ unfold HomFunctor_fullimage in f.
+ set (roundtrip_lemma (me_full(MonicEnrichment:=C))) as q.
+ set (q (me_faithful(MonicEnrichment:=C)) _ _ _ _ f) as q'.
+ apply q'.
+ Qed.