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).
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).