Null types

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-05-09.
Last modified on 2023-06-10.

module orthogonal-factorization-systems.null-types where
open import foundation.constant-maps
open import foundation.equivalences
open import foundation.function-types
open import foundation.propositions
open import foundation.type-arithmetic-unit-type
open import foundation.unit-type
open import foundation.universe-levels

open import orthogonal-factorization-systems.local-types


A type A is said to be null at Y, or Y-null, if the constant map

  const : A → (Y → A)

is an equivalence. The idea is that A observes the type Y to be contractible.


module _
  {l1 l2 : Level} (Y : UU l1) (A : UU l2)

  is-null : UU (l1  l2)
  is-null = is-equiv (const Y A)


A type is Y-null if and only if it is local at the terminal projection Y → unit

module _
  {l1 l2 : Level} (Y : UU l1) (A : UU l2)

  is-local-is-null : is-null Y A  is-local  y  star) A
  is-local-is-null =
      ( const Y A)
      ( map-left-unit-law-function-type A)
      ( is-equiv-map-left-unit-law-function-type A)

  is-null-is-local : is-local  y  star) A  is-null Y A
  is-null-is-local =
      ( precomp  y  star) A)
      ( map-inv-left-unit-law-function-type A)
      ( is-equiv-map-inv-left-unit-law-function-type A)

  equiv-is-local-is-null : is-null Y A  is-local  y  star) A
  equiv-is-local-is-null =
      ( is-property-is-equiv (const Y A))
      ( is-property-is-equiv (precomp  y  star) A))
      ( is-local-is-null)
      ( is-null-is-local)

  equiv-is-null-is-local : is-local  y  star) A  is-null Y A
  equiv-is-null-is-local = inv-equiv equiv-is-local-is-null

Recent changes