Definition pullBackPointOverWithSection' {X X':Type} (g : X -> X') {x:X} {x':X'} (r : g x = x') {Y : X' -> Type} {y : Y x'} {f : ∏ x', Y x'} (k : y = f x') : pullBackPointOver g r y = pullBackSection g f x. Proof. induction (!k), r. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.