This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Null families of types

module orthogonal-factorization-systems.null-families-of-types where

Imports

open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.precomposition-functions
open import foundation.propositions
open import foundation.retracts-of-types
open import foundation.universe-levels

open import orthogonal-factorization-systems.null-types
open import orthogonal-factorization-systems.orthogonal-maps

Idea

A family of types B : A → UU l is said to be null^¶ at Y, or Y-null, if every fiber is. I.e., if the diagonal map

  Δ : B x → (Y → B x)

is an equivalence for every x in A.

Definitions

`Y`-null families of types

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

  is-null-family : UU (l1 ⊔ l2 ⊔ l3)
  is-null-family = (x : A) → is-null Y (B x)

  is-property-is-null-family : is-prop is-null-family
  is-property-is-null-family =
    is-prop-Π (λ x → is-prop-is-null Y (B x))

  is-null-family-Prop : Prop (l1 ⊔ l2 ⊔ l3)
  is-null-family-Prop = (is-null-family , is-property-is-null-family)

Properties

Closure under equivalences

If C is Y-null and we have equivalences X ≃ Y and (x : A) → B x ≃ C x, then B is X-null.

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

  is-null-family-equiv :
    {l5 : Level} {C : A → UU l5} →
    X ≃ Y → ((x : A) → B x ≃ C x) →
    is-null-family Y C → is-null-family X B
  is-null-family-equiv e f H x = is-null-equiv e (f x) (H x)

  is-null-family-equiv-exponent :
    (e : X ≃ Y) → is-null-family Y B → is-null-family X B
  is-null-family-equiv-exponent e H x = is-null-equiv-exponent e (H x)

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

  is-null-family-equiv-family :
    ((x : A) → B x ≃ C x) → is-null-family Y C → is-null-family Y B
  is-null-family-equiv-family f H x = is-null-equiv-base (f x) (H x)

Closure under retracts

If C is Y-null and X is a retract of Y and B x is a retract of C x for all x, then B is X-null.

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

  is-null-family-retract :
    X retract-of Y → ((x : A) → (B x) retract-of (C x)) →
    is-null-family Y C → is-null-family X B
  is-null-family-retract e f H x = is-null-retract e (f x) (H x)

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

  is-null-family-retract-family :
    ((x : A) → (B x) retract-of (C x)) → is-null-family Y C → is-null-family Y B
  is-null-family-retract-family f H x = is-null-retract-base (f x) (H x)

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

  is-null-family-retract-exponent :
    X retract-of Y → is-null-family Y B → is-null-family X B
  is-null-family-retract-exponent e H x = is-null-retract-exponent e (H x)

agda-unimath