# Reflective subuniverses ```agda module orthogonal-factorization-systems.reflective-subuniverses where ``` <details><summary>Imports</summary> ```agda open import foundation.action-on-identifications-functions open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.function-extensionality open import foundation.function-types open import foundation.identity-types open import foundation.propositions open import foundation.retractions open import foundation.subuniverses open import foundation.universe-levels open import orthogonal-factorization-systems.local-types open import orthogonal-factorization-systems.localizations-subuniverses open import orthogonal-factorization-systems.modal-induction open import orthogonal-factorization-systems.modal-operators open import orthogonal-factorization-systems.modal-subuniverse-induction ``` </details> ## Idea A **reflective subuniverse** is a [subuniverse](foundation.subuniverses.md) `P` together with a reflecting operator `○ : UU → UU` that take values in `P`, and a [modal unit](orthogonal-factorization-systems.modal-operators.md) `A → ○ A` for all [small types](foundation-core.small-types.md) `A`, with the property that the types in `P` are [local](orthogonal-factorization-systems.local-types.md) at the modal unit for every `A`. Hence the modal types with respect to `○` are precisely the types in the reflective subuniverse. ## Definitions ### The predicate on subuniverses of being reflective ```agda is-reflective-subuniverse : {l1 l2 : Level} (P : subuniverse l1 l2) → UU (lsuc l1 ⊔ l2) is-reflective-subuniverse {l1} P = Σ ( operator-modality l1 l1) ( λ ○ → Σ ( unit-modality ○) ( λ unit-○ → ( (X : UU l1) → is-in-subuniverse P (○ X)) × ( (X Y : UU l1) → is-in-subuniverse P X → is-local (unit-○ {Y}) X))) ``` ```agda module _ {l1 l2 : Level} (P : subuniverse l1 l2) (is-reflective-P : is-reflective-subuniverse P) where operator-is-reflective-subuniverse : operator-modality l1 l1 operator-is-reflective-subuniverse = pr1 is-reflective-P unit-is-reflective-subuniverse : unit-modality (operator-is-reflective-subuniverse) unit-is-reflective-subuniverse = pr1 (pr2 is-reflective-P) is-in-subuniverse-operator-type-is-reflective-subuniverse : (X : UU l1) → is-in-subuniverse P (operator-is-reflective-subuniverse X) is-in-subuniverse-operator-type-is-reflective-subuniverse = pr1 (pr2 (pr2 is-reflective-P)) is-local-is-in-subuniverse-is-reflective-subuniverse : (X Y : UU l1) → is-in-subuniverse P X → is-local (unit-is-reflective-subuniverse {Y}) X is-local-is-in-subuniverse-is-reflective-subuniverse = pr2 (pr2 (pr2 is-reflective-P)) ``` ### The type of reflective subuniverses ```agda reflective-subuniverse : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) reflective-subuniverse l1 l2 = Σ (subuniverse l1 l2) (is-reflective-subuniverse) ``` ```agda module _ {l1 l2 : Level} (P : reflective-subuniverse l1 l2) where subuniverse-reflective-subuniverse : subuniverse l1 l2 subuniverse-reflective-subuniverse = pr1 P is-in-reflective-subuniverse : UU l1 → UU l2 is-in-reflective-subuniverse = is-in-subuniverse subuniverse-reflective-subuniverse inclusion-reflective-subuniverse : type-subuniverse (subuniverse-reflective-subuniverse) → UU l1 inclusion-reflective-subuniverse = inclusion-subuniverse subuniverse-reflective-subuniverse is-reflective-subuniverse-reflective-subuniverse : is-reflective-subuniverse (subuniverse-reflective-subuniverse) is-reflective-subuniverse-reflective-subuniverse = pr2 P operator-reflective-subuniverse : operator-modality l1 l1 operator-reflective-subuniverse = operator-is-reflective-subuniverse ( subuniverse-reflective-subuniverse) ( is-reflective-subuniverse-reflective-subuniverse) unit-reflective-subuniverse : unit-modality (operator-reflective-subuniverse) unit-reflective-subuniverse = unit-is-reflective-subuniverse ( subuniverse-reflective-subuniverse) ( is-reflective-subuniverse-reflective-subuniverse) is-in-subuniverse-operator-type-reflective-subuniverse : ( X : UU l1) → is-in-subuniverse ( subuniverse-reflective-subuniverse) ( operator-reflective-subuniverse X) is-in-subuniverse-operator-type-reflective-subuniverse = is-in-subuniverse-operator-type-is-reflective-subuniverse ( subuniverse-reflective-subuniverse) ( is-reflective-subuniverse-reflective-subuniverse) is-local-is-in-subuniverse-reflective-subuniverse : ( X Y : UU l1) → is-in-subuniverse subuniverse-reflective-subuniverse X → is-local (unit-reflective-subuniverse {Y}) X is-local-is-in-subuniverse-reflective-subuniverse = is-local-is-in-subuniverse-is-reflective-subuniverse ( subuniverse-reflective-subuniverse) ( is-reflective-subuniverse-reflective-subuniverse) ``` ## Properties ### Reflective subuniverses are subuniverses that have all localizations ```agda module _ {l1 l2 : Level} (P : subuniverse l1 l2) (is-reflective-P : is-reflective-subuniverse P) where has-all-localizations-is-reflective-subuniverse : (A : UU l1) → subuniverse-localization P A pr1 (has-all-localizations-is-reflective-subuniverse A) = operator-is-reflective-subuniverse P is-reflective-P A pr1 (pr2 (has-all-localizations-is-reflective-subuniverse A)) = is-in-subuniverse-operator-type-is-reflective-subuniverse P is-reflective-P A pr1 (pr2 (pr2 (has-all-localizations-is-reflective-subuniverse A))) = unit-is-reflective-subuniverse P is-reflective-P pr2 (pr2 (pr2 (has-all-localizations-is-reflective-subuniverse A))) X is-in-subuniverse-X = is-local-is-in-subuniverse-is-reflective-subuniverse P is-reflective-P X A is-in-subuniverse-X module _ {l1 l2 : Level} (P : subuniverse l1 l2) (L : (A : UU l1) → subuniverse-localization P A) where is-reflective-has-all-localizations-subuniverse : is-reflective-subuniverse P pr1 is-reflective-has-all-localizations-subuniverse A = type-subuniverse-localization P (L A) pr1 (pr2 is-reflective-has-all-localizations-subuniverse) {A} = unit-subuniverse-localization P (L A) pr1 (pr2 (pr2 is-reflective-has-all-localizations-subuniverse)) A = is-in-subuniverse-subuniverse-localization P (L A) pr2 (pr2 (pr2 is-reflective-has-all-localizations-subuniverse)) A B is-in-subuniverse-A = is-local-at-unit-is-in-subuniverse-subuniverse-localization P (L B) A is-in-subuniverse-A ``` ## Recursion for reflective subuniverses ```agda module _ {l1 l2 : Level} (P : subuniverse l1 l2) (is-reflective-P : is-reflective-subuniverse P) where rec-modality-is-reflective-subuniverse : rec-modality (unit-is-reflective-subuniverse P is-reflective-P) rec-modality-is-reflective-subuniverse {X} {Y} = map-inv-is-equiv ( is-local-is-in-subuniverse-is-reflective-subuniverse ( P) ( is-reflective-P) ( operator-is-reflective-subuniverse P is-reflective-P Y) ( X) ( is-in-subuniverse-operator-type-is-reflective-subuniverse ( P) ( is-reflective-P) ( Y))) map-is-reflective-subuniverse : {X Y : UU l1} → (X → Y) → operator-is-reflective-subuniverse P is-reflective-P X → operator-is-reflective-subuniverse P is-reflective-P Y map-is-reflective-subuniverse = ap-map-rec-modality ( unit-is-reflective-subuniverse P is-reflective-P) ( rec-modality-is-reflective-subuniverse) strong-rec-subuniverse-is-reflective-subuniverse : strong-rec-subuniverse-modality ( unit-is-reflective-subuniverse P is-reflective-P) strong-rec-subuniverse-is-reflective-subuniverse = strong-rec-subuniverse-rec-modality ( unit-is-reflective-subuniverse P is-reflective-P) ( rec-modality-is-reflective-subuniverse) rec-subuniverse-is-reflective-subuniverse : rec-subuniverse-modality (unit-is-reflective-subuniverse P is-reflective-P) rec-subuniverse-is-reflective-subuniverse = rec-subuniverse-rec-modality ( unit-is-reflective-subuniverse P is-reflective-P) ( rec-modality-is-reflective-subuniverse) ``` ## See also - [Σ-closed reflective subuniverses](orthogonal-factorization-systems.sigma-closed-reflective-subuniverses.md) - [Localizations with respect to subuniverses](orthogonal-factorization-systems.localizations-subuniverses.md) ## References {{#bibliography}} {{#reference UF13}} {{#reference RSS20}} {{#reference Rij19}}