# Modal subuniverse induction ```agda module orthogonal-factorization-systems.modal-subuniverse-induction where ``` <details><summary>Imports</summary> ```agda open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.function-types open import foundation.functoriality-dependent-function-types open import foundation.homotopies open import foundation.identity-types open import foundation.multivariable-sections open import foundation.precomposition-dependent-functions open import foundation.precomposition-functions open import foundation.retractions open import foundation.type-theoretic-principle-of-choice open import foundation.universe-levels open import orthogonal-factorization-systems.modal-induction open import orthogonal-factorization-systems.modal-operators ``` </details> ## Idea Given a [modal operator](orthogonal-factorization-systems.modal-operators.md) `○` and a modal unit, we can form the [subuniverse](foundation.subuniverses.md) of modal types as those types whose unit is an [equivalence](foundation-core.equivalences.md). A **modal subuniverse induction principle** for the modality is then a [section of maps of maps](foundation.multivariable-sections.md): ```text multivariable-section (precomp-Π unit-○ P) ``` where ```text precomp-Π unit-○ P : ((x' : ○ X) → P x') → (x : X) → P (unit-○ x) ``` for all families of modal types `P` over some `○ X`. Note that for such principles to coincide with [modal induction](orthogonal-factorization-systems.modal-induction.md), the modality must be idempotent. ## Definition ### Subuniverse induction ```agda module _ {l1 l2 : Level} {○ : operator-modality l1 l2} (unit-○ : unit-modality ○) where induction-principle-subuniverse-modality : UU (lsuc l1 ⊔ l2) induction-principle-subuniverse-modality = {X : UU l1} (P : ○ X → UU l1) (is-modal-P : is-modal-family unit-○ P) → multivariable-section 1 (precomp-Π unit-○ P) ind-subuniverse-modality : UU (lsuc l1 ⊔ l2) ind-subuniverse-modality = {X : UU l1} (P : ○ X → UU l1) → is-modal-family unit-○ P → ((x : X) → P (unit-○ x)) → (x' : ○ X) → P x' compute-ind-subuniverse-modality : ind-subuniverse-modality → UU (lsuc l1 ⊔ l2) compute-ind-subuniverse-modality ind-○ = {X : UU l1} (P : ○ X → UU l1) (is-modal-P : is-modal-family unit-○ P) → (f : (x : X) → P (unit-○ x)) → ind-○ P is-modal-P f ∘ unit-○ ~ f ind-induction-principle-subuniverse-modality : induction-principle-subuniverse-modality → ind-subuniverse-modality ind-induction-principle-subuniverse-modality I P is-modal-P = map-multivariable-section 1 (precomp-Π unit-○ P) (I P is-modal-P) compute-ind-induction-principle-subuniverse-modality : (I : induction-principle-subuniverse-modality) → compute-ind-subuniverse-modality ( ind-induction-principle-subuniverse-modality I) compute-ind-induction-principle-subuniverse-modality I P is-modal-P = is-multivariable-section-map-multivariable-section 1 ( precomp-Π unit-○ P) ( I P is-modal-P) ``` ### Subuniverse recursion ```agda module _ {l1 l2 : Level} {○ : operator-modality l1 l2} (unit-○ : unit-modality ○) where recursion-principle-subuniverse-modality : UU (lsuc l1 ⊔ l2) recursion-principle-subuniverse-modality = {X Y : UU l1} → is-modal unit-○ Y → multivariable-section 1 (precomp {A = X} unit-○ Y) rec-subuniverse-modality : UU (lsuc l1 ⊔ l2) rec-subuniverse-modality = {X Y : UU l1} → is-modal unit-○ Y → (X → Y) → ○ X → Y compute-rec-subuniverse-modality : rec-subuniverse-modality → UU (lsuc l1 ⊔ l2) compute-rec-subuniverse-modality rec-○ = {X Y : UU l1} (is-modal-Y : is-modal unit-○ Y) → (f : X → Y) → rec-○ is-modal-Y f ∘ unit-○ ~ f rec-recursion-principle-subuniverse-modality : recursion-principle-subuniverse-modality → rec-subuniverse-modality rec-recursion-principle-subuniverse-modality I {Y = Y} is-modal-Y = map-multivariable-section 1 (precomp unit-○ Y) (I is-modal-Y) compute-rec-recursion-principle-subuniverse-modality : (I : recursion-principle-subuniverse-modality) → compute-rec-subuniverse-modality ( rec-recursion-principle-subuniverse-modality I) compute-rec-recursion-principle-subuniverse-modality I {Y = Y} is-modal-Y = is-multivariable-section-map-multivariable-section 1 ( precomp unit-○ Y) ( I is-modal-Y) ``` ### Strong subuniverse induction We can weaken the assumption that the codomain is modal and only ask that the unit has a [retraction](foundation-core.retractions.md). We call this principle **strong subuniverse induction**. Note that such a retraction may not in general be [unique](foundation-core.contractible-types.md), and the computational behaviour of this induction principle depends on the choice of retraction. ```agda module _ {l1 l2 : Level} {○ : operator-modality l1 l2} (unit-○ : unit-modality ○) where strong-induction-principle-subuniverse-modality : UU (lsuc l1 ⊔ l2) strong-induction-principle-subuniverse-modality = {X : UU l1} (P : ○ X → UU l1) → ((x' : ○ X) → retraction (unit-○ {P x'})) → multivariable-section 1 (precomp-Π unit-○ P) strong-ind-subuniverse-modality : UU (lsuc l1 ⊔ l2) strong-ind-subuniverse-modality = {X : UU l1} (P : ○ X → UU l1) → ((x' : ○ X) → retraction (unit-○ {P x'})) → ((x : X) → P (unit-○ x)) → (x' : ○ X) → P x' compute-strong-ind-subuniverse-modality : strong-ind-subuniverse-modality → UU (lsuc l1 ⊔ l2) compute-strong-ind-subuniverse-modality ind-○ = {X : UU l1} (P : ○ X → UU l1) → (is-premodal-P : (x' : ○ X) → retraction (unit-○ {P x'})) → (f : (x : X) → P (unit-○ x)) → ind-○ P is-premodal-P f ∘ unit-○ ~ f strong-ind-strong-induction-principle-subuniverse-modality : strong-induction-principle-subuniverse-modality → strong-ind-subuniverse-modality strong-ind-strong-induction-principle-subuniverse-modality I P is-premodal-P = map-multivariable-section 1 (precomp-Π unit-○ P) (I P is-premodal-P) compute-strong-ind-strong-induction-principle-subuniverse-modality : (I : strong-induction-principle-subuniverse-modality) → compute-strong-ind-subuniverse-modality ( strong-ind-strong-induction-principle-subuniverse-modality I) compute-strong-ind-strong-induction-principle-subuniverse-modality I P is-premodal-P = is-multivariable-section-map-multivariable-section 1 ( precomp-Π unit-○ P) ( I P is-premodal-P) ``` ### Strong subuniverse recursion ```agda module _ {l1 l2 : Level} {○ : operator-modality l1 l2} (unit-○ : unit-modality ○) where strong-recursion-principle-subuniverse-modality : UU (lsuc l1 ⊔ l2) strong-recursion-principle-subuniverse-modality = {X Y : UU l1} → retraction (unit-○ {Y}) → multivariable-section 1 (precomp {A = X} unit-○ Y) strong-rec-subuniverse-modality : UU (lsuc l1 ⊔ l2) strong-rec-subuniverse-modality = {X Y : UU l1} → retraction (unit-○ {Y}) → (X → Y) → ○ X → Y compute-strong-rec-subuniverse-modality : strong-rec-subuniverse-modality → UU (lsuc l1 ⊔ l2) compute-strong-rec-subuniverse-modality rec-○ = {X Y : UU l1} (is-premodal-Y : retraction (unit-○ {Y})) → (f : X → Y) → rec-○ is-premodal-Y f ∘ unit-○ ~ f strong-rec-strong-recursion-principle-subuniverse-modality : strong-recursion-principle-subuniverse-modality → strong-rec-subuniverse-modality strong-rec-strong-recursion-principle-subuniverse-modality I {Y = Y} is-premodal-Y = map-multivariable-section 1 (precomp unit-○ Y) (I is-premodal-Y) compute-strong-rec-strong-recursion-principle-subuniverse-modality : (I : strong-recursion-principle-subuniverse-modality) → compute-strong-rec-subuniverse-modality ( strong-rec-strong-recursion-principle-subuniverse-modality I) compute-strong-rec-strong-recursion-principle-subuniverse-modality I {Y = Y} is-premodal-Y = is-multivariable-section-map-multivariable-section 1 ( precomp unit-○ Y) ( I is-premodal-Y) ``` ## Properties ### Subuniverse recursion from subuniverse induction ```agda module _ {l1 l2 : Level} {○ : operator-modality l1 l2} (unit-○ : unit-modality ○) where rec-subuniverse-ind-subuniverse-modality : ind-subuniverse-modality unit-○ → rec-subuniverse-modality unit-○ rec-subuniverse-ind-subuniverse-modality ind-○ {Y = Y} is-modal-Y = ind-○ (λ _ → Y) (λ _ → is-modal-Y) compute-rec-subuniverse-compute-ind-subuniverse-modality : (ind-○ : ind-subuniverse-modality unit-○) → compute-ind-subuniverse-modality unit-○ ind-○ → compute-rec-subuniverse-modality unit-○ ( rec-subuniverse-ind-subuniverse-modality ind-○) compute-rec-subuniverse-compute-ind-subuniverse-modality ind-○ compute-ind-○ {Y = Y} is-modal-Y = compute-ind-○ (λ _ → Y) (λ _ → is-modal-Y) recursion-principle-induction-principle-subuniverse-modality : induction-principle-subuniverse-modality unit-○ → recursion-principle-subuniverse-modality unit-○ recursion-principle-induction-principle-subuniverse-modality I {Y = Y} is-modal-Y = I (λ _ → Y) (λ _ → is-modal-Y) ``` ### Subuniverse induction from strong subuniverse induction ```agda module _ {l1 l2 : Level} {○ : operator-modality l1 l2} (unit-○ : unit-modality ○) where ind-subuniverse-strong-ind-subuniverse-modality : strong-ind-subuniverse-modality unit-○ → ind-subuniverse-modality unit-○ ind-subuniverse-strong-ind-subuniverse-modality ind-○ P is-modal-P = ind-○ P (retraction-is-equiv ∘ is-modal-P) compute-ind-subuniverse-strong-ind-subuniverse-modality : (ind-○ : strong-ind-subuniverse-modality unit-○) → compute-strong-ind-subuniverse-modality unit-○ ind-○ → compute-ind-subuniverse-modality unit-○ ( ind-subuniverse-strong-ind-subuniverse-modality ind-○) compute-ind-subuniverse-strong-ind-subuniverse-modality ind-○ compute-ind-○ P is-modal-P = compute-ind-○ P (retraction-is-equiv ∘ is-modal-P) induction-principle-strong-induction-principle-subuniverse-modality : strong-induction-principle-subuniverse-modality unit-○ → induction-principle-subuniverse-modality unit-○ induction-principle-strong-induction-principle-subuniverse-modality I P is-modal-P = I P (retraction-is-equiv ∘ is-modal-P) ``` ### Subuniverse recursion from strong subuniverse recursion ```agda module _ {l1 l2 : Level} {○ : operator-modality l1 l2} (unit-○ : unit-modality ○) where rec-subuniverse-strong-rec-subuniverse-modality : strong-rec-subuniverse-modality unit-○ → rec-subuniverse-modality unit-○ rec-subuniverse-strong-rec-subuniverse-modality rec-○ is-modal-Y = rec-○ (retraction-is-equiv is-modal-Y) compute-rec-subuniverse-strong-rec-subuniverse-modality : (rec-○ : strong-rec-subuniverse-modality unit-○) (compute-rec-○ : compute-strong-rec-subuniverse-modality unit-○ rec-○) → compute-rec-subuniverse-modality unit-○ ( rec-subuniverse-strong-rec-subuniverse-modality rec-○) compute-rec-subuniverse-strong-rec-subuniverse-modality rec-○ compute-rec-○ is-modal-Y = compute-rec-○ (retraction-is-equiv is-modal-Y) recursion-principle-strong-recursion-principle-subuniverse-modality : strong-recursion-principle-subuniverse-modality unit-○ → recursion-principle-subuniverse-modality unit-○ recursion-principle-strong-recursion-principle-subuniverse-modality I is-modal-Y = I (retraction-is-equiv is-modal-Y) ``` ### Subuniverse induction from modal induction ```agda module _ {l1 l2 : Level} {○ : operator-modality l1 l2} (unit-○ : unit-modality ○) where strong-ind-subuniverse-ind-modality : ind-modality unit-○ → strong-ind-subuniverse-modality unit-○ strong-ind-subuniverse-ind-modality ind-○ P is-premodal-P f x' = map-retraction unit-○ (is-premodal-P x') (ind-○ P (unit-○ ∘ f) x') compute-strong-ind-subuniverse-ind-modality : (ind-○ : ind-modality unit-○) → compute-ind-modality unit-○ ind-○ → compute-strong-ind-subuniverse-modality unit-○ ( strong-ind-subuniverse-ind-modality ind-○) compute-strong-ind-subuniverse-ind-modality ind-○ compute-ind-○ P is-premodal-P f x = ( ap ( map-retraction unit-○ (is-premodal-P (unit-○ x))) ( compute-ind-○ P (unit-○ ∘ f) x)) ∙ ( is-retraction-map-retraction unit-○ (is-premodal-P (unit-○ x)) (f x)) strong-induction-principle-subuniverse-induction-principle-modality : induction-principle-modality unit-○ → strong-induction-principle-subuniverse-modality unit-○ pr1 ( strong-induction-principle-subuniverse-induction-principle-modality I P is-modal-P) = strong-ind-subuniverse-ind-modality ( ind-induction-principle-modality unit-○ I) P is-modal-P pr2 ( strong-induction-principle-subuniverse-induction-principle-modality I P is-modal-P) = compute-strong-ind-subuniverse-ind-modality ( ind-induction-principle-modality unit-○ I) ( compute-ind-induction-principle-modality unit-○ I) ( P) ( is-modal-P) ind-subuniverse-ind-modality : ind-modality unit-○ → ind-subuniverse-modality unit-○ ind-subuniverse-ind-modality ind-○ = ind-subuniverse-strong-ind-subuniverse-modality unit-○ ( strong-ind-subuniverse-ind-modality ind-○) compute-ind-subuniverse-ind-modality : (ind-○ : ind-modality unit-○) → compute-ind-modality unit-○ ind-○ → compute-ind-subuniverse-modality unit-○ ( ind-subuniverse-ind-modality ind-○) compute-ind-subuniverse-ind-modality ind-○ compute-ind-○ = compute-ind-subuniverse-strong-ind-subuniverse-modality unit-○ ( strong-ind-subuniverse-ind-modality ind-○) ( compute-strong-ind-subuniverse-ind-modality ind-○ compute-ind-○) induction-principle-subuniverse-induction-principle-modality : induction-principle-modality unit-○ → induction-principle-subuniverse-modality unit-○ pr1 ( induction-principle-subuniverse-induction-principle-modality I P is-modal-P) = ind-subuniverse-ind-modality ( ind-induction-principle-modality unit-○ I) ( P) ( is-modal-P) pr2 ( induction-principle-subuniverse-induction-principle-modality I P is-modal-P) = compute-ind-subuniverse-ind-modality ( ind-induction-principle-modality unit-○ I) ( compute-ind-induction-principle-modality unit-○ I) ( P) ( is-modal-P) ``` ### Subuniverse recursion from modal recursion ```agda module _ {l1 l2 : Level} {○ : operator-modality l1 l2} (unit-○ : unit-modality ○) where strong-rec-subuniverse-rec-modality : rec-modality unit-○ → strong-rec-subuniverse-modality unit-○ strong-rec-subuniverse-rec-modality rec-○ is-premodal-Y f x' = map-retraction unit-○ (is-premodal-Y) (rec-○ (unit-○ ∘ f) x') compute-strong-rec-subuniverse-rec-modality : (rec-○ : rec-modality unit-○) → compute-rec-modality unit-○ rec-○ → compute-strong-rec-subuniverse-modality unit-○ ( strong-rec-subuniverse-rec-modality rec-○) compute-strong-rec-subuniverse-rec-modality rec-○ compute-rec-○ is-premodal-Y f x = ( ap ( map-retraction unit-○ (is-premodal-Y)) ( compute-rec-○ (unit-○ ∘ f) x)) ∙ ( is-retraction-map-retraction unit-○ (is-premodal-Y) (f x)) strong-recursion-principle-subuniverse-recursion-principle-modality : recursion-principle-modality unit-○ → strong-recursion-principle-subuniverse-modality unit-○ pr1 ( strong-recursion-principle-subuniverse-recursion-principle-modality I is-premodal-Y) = strong-rec-subuniverse-rec-modality ( rec-recursion-principle-modality unit-○ I) ( is-premodal-Y) pr2 ( strong-recursion-principle-subuniverse-recursion-principle-modality I is-premodal-Y) = compute-strong-rec-subuniverse-rec-modality ( rec-recursion-principle-modality unit-○ I) ( compute-rec-recursion-principle-modality unit-○ I) ( is-premodal-Y) rec-subuniverse-rec-modality : rec-modality unit-○ → rec-subuniverse-modality unit-○ rec-subuniverse-rec-modality rec-○ = rec-subuniverse-strong-rec-subuniverse-modality unit-○ ( strong-rec-subuniverse-rec-modality rec-○) compute-rec-subuniverse-rec-modality : (rec-○ : rec-modality unit-○) → compute-rec-modality unit-○ rec-○ → compute-rec-subuniverse-modality unit-○ (rec-subuniverse-rec-modality rec-○) compute-rec-subuniverse-rec-modality rec-○ compute-rec-○ = compute-rec-subuniverse-strong-rec-subuniverse-modality unit-○ ( strong-rec-subuniverse-rec-modality rec-○) ( compute-strong-rec-subuniverse-rec-modality rec-○ compute-rec-○) recursion-principle-subuniverse-recursion-principle-modality : recursion-principle-modality unit-○ → recursion-principle-subuniverse-modality unit-○ pr1 ( recursion-principle-subuniverse-recursion-principle-modality I is-modal-Y) = rec-subuniverse-rec-modality ( rec-recursion-principle-modality unit-○ I) is-modal-Y pr2 ( recursion-principle-subuniverse-recursion-principle-modality I is-modal-Y) = compute-rec-subuniverse-rec-modality ( rec-recursion-principle-modality unit-○ I) ( compute-rec-recursion-principle-modality unit-○ I) ( is-modal-Y) ``` ## See also - [Modal induction](orthogonal-factorization-systems.modal-induction.md) - [Reflective subuniverses](orthogonal-factorization-systems.reflective-subuniverses.md)