fact: Definition easy_modality : Modality := Build_Modality In_easy _ inO_equiv_inO_easy O_reflector O_inO_easy to O_ind_easy O_ind_easy_beta inO_paths_easy.
imports: HoTT.Basics HoTT.Types HFiber Extensions Factorization Limits.Pullback ReflectiveSubuniverse