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