`{Funext} (A : Type) `{IsHProp A} : In O A. Proof. apply inO_const_fromgen; intros i f. exists (f (inhab i)). intros; apply path_ishprop. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions NullHomotopy. Require Import Modality. Module Import IsLocal_Internal. Module Import IsNull_Internal.