Definition pullBackFamily {X X':Type} (g : X -> X') (Y : X' -> Type) := λ x, Y (g x).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.