Modal subuniverse induction

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-11-24.
Last modified on 2023-11-24.

module orthogonal-factorization-systems.modal-subuniverse-induction where
Imports 
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

Idea

Given a modal operator ○ and a modal unit, we can form the subuniverse of modal types as those types whose unit is an equivalence. A modal subuniverse induction principle for the modality is then a section of maps of maps:

  multivariable-section (precomp-Π unit-○ P)

where

  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, the modality must be idempotent.

Definition

Subuniverse induction

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

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. We call this principle strong subuniverse induction. Note that such a retraction may not in general be unique, and the computational behaviour of this induction principle depends on the choice of retraction.

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

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

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

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

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

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

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

Recent changes