equiv_functor_precompose_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@{v u} (Y <~> Z) (X <~> Z) := equiv_functor_equiv e^-1%equiv 1%equiv.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths.