(*********************************************************************************************************************************)
(* ReificationsAndGeneralizedArrows: *)
(* *)
-(* The category of generalized arrows and the category of reifications are equivalent categories. *)
+(* For each pair of enrichments E1 and E2, there is a bijection between the generalized arrows E1->E2 and the reifications *)
+(* E1->E2 *)
(* *)
(*********************************************************************************************************************************)
Definition roundtrip_lemma
`(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (reification : Reification K C (me_i C))
- := roundtrip_lemma' (RepresentableFunctor C (me_i C)) (ffme_mf_full C) (ffme_mf_faithful C) (step1_functor K C reification).
+ := roundtrip_lemma' (HomFunctor C (me_i C)) (ffme_mf_full C) (ffme_mf_faithful C) (step1_functor K C reification).
Lemma roundtrip_reification_to_reification
`(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (reification : Reification K C (me_i C))
simpl.
unfold mon_f.
unfold garrow_functor.
- apply (if_comp(F2:=(step1_functor K C reification >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C)))))).
+ apply (if_comp(F2:=(step1_functor K C reification >>>> InclusionFunctor _ (FullImage (HomFunctor C (me_i C)))))).
apply (@step1_niso _ K _ _ C reification).
apply (if_inv (roundtrip_lemma K C reification)).
Qed.
Lemma roundtrip_garrow_to_garrow
`(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (garrow : GeneralizedArrow K C)
: garrow ≃ garrow_from_reification K C (reification_from_garrow K C garrow).
- apply (ffc_functor_weakly_monic _ (ffme_mf_conservative C)).
+ apply (ffc_functor_weakly_monic _ (ffme_mf_full C) (ffme_mf_faithful C) (ffme_mf_conservative C) (ffme_mf_conservative C)).
apply if_inv.
apply (if_comp(F2:=(step1_functor K C (reification_from_garrow K C garrow)
- >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C)))))).
+ >>>> InclusionFunctor _ (FullImage (HomFunctor C (me_i C)))))).
unfold mf_f.
unfold garrow_from_reification.
unfold garrow_functor.