{X Y : Type} (f : X -> Y) := ExtensionAlong (@tr (-1) X) (fun _ => Y) f.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Factorization. Require Import Truncations.Core Modalities.Modality.