Functoriality of the sharp modality

Content created by Fredrik Bakke.

Created on 2024-09-06.
Last modified on 2024-09-06.

{-# OPTIONS --cohesion --flat-split #-}

module modal-type-theory.functoriality-sharp-modality where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.locally-small-types
open import foundation.universe-levels

open import modal-type-theory.sharp-modality

open import orthogonal-factorization-systems.locally-small-modal-operators
open import orthogonal-factorization-systems.modal-induction
open import orthogonal-factorization-systems.modal-subuniverse-induction

Idea

The sharp 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.

Definitions

The sharp modality’s action on maps

action-sharp-map :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} → (A → B) → (♯ A → ♯ B)
action-sharp-map f = rec-sharp (unit-sharp ∘ f)

Recent changes