fact: Record Modality@{i} := Build_Modality' { modality_subuniv : Subuniverse@{i} ; modality_prereflects : forall (T : Type@{i}), PreReflects modality_subuniv T ; modality_reflectsD : forall (T : Type@{i}), ReflectsD modality_subuniv modality_subuniv T ; }.
imports: HoTT.Basics HoTT.Types HFiber Extensions Factorization Limits.Pullback ReflectiveSubuniverse