f (X : Type) : Type := | loc : X -> X | lsect : forall i (g : S i -> X), T i -> X | lissect : forall i (g : S i -> X) (s : S i), lsect i g (f i s) = g s | lretr : forall i (g : S i -> X), T i -> X | lisretr : forall i (h : T i -> X) (t : T i), lretr i (h o f i) t = h t.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import ReflectiveSubuniverse Accessible. Import IsLocal_Internal.