{X Y : Type} (f : X -> Y) : X -> Pullback f f := fun x => (x;x;idpath).
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Homotopy.IdentitySystems Cubical.PathSquare. Require Import Diagrams.CommutativeSquares.