Functoriality of higher modalities

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-11-24.
Last modified on 2024-02-06.

module orthogonal-factorization-systems.functoriality-higher-modalities where
Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.path-algebra
open import foundation.small-types
open import foundation.transport-along-identifications
open import foundation.univalence
open import foundation.universe-levels
open import foundation.whiskering-identifications-concatenation

open import orthogonal-factorization-systems.higher-modalities
open import orthogonal-factorization-systems.modal-induction
open import orthogonal-factorization-systems.modal-operators
open import orthogonal-factorization-systems.modal-subuniverse-induction

Idea

Every higher modality is functorial. Given a map f : A → B, there is a unique map ○f : ○A → ○B that fits into a natural square

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

This construction preserves composition, identifications, homotopies, and equivalences.

Properties

Action on maps

module _
  {l1 l2 : Level} (m : higher-modality l1 l2)
  where

  ap-map-higher-modality :
    {X Y : UU l1} 
    (X  Y)  operator-higher-modality m X  operator-higher-modality m Y
  ap-map-higher-modality =
    ap-map-ind-modality (unit-higher-modality m) (ind-higher-modality m)

Functoriality

module _
  {l : Level} (m : higher-modality l l)
  where

  functoriality-higher-modality :
    {X Y Z : UU l} (g : Y  Z) (f : X  Y) 
    ( ap-map-higher-modality m g  ap-map-higher-modality m f) ~
    ( ap-map-higher-modality m (g  f))
  functoriality-higher-modality {X} {Y} {Z} g f =
    ind-subuniverse-Id-higher-modality m
      ( ap-map-higher-modality m g  ap-map-higher-modality m f)
      ( ap-map-higher-modality m (g  f))
      ( λ x 
        ( ap
          ( ap-map-higher-modality m g)
          ( compute-rec-higher-modality m (unit-higher-modality m  f) x)) 
        ( ( compute-rec-higher-modality m (unit-higher-modality m  g) (f x)) 
          ( inv
            ( compute-rec-higher-modality m
              ( unit-higher-modality m  (g  f))
              ( x)))))

Naturality of the unit of a higher modality

For every map f : X → Y there is a naturality square

         f
    X ------> Y
    |         |
    |         |
    v         v
   ○ X ----> ○ Y.
        ○ f
module _
  {l1 l2 : Level} (m : higher-modality l1 l2)
  where

  naturality-unit-higher-modality :
    {X Y : UU l1} (f : X  Y) 
    ( ap-map-higher-modality m f  unit-higher-modality m) ~
    ( unit-higher-modality m  f)
  naturality-unit-higher-modality =
    naturality-unit-ind-modality
      ( unit-higher-modality m)
      ( ind-higher-modality m)
      ( compute-ind-higher-modality m)
  naturality-unit-higher-modality' :
    {X Y : UU l1} (f : X  Y) {x x' : X} 
    unit-higher-modality m x  unit-higher-modality m x' 
    unit-higher-modality m (f x)  unit-higher-modality m (f x')
  naturality-unit-higher-modality' =
    naturality-unit-ind-modality'
      ( unit-higher-modality m)
      ( ind-higher-modality m)
      ( compute-ind-higher-modality m)

module _
  {l : Level} (m : higher-modality l l)
  where

  compute-naturality-unit-ind-modality :
    {X Y Z : UU l} (g : Y  Z) (f : X  Y) (x : X) 
    ( ( functoriality-higher-modality m g f (unit-higher-modality m x)) 
      ( naturality-unit-higher-modality m (g  f) x)) 
    ( ( ap
        ( ap-map-higher-modality m g)
        ( naturality-unit-higher-modality m f x)) 
      ( naturality-unit-higher-modality m g (f x)))
  compute-naturality-unit-ind-modality g f x =
    ( right-whisker-concat
      ( compute-ind-subuniverse-Id-higher-modality m
        ( ap-map-higher-modality m g  ap-map-higher-modality m f)
        ( ap-map-higher-modality m (g  f))
        ( _)
        ( x))
      ( compute-rec-higher-modality m (unit-higher-modality m  (g  f)) x)) 
    ( assoc
      ( ap
        ( ap-map-higher-modality m g)
        ( compute-rec-higher-modality m (unit-higher-modality m  f) x))
      ( ( compute-rec-higher-modality m (unit-higher-modality m  g) (f x)) 
        ( inv
          ( compute-rec-higher-modality m (unit-higher-modality m  g  f) x)))
      ( compute-rec-higher-modality m (unit-higher-modality m  g  f) x)) 
    ( left-whisker-concat
      ( ap
        ( ap-map-higher-modality m g)
        ( compute-rec-higher-modality m (unit-higher-modality m  f) x))
      ( is-section-inv-concat'
        ( compute-rec-higher-modality m (unit-higher-modality m  g  f) x)
        ( compute-rec-higher-modality m (unit-higher-modality m  g) (f x))))

Action on homotopies

This definition of action on homotopies is meant to avoid using function extensionality. This is left for future work.

module _
  {l : Level} (m : higher-modality l l)
  where

  htpy-ap-higher-modality :
    {X Y : UU l} {f g : X  Y} 
    f ~ g  ap-map-higher-modality m f ~ ap-map-higher-modality m g
  htpy-ap-higher-modality H x' =
    ap  f  ap-map-higher-modality m f x') (eq-htpy H)

References

Recent changes