fact: Definition R_in_comapK {A B} (R : Param04.Rel A B) : forall (b : B) (a : A), comap_in_R R b a o R_in_comap R b a == idmap := Map4.R_in_mapK _ (Param04.contravariant A B R).
imports: Coq(ssreflect) HoTT(HoTT) HoTT_additions Database elpi(elpi)