The zero modality

Content created by Fredrik Bakke.

Created on 2023-06-08.
Last modified on 2024-11-19.

module orthogonal-factorization-systems.zero-modality where
Imports 
open import foundation.unit-type
open import foundation.universe-levels

open import orthogonal-factorization-systems.modal-operators
open import orthogonal-factorization-systems.types-local-at-maps
open import orthogonal-factorization-systems.uniquely-eliminating-modalities

Idea

The zero modality is the modality that maps every type to the unit type.

Definition

operator-zero-modality :
  (l1 l2 : Level) → operator-modality l1 l2
operator-zero-modality l1 l2 _ = raise-unit l2

unit-zero-modality :
  {l1 l2 : Level} → unit-modality (operator-zero-modality l1 l2)
unit-zero-modality _ = raise-star

Properties

The zero modality is a uniquely eliminating modality

is-uniquely-eliminating-modality-zero-modality :
  {l1 l2 : Level} →
  is-uniquely-eliminating-modality (unit-zero-modality {l1} {l2})
is-uniquely-eliminating-modality-zero-modality {l2 = l2} P =
  is-local-is-contr
    ( unit-zero-modality)
    ( raise-unit l2)
    ( is-contr-raise-unit)

The zero modality is equivalent to -2-truncation

This remains to be made formal. #739

Recent changes