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