equiv_functor_sigma' `{P : A -> Type} `{Q : B -> Type} (f : A <~> B) (g : forall a, P a <~> Q (f a)) : sig P <~> sig Q := equiv_functor_sigma f g.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.