{A B} (f : A -> B) (C : B -> Type) : (forall b, ooExtendableAlong (const_tt (hfiber f b)) (fun _ => C b)) -> ooExtendableAlong f C := fun null n => extendable_isnull_fibers n f C null. Class IsAccModality@{a i} (O : Subuniverse@{i}) := { acc_ngen : NullGenerators@{a} ; inO_iff_isnull : forall (X : Type@{i}), iff@{i i i} (In O X) (IsNull acc_ngen X) ; }. Arguments acc_ngen O {_}. Arguments inO_iff_isnull O {_} X. Section AccessibleModalities. Context (O : Modality) {acco : IsAccModality O}. Global Instance isconnected_acc_ngen i : IsConnected O (acc_ngen O i). Proof. apply isconnected_from_elim_to_O. pose (H := fst (fst (inO_iff_isnull O (O (acc_ngen O i))) _ i 1%nat) (to O ((acc_ngen O) i))). exists (H.1 tt). exact (fun x => (H.2 x)^). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions NullHomotopy. Require Import Modality. Module Import IsLocal_Internal. Module Import IsNull_Internal.