equiv_functor_postcompose_equiv@{i j k u v | i <= u, j <= v, k <= u, k <= v} {X : Type@{i}} {Y : Type@{j}} (Z : Type@{k}) (e : X <~> Y) : Equiv@{u v} (Z <~> X) (Z <~> Y) := equiv_functor_equiv 1%equiv e. Global Instance isequiv_equiv_inverse {A B} : IsEquiv (@equiv_inverse A B). Proof. refine (isequiv_adjointify _ equiv_inverse _ _); intros e; apply path_equiv; reflexivity. Defined.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths.