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