proposition: Fact comap_uparam_arrow `{Funext} A A' (PA : A <=> A') B B' (PB : B <=> B') : comap (uparam_arrow PA PB) = fun f a => comap PB (f (map PA a)).
proof: Proof. reflexivity. Qed.
imports: elpi(elpi) Coq(ssreflect) HoTT(HoTT) HoTT_additions Hierarchy