(O : Modality) `{IsAccRSU O} : IsAccModality O. Proof. unshelve econstructor. { refine (Build_NullGenerators ( { i : lgen_indices@{a} (acc_lgen O) & O (lgen_domain@{a} (acc_lgen O) i) } + { i : lgen_indices@{a} (acc_lgen O) & O (lgen_codomain@{a} (acc_lgen O) i) }) _). intros [ [i x] | [i x] ]; exact (hfiber (to O _) x). } { assert (cm := @conn_map_to_O O). split. - intros X_inO [ [i x] | [i x] ]; exact (ooextendable_const_isconnected_inO O _ _). - intros Xnull. apply (snd (inO_iff_islocal O X)); intros i. refine (cancelL_ooextendable (fun _ => X) (acc_lgen O i) (to O (lgen_codomain (acc_lgen O) i)) _ _). + apply ooextendable_isnull_fibers; intros x. exact (Xnull (inr (i;x))). + refine (ooextendable_homotopic _ (O_functor O (acc_lgen O i) o to O (lgen_domain (acc_lgen O) i)) _ _). 1:apply to_O_natural. apply ooextendable_compose. * apply ooextendable_equiv, O_inverts_generators. * apply ooextendable_isnull_fibers; intros x. exact (Xnull (inl (i;x))). } Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions NullHomotopy. Require Import Modality. Module Import IsLocal_Internal. Module Import IsNull_Internal.