# Modal induction

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-11-24.

module orthogonal-factorization-systems.modal-induction where

Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.functoriality-dependent-function-types
open import foundation.functoriality-dependent-pair-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.sections
open import foundation.type-theoretic-principle-of-choice
open import foundation.unit-type
open import foundation.universe-levels

open import orthogonal-factorization-systems.modal-operators


## Idea

Given a modal operator ○ and a modal unit, a modal induction principle for the modality is a section of maps of maps:

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


where

  precomp-Π unit-○ (○ ∘ P) : ((x' : ○ X) → ○ (P x')) → (x : X) → ○ (P (unit-○ x))


for all families P over some ○ X.

Note that for such principles to coincide with modal subuniverse induction, the modality must be idempotent.

## Definition

module _
{l1 l2 : Level}
{○ : operator-modality l1 l2}
(unit-○ : unit-modality ○)
where

ind-modality : UU (lsuc l1 ⊔ l2)
ind-modality =
{X : UU l1} (P : ○ X → UU l1) →
((x : X) → ○ (P (unit-○ x))) →
(x' : ○ X) → ○ (P x')

compute-ind-modality : ind-modality → UU (lsuc l1 ⊔ l2)
compute-ind-modality ind-○ =
{X : UU l1} (P : ○ X → UU l1) →
(f : (x : X) → ○ (P (unit-○ x))) →
(x : X) → ind-○ P f (unit-○ x) ＝ f x

induction-principle-modality : UU (lsuc l1 ⊔ l2)
induction-principle-modality =
{X : UU l1} (P : ○ X → UU l1) →
multivariable-section 1 (precomp-Π unit-○ (○ ∘ P))

ind-induction-principle-modality : induction-principle-modality → ind-modality
ind-induction-principle-modality I P =
map-multivariable-section 1 (precomp-Π unit-○ (○ ∘ P)) (I P)

compute-ind-induction-principle-modality :
(I : induction-principle-modality) →
compute-ind-modality (ind-induction-principle-modality I)
compute-ind-induction-principle-modality I P =
is-multivariable-section-map-multivariable-section 1
( precomp-Π unit-○ (○ ∘ P))
( I P)

module _
{l1 l2 : Level}
{○ : operator-modality l1 l2}
(unit-○ : unit-modality ○)
where

rec-modality : UU (lsuc l1 ⊔ l2)
rec-modality = {X Y : UU l1} → (X → ○ Y) → ○ X → ○ Y

compute-rec-modality : rec-modality → UU (lsuc l1 ⊔ l2)
compute-rec-modality rec-○ =
{X Y : UU l1} →
(f : X → ○ Y) →
(x : X) → rec-○ f (unit-○ x) ＝ f x

recursion-principle-modality : UU (lsuc l1 ⊔ l2)
recursion-principle-modality =
{X Y : UU l1} → multivariable-section 1 (precomp {A = X} unit-○ (○ Y))

rec-recursion-principle-modality : recursion-principle-modality → rec-modality
rec-recursion-principle-modality I {Y = Y} =
map-multivariable-section 1 (precomp unit-○ (○ Y)) I

compute-rec-recursion-principle-modality :
(I : recursion-principle-modality) →
compute-rec-modality (rec-recursion-principle-modality I)
compute-rec-recursion-principle-modality I {Y = Y} =
is-multivariable-section-map-multivariable-section 1
( precomp unit-○ (○ Y)) I


## Properties

module _
{l1 l2 : Level}
{○ : operator-modality l1 l2}
(unit-○ : unit-modality ○)
where

rec-ind-modality : ind-modality unit-○ → rec-modality unit-○
rec-ind-modality ind {Y = Y} = ind (λ _ → Y)

compute-rec-compute-ind-modality :
(ind-○ : ind-modality unit-○) →
compute-ind-modality unit-○ ind-○ →
compute-rec-modality unit-○ (rec-ind-modality ind-○)
compute-rec-compute-ind-modality ind-○ compute-ind-○ {Y = Y} =
compute-ind-○ (λ _ → Y)

recursion-principle-induction-principle-modality :
induction-principle-modality unit-○ → recursion-principle-modality unit-○
recursion-principle-induction-principle-modality I {Y = Y} = I (λ _ → Y)

is-section-ind-modality :
{l1 l2 : Level}
{○ : operator-modality l1 l2}
(unit-○ : unit-modality ○)
(ind-○ : ind-modality unit-○)
(compute-ind-○ : compute-ind-modality unit-○ ind-○)
{X : UU l1} {P : ○ X → UU l1} → (precomp-Π unit-○ (○ ∘ P) ∘ ind-○ P) ~ id
is-section-ind-modality unit-○ ind-○ compute-ind-○ {X} {P} =
eq-htpy ∘ compute-ind-○ P

is-retraction-ind-id-modality :
{l : Level}
{○ : operator-modality l l}
(unit-○ : unit-modality ○)
(ind-○ : ind-modality unit-○)
(compute-ind-○ : compute-ind-modality unit-○ ind-○)
{X : UU l} → (ind-○ (λ _ → X) id ∘ unit-○) ~ id
is-retraction-ind-id-modality {○ = ○} unit-○ ind-○ compute-ind-○ {X} =
compute-ind-○ (λ _ → X) id

module _
{l1 l2 : Level}
{○ : operator-modality l1 l2}
(unit-○ : unit-modality ○)
(rec-○ : rec-modality unit-○)
(compute-rec-○ : compute-rec-modality unit-○ rec-○)
where

is-retraction-rec-map-modality :
{X Y : UU l1} (f : ○ X → Y) (r : retraction f) →
(rec-○ (map-retraction f r) ∘ (unit-○ ∘ f)) ~ id
is-retraction-rec-map-modality {X} {Y} f r =
( compute-rec-○ (map-retraction f r) ∘ f) ∙h
( is-retraction-map-retraction f r)

retraction-rec-map-modality :
{X Y : UU l1} (f : ○ X → Y) →
retraction f → retraction (unit-○ ∘ f)
pr1 (retraction-rec-map-modality {X} {Y} f r) = rec-○ (map-retraction f r)
pr2 (retraction-rec-map-modality f r) = is-retraction-rec-map-modality f r

section-rec-map-modality :
{X Y : UU l1} (f : X → ○ Y) →
section f → section (rec-○ f)
pr1 (section-rec-map-modality f s) = unit-○ ∘ map-section f s
pr2 (section-rec-map-modality {X} {Y} f s) =
(compute-rec-○ f ∘ map-section f s) ∙h is-section-map-section f s


### A modal induction principle consists precisely of an induction rule and a computation rule

equiv-section-unit-induction-principle-modality :
{ l1 l2 : Level}
{ ○ : operator-modality l1 l2}
( unit-○ : unit-modality ○) →
( induction-principle-modality unit-○) ≃
Σ ( {X : UU l1} (P : ○ X → UU l1) →
((x : X) → ○ (P (unit-○ x))) → (x' : ○ X) → ○ (P x'))
( λ I →
{X : UU l1} (P : ○ X → UU l1) (f : (x : X) → ○ (P (unit-○ x))) →
I P f ∘ unit-○ ~ f)
equiv-section-unit-induction-principle-modality unit-○ =
distributive-implicit-Π-Σ ∘e
equiv-implicit-Π-equiv-family (λ _ → distributive-Π-Σ)

equiv-section-unit-recursion-principle-modality :
{ l1 l2 : Level}
{ ○ : operator-modality l1 l2}
( unit-○ : unit-modality ○) →
( recursion-principle-modality unit-○) ≃
Σ ( {X Y : UU l1} → (X → ○ Y) → ○ X → ○ Y)
( λ I → {X Y : UU l1} (f : X → ○ Y) → I f ∘ unit-○ ~ f)
equiv-section-unit-recursion-principle-modality unit-○ =
distributive-implicit-Π-Σ ∘e
equiv-implicit-Π-equiv-family (λ _ → distributive-implicit-Π-Σ)


### The modal operator's action on maps

module _
{l1 l2 : Level}
{○ : operator-modality l1 l2}
(unit-○ : unit-modality ○)
where

ap-map-rec-modality :
rec-modality unit-○ → {X Y : UU l1} → (X → Y) → ○ X → ○ Y
ap-map-rec-modality rec-○ f = rec-○ (unit-○ ∘ f)

ap-map-ind-modality :
ind-modality unit-○ → {X Y : UU l1} → (X → Y) → ○ X → ○ Y
ap-map-ind-modality ind-○ =
ap-map-rec-modality (rec-ind-modality unit-○ ind-○)


### Naturality of the unit

For every f : X → Y there is an associated naturality square

         f
X ------> Y
|         |
|         |
∨         ∨
○ X ----> ○ Y.
○ f

module _
{l1 l2 : Level}
{○ : operator-modality l1 l2}
(unit-○ : unit-modality ○)
(rec-○ : rec-modality unit-○)
(compute-rec-○ : compute-rec-modality unit-○ rec-○)
where

naturality-unit-rec-modality :
{X Y : UU l1} (f : X → Y) →
(ap-map-rec-modality unit-○ rec-○ f ∘ unit-○) ~ (unit-○ ∘ f)
naturality-unit-rec-modality f =
compute-rec-○ (unit-○ ∘ f)

naturality-unit-rec-modality' :
{X Y : UU l1} (f : X → Y) {x x' : X} →
unit-○ x ＝ unit-○ x' → unit-○ (f x) ＝ unit-○ (f x')
naturality-unit-rec-modality' f {x} {x'} p =
( inv (naturality-unit-rec-modality f x)) ∙
( ( ap (ap-map-rec-modality unit-○ rec-○ f) p) ∙
( naturality-unit-rec-modality f x'))

module _
{l1 l2 : Level}
{○ : operator-modality l1 l2}
(unit-○ : unit-modality ○)
(ind-○ : ind-modality unit-○)
(compute-ind-○ : compute-ind-modality unit-○ ind-○)
where

naturality-unit-ind-modality :
{X Y : UU l1} (f : X → Y) →
ap-map-ind-modality unit-○ ind-○ f ∘ unit-○ ~ unit-○ ∘ f
naturality-unit-ind-modality =
naturality-unit-rec-modality unit-○
( rec-ind-modality unit-○ ind-○)
( compute-rec-compute-ind-modality unit-○ ind-○ compute-ind-○)

naturality-unit-ind-modality' :
{X Y : UU l1} (f : X → Y) {x x' : X} →
unit-○ x ＝ unit-○ x' → unit-○ (f x) ＝ unit-○ (f x')
naturality-unit-ind-modality' =
naturality-unit-rec-modality' unit-○
( rec-ind-modality unit-○ ind-○)
( compute-rec-compute-ind-modality unit-○ ind-○ compute-ind-○)