fact: Definition reflects_in (O : Subuniverse) (T : Type) `{In O T} : @Reflects O T (prereflects_in O T).
imports: HoTT.Basics HoTT.Types Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback PathAny Colimits.Pushout