Null types

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-05-09.
Last modified on 2024-11-19.

module orthogonal-factorization-systems.null-types where
Imports 
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.diagonal-maps-of-types
open import foundation.equivalences
open import foundation.equivalences-arrows
open import foundation.fibers-of-maps
open import foundation.function-extensionality
open import foundation.homotopies
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.postcomposition-functions
open import foundation.precomposition-dependent-functions
open import foundation.precomposition-functions
open import foundation.propositions
open import foundation.retracts-of-maps
open import foundation.retracts-of-types
open import foundation.type-arithmetic-unit-type
open import foundation.unit-type
open import foundation.universal-property-equivalences
open import foundation.universal-property-family-of-fibers-of-maps
open import foundation.universal-property-unit-type
open import foundation.universe-levels

open import orthogonal-factorization-systems.maps-local-at-maps
open import orthogonal-factorization-systems.orthogonal-maps
open import orthogonal-factorization-systems.types-local-at-maps

Idea

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

  Δ : A → (Y → A)

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

Definitions

The predicate on a type of being Y-null

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

  is-null : UU (l1 ⊔ l2)
  is-null = is-equiv (diagonal-exponential A Y)

  is-prop-is-null : is-prop is-null
  is-prop-is-null = is-property-is-equiv (diagonal-exponential A Y)

  is-null-Prop : Prop (l1 ⊔ l2)
  pr1 is-null-Prop = is-null
  pr2 is-null-Prop = is-prop-is-null

Properties

Closure under equivalences

If B is Y-null and we have equivalences X ≃ Y and A ≃ B, then A is X-null.

module _
  {l1 l2 l3 l4 : Level} {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4}
  where

  is-null-equiv : (e : X ≃ Y) (f : A ≃ B) → is-null Y B → is-null X A
  is-null-equiv e f H =
    is-equiv-htpy-equiv
      ( equiv-precomp e A ∘e equiv-postcomp Y (inv-equiv f) ∘e (_ , H) ∘e f)
      ( λ x → eq-htpy (λ _ → inv (is-retraction-map-inv-equiv f x)))

module _
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} {A : UU l3}
  where

  is-null-equiv-exponent : (e : X ≃ Y) → is-null Y A → is-null X A
  is-null-equiv-exponent e H =
    is-equiv-comp
      ( precomp (map-equiv e) A)
      ( diagonal-exponential A Y)
      ( H)
      ( is-equiv-precomp-equiv e A)

module _
  {l1 l2 l3 : Level} {Y : UU l1} {A : UU l2} {B : UU l3}
  where

  is-null-equiv-base : (f : A ≃ B) → is-null Y B → is-null Y A
  is-null-equiv-base f H =
    is-equiv-htpy-equiv
      ( equiv-postcomp Y (inv-equiv f) ∘e (_ , H) ∘e f)
      ( λ b → eq-htpy (λ _ → inv (is-retraction-map-inv-equiv f b)))

Closure under retracts

If B is Y-null and X is a retract of Y and A is a retract of B, then A is X-null.

module _
  {l1 l2 l3 l4 : Level} {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4}
  where

  is-null-retract :
    X retract-of Y → A retract-of B → is-null Y B → is-null X A
  is-null-retract e f =
    is-equiv-retract-map-is-equiv
      ( diagonal-exponential A X)
      ( diagonal-exponential B Y)
      ( retract-map-diagonal-exponential-retract f e)

module _
  {l1 l2 l3 : Level} {Y : UU l1} {A : UU l2} {B : UU l3}
  where

  is-null-retract-base : A retract-of B → is-null Y B → is-null Y A
  is-null-retract-base = is-null-retract id-retract

module _
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} {A : UU l3}
  where

  is-null-retract-exponent : X retract-of Y → is-null Y A → is-null X A
  is-null-retract-exponent e = is-null-retract e id-retract

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)
  where

  is-local-terminal-map-is-null : is-null Y A → is-local (terminal-map Y) A
  is-local-terminal-map-is-null =
    is-equiv-comp
      ( diagonal-exponential A Y)
      ( map-left-unit-law-function-type A)
      ( is-equiv-map-left-unit-law-function-type A)

  is-null-is-local-terminal-map : is-local (terminal-map Y) A → is-null Y A
  is-null-is-local-terminal-map =
    is-equiv-comp
      ( precomp (terminal-map Y) A)
      ( map-inv-left-unit-law-function-type A)
      ( is-equiv-map-inv-left-unit-law-function-type A)

  equiv-is-local-terminal-map-is-null :
    is-null Y A ≃ is-local (terminal-map Y) A
  equiv-is-local-terminal-map-is-null =
    equiv-iff-is-prop
      ( is-property-is-equiv (diagonal-exponential A Y))
      ( is-property-is-equiv (precomp (terminal-map Y) A))
      ( is-local-terminal-map-is-null)
      ( is-null-is-local-terminal-map)

  equiv-is-null-is-local-terminal-map :
    is-local (terminal-map Y) A ≃ is-null Y A
  equiv-is-null-is-local-terminal-map =
    inv-equiv equiv-is-local-terminal-map-is-null

A type is Y-null if and only if the terminal projection of Y is orthogonal to the terminal projection of A

module _
  {l1 l2 : Level} {Y : UU l1} {A : UU l2}
  where

  is-null-is-orthogonal-terminal-maps :
    is-orthogonal (terminal-map Y) (terminal-map A) → is-null Y A
  is-null-is-orthogonal-terminal-maps H =
    is-null-is-local-terminal-map Y A
      ( is-local-is-orthogonal-terminal-map (terminal-map Y) H)

  is-orthogonal-terminal-maps-is-null :
    is-null Y A → is-orthogonal (terminal-map Y) (terminal-map A)
  is-orthogonal-terminal-maps-is-null H =
    is-orthogonal-is-orthogonal-fiber-condition-right-map
      ( terminal-map Y)
      ( terminal-map A)
      ( λ _ →
        is-equiv-source-is-equiv-target-equiv-arrow
          ( precomp (terminal-map Y) (fiber (terminal-map A) star))
          ( diagonal-exponential A Y)
          ( ( equiv-fiber-terminal-map star) ∘e
            ( equiv-universal-property-unit (fiber (terminal-map A) star)) ,
            ( equiv-postcomp Y (equiv-fiber-terminal-map star)) ,
            ( refl-htpy))
          ( H))

A type is f-local if it is null at every fiber of f

module _
  {l1 l2 l3 : Level} {Y : UU l1} {X : UU l2} (f : Y → X)
  where

  is-local-dependent-type-is-null-fiber :
    (A : X → UU l3) →
    ((x : X) → is-null (fiber f x) (A x)) → is-local-dependent-type f A
  is-local-dependent-type-is-null-fiber A = is-equiv-precomp-Π-fiber-condition

  is-local-is-null-fiber :
    (A : UU l3) → ((x : X) → is-null (fiber f x) A) → is-local f A
  is-local-is-null-fiber A = is-local-dependent-type-is-null-fiber (λ _ → A)

Contractible types are null at all types

is-null-is-contr :
  {l1 l2 : Level} {A : UU l1} (B : UU l2) → is-contr A → is-null B A
is-null-is-contr {A = A} B is-contr-A =
  is-null-is-local-terminal-map B A
    ( is-local-is-contr (terminal-map B) A is-contr-A)

Recent changes