fact: Definition comap_in_R {A B} (R : Param02a.Rel A B) : forall (b : B) (a : A), comap R b = a -> R a b := Map2a.map_in_R _ (Param02a.contravariant A B R).
imports: Coq(ssreflect) HoTT(HoTT) HoTT_additions Database elpi(elpi)