f (X : Type) : Type := | loc : X -> X | islocal_localize : forall i, IsEquiv (fun (g : T i -> X) => g o f i).
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import ReflectiveSubuniverse Accessible. Import IsLocal_Internal.