f X := (forall (i : lgen_indices f), ooExtendableAlong (f i) (fun _ => X)). End IsLocal_Internal. Class IsAccRSU@{a i} (O : Subuniverse@{i}) := { acc_lgen : LocalGenerators@{a} ; inO_iff_islocal : forall (X : Type@{i}), iff@{i i i} (In O X) ( acc_lgen X) ; }. Arguments acc_lgen O {_}. Arguments inO_iff_islocal O {_} X. Global Instance O_inverts_generators {O : ReflectiveSubuniverse} `{IsAccRSU O} (i : lgen_indices (acc_lgen O)) : O_inverts O (acc_lgen O i). Proof. pose (ext_dom := fst (inO_iff_islocal O (O (lgen_domain (acc_lgen O) i))) _). pose (ext_cod := fst (inO_iff_islocal O (O (lgen_codomain (acc_lgen O) i))) _). simple refine (isequiv_adjointify _ _ _ _). - apply O_rec. exact ((fst (ext_dom i 1%nat) (to O _)).1). - apply O_indpaths; intros x; simpl. rewrite O_rec_beta. refine ((fst (snd (ext_cod i 2) (fun x => O_functor O (acc_lgen O i) ((fst (ext_dom i 1%nat) (to O _)).1 x)) _) _).1 x); intros a. rewrite ((fst (ext_dom i 1%nat) (to O _)).2 a). apply to_O_natural. - apply O_indpaths; intros x; simpl. rewrite (to_O_natural O (acc_lgen O i) x). rewrite O_rec_beta. apply ((fst (ext_dom i 1%nat) (to O _)).2 x). Qed.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions NullHomotopy. Require Import Modality. Module Import IsLocal_Internal. Module Import IsNull_Internal.