fact: Definition equiv_functor_sigma `{P : A -> Type} `{Q : B -> Type} (f : A -> B) `{IsEquiv A B f} (g : forall a, P a -> Q (f a)) `{forall a, @IsEquiv (P a) (Q (f a)) (g a)} : sig P <~> sig Q := Build_Equiv _ _ (functor_sigma f g) _.
imports: HoTT.Basics Types.Arrow Types.Paths