Inhabited types

module foundation.inhabited-types where
Imports
open import foundation.equality-dependent-function-types
open import foundation.functoriality-propositional-truncation
open import foundation.propositional-truncations
open import foundation.univalence

open import foundation-core.contractible-types
open import foundation-core.dependent-pair-types
open import foundation-core.equivalences
open import foundation-core.fundamental-theorem-of-identity-types
open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.subtype-identity-principle
open import foundation-core.universe-levels

Idea

Inhabited types are types equipped with an element of its propositional truncation.

Remark: This contrasts with the definition of pointed types in that we do not discern between proofs of inhabitedness, so that it is merely a property of the type to be inhabited.

Definitions

Inhabited types

is-inhabited-Prop : {l : Level}  UU l  Prop l
is-inhabited-Prop X = trunc-Prop X

is-inhabited : {l : Level}  UU l  UU l
is-inhabited X = type-Prop (is-inhabited-Prop X)

is-property-is-inhabited : {l : Level}  (X : UU l)  is-prop (is-inhabited X)
is-property-is-inhabited X = is-prop-type-Prop (is-inhabited-Prop X)

Inhabited-Type : (l : Level)  UU (lsuc l)
Inhabited-Type l = Σ (UU l) is-inhabited

module _
  {l : Level} (X : Inhabited-Type l)
  where

  type-Inhabited-Type : UU l
  type-Inhabited-Type = pr1 X

  is-inhabited-type-Inhabited-Type : type-trunc-Prop type-Inhabited-Type
  is-inhabited-type-Inhabited-Type = pr2 X

Families of inhabited types

Fam-Inhabited-Types :
  {l1 : Level} (l2 : Level)  UU l1  UU (l1  lsuc l2)
Fam-Inhabited-Types l2 X = X  Inhabited-Type l2

module _
  {l1 l2 : Level} {X : UU l1} (Y : Fam-Inhabited-Types l2 X)
  where

  type-Fam-Inhabited-Types : X  UU l2
  type-Fam-Inhabited-Types x = type-Inhabited-Type (Y x)

  is-inhabited-type-Fam-Inhabited-Types :
    (x : X)  type-trunc-Prop (type-Fam-Inhabited-Types x)
  is-inhabited-type-Fam-Inhabited-Types x =
    is-inhabited-type-Inhabited-Type (Y x)

  total-Fam-Inhabited-Types : UU (l1  l2)
  total-Fam-Inhabited-Types = Σ X type-Fam-Inhabited-Types

Properties

Characterization of equality of inhabited types

equiv-Inhabited-Type :
  {l1 l2 : Level}  Inhabited-Type l1  Inhabited-Type l2  UU (l1  l2)
equiv-Inhabited-Type X Y = type-Inhabited-Type X  type-Inhabited-Type Y

module _
  {l : Level} (X : Inhabited-Type l)
  where

  is-contr-total-equiv-Inhabited-Type :
    is-contr (Σ (Inhabited-Type l) (equiv-Inhabited-Type X))
  is-contr-total-equiv-Inhabited-Type =
    is-contr-total-Eq-subtype
      ( is-contr-total-equiv (type-Inhabited-Type X))
      ( λ X  is-prop-type-trunc-Prop)
      ( type-Inhabited-Type X)
      ( id-equiv)
      ( is-inhabited-type-Inhabited-Type X)

  equiv-eq-Inhabited-Type :
    (Y : Inhabited-Type l)  (X  Y)  equiv-Inhabited-Type X Y
  equiv-eq-Inhabited-Type .X refl = id-equiv

  is-equiv-equiv-eq-Inhabited-Type :
    (Y : Inhabited-Type l)  is-equiv (equiv-eq-Inhabited-Type Y)
  is-equiv-equiv-eq-Inhabited-Type =
    fundamental-theorem-id
      is-contr-total-equiv-Inhabited-Type
      equiv-eq-Inhabited-Type

  extensionality-Inhabited-Type :
    (Y : Inhabited-Type l)  (X  Y)  equiv-Inhabited-Type X Y
  pr1 (extensionality-Inhabited-Type Y) = equiv-eq-Inhabited-Type Y
  pr2 (extensionality-Inhabited-Type Y) = is-equiv-equiv-eq-Inhabited-Type Y

  eq-equiv-Inhabited-Type :
    (Y : Inhabited-Type l)  equiv-Inhabited-Type X Y  (X  Y)
  eq-equiv-Inhabited-Type Y =
    map-inv-equiv (extensionality-Inhabited-Type Y)

Characterization of equality of families of inhabited types

equiv-Fam-Inhabited-Types :
  {l1 l2 l3 : Level} {X : UU l1} 
  Fam-Inhabited-Types l2 X  Fam-Inhabited-Types l3 X  UU (l1  l2  l3)
equiv-Fam-Inhabited-Types {X = X} Y Z =
  (x : X)  equiv-Inhabited-Type (Y x) (Z x)

module _
  {l1 l2 : Level} {X : UU l1} (Y : Fam-Inhabited-Types l2 X)
  where

  id-equiv-Fam-Inhabited-Types : equiv-Fam-Inhabited-Types Y Y
  id-equiv-Fam-Inhabited-Types = id-equiv-fam (type-Fam-Inhabited-Types Y)

  is-contr-total-equiv-Fam-Inhabited-Types :
    is-contr (Σ (Fam-Inhabited-Types l2 X) (equiv-Fam-Inhabited-Types Y))
  is-contr-total-equiv-Fam-Inhabited-Types =
    is-contr-total-Eq-Π
      ( λ x  equiv-Inhabited-Type (Y x))
      ( λ x  is-contr-total-equiv-Inhabited-Type (Y x))

  equiv-eq-Fam-Inhabited-Types :
    (Z : Fam-Inhabited-Types l2 X)  (Y  Z)  equiv-Fam-Inhabited-Types Y Z
  equiv-eq-Fam-Inhabited-Types .Y refl = id-equiv-Fam-Inhabited-Types

  is-equiv-equiv-eq-Fam-Inhabited-Types :
    (Z : Fam-Inhabited-Types l2 X)  is-equiv (equiv-eq-Fam-Inhabited-Types Z)
  is-equiv-equiv-eq-Fam-Inhabited-Types =
    fundamental-theorem-id
      is-contr-total-equiv-Fam-Inhabited-Types
      equiv-eq-Fam-Inhabited-Types

Inhabited types are closed under Σ

is-inhabited-Σ :
  {l1 l2 : Level} {X : UU l1} {Y : X  UU l2} 
  is-inhabited X  ((x : X)  is-inhabited (Y x))  is-inhabited (Σ X Y)
is-inhabited-Σ {l1} {l2} {X} {Y} H K =
  apply-universal-property-trunc-Prop H
    ( is-inhabited-Prop (Σ X Y))
    ( λ x 
      apply-universal-property-trunc-Prop
        ( K x)
        ( is-inhabited-Prop (Σ X Y))
        ( λ y  unit-trunc-Prop (x , y)))

Σ-Inhabited-Type :
  {l1 l2 : Level} (X : Inhabited-Type l1)
  (Y : type-Inhabited-Type X  Inhabited-Type l2)  Inhabited-Type (l1  l2)
pr1 (Σ-Inhabited-Type X Y) =
  Σ (type-Inhabited-Type X)  x  type-Inhabited-Type (Y x))
pr2 (Σ-Inhabited-Type X Y) =
  is-inhabited-Σ
    ( is-inhabited-type-Inhabited-Type X)
    ( λ x  is-inhabited-type-Inhabited-Type (Y x))

Inhabited types are closed under maps

map-is-inhabited :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} 
  (f : (A  B))  is-inhabited A  is-inhabited B
map-is-inhabited f = map-trunc-Prop f

Contractible types are inhabited

is-inhabited-is-contr :
  {l1 : Level} {A : UU l1}  is-contr A  is-inhabited A
is-inhabited-is-contr p =
  unit-trunc-Prop (center p)

See also