{X Z : Type} `{IsLocal f Z} (g : X -> Z) : Localize f X -> Z. Proof. refine (Localize_ind f X (fun _ => Z) g _); intros i. apply ooextendable_over_const. apply ooextendable_islocal. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import ReflectiveSubuniverse Accessible. Import IsLocal_Internal.