Inhabited finite types

module univalent-combinatorics.inhabited-finite-types where

Imports

open import elementary-number-theory.natural-numbers

open import foundation.equivalences
open import foundation.functions
open import foundation.functoriality-dependent-function-types
open import foundation.identity-types
open import foundation.inhabited-types
open import foundation.propositions
open import foundation.subtypes
open import foundation.subuniverses
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.type-theoretic-principle-of-choice
open import foundation.universe-levels

open import univalent-combinatorics.dependent-pair-types
open import univalent-combinatorics.finite-types

Idea

An inhabited finite type is a finite type that is inhabited, meaning it is a type that is merely equivalent to a standard finite type, and that comes equipped with a term of its propositional truncation.

Definitions

Inhabited finite types

Inhabited-𝔽 : (l : Level) → UU (lsuc l)
Inhabited-𝔽 l = Σ (𝔽 l) (λ X → is-inhabited (type-𝔽 X))

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

  finite-type-Inhabited-𝔽 : 𝔽 l
  finite-type-Inhabited-𝔽 = pr1 X

  type-Inhabited-𝔽 : UU l
  type-Inhabited-𝔽 = type-𝔽 finite-type-Inhabited-𝔽

  is-finite-Inhabited-𝔽 : is-finite type-Inhabited-𝔽
  is-finite-Inhabited-𝔽 = is-finite-type-𝔽 finite-type-Inhabited-𝔽

  is-inhabited-type-Inhabited-𝔽 : is-inhabited type-Inhabited-𝔽
  is-inhabited-type-Inhabited-𝔽 = pr2 X

  inhabited-type-Inhabited-𝔽 : Inhabited-Type l
  pr1 inhabited-type-Inhabited-𝔽 = type-Inhabited-𝔽
  pr2 inhabited-type-Inhabited-𝔽 = is-inhabited-type-Inhabited-𝔽

compute-Inhabited-𝔽 :
  {l : Level} →
  Inhabited-𝔽 l ≃
    Σ (Inhabited-Type l) (λ X → is-finite (type-Inhabited-Type X))
compute-Inhabited-𝔽 = equiv-right-swap-Σ

is-finite-and-inhabited-Prop : {l : Level} → UU l → Prop l
is-finite-and-inhabited-Prop X =
  prod-Prop (is-finite-Prop X) (is-inhabited-Prop X)

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

compute-Inhabited-𝔽' :
  {l : Level} →
  Inhabited-𝔽 l ≃ type-subuniverse is-finite-and-inhabited-Prop
compute-Inhabited-𝔽' = associative-Σ _ _ _

map-compute-Inhabited-𝔽' :
  {l : Level} →
  Inhabited-𝔽 l → type-subuniverse is-finite-and-inhabited-Prop
map-compute-Inhabited-𝔽' = map-associative-Σ _ _ _

map-inv-compute-Inhabited-𝔽' :
  {l : Level} →
  type-subuniverse is-finite-and-inhabited-Prop → Inhabited-𝔽 l
map-inv-compute-Inhabited-𝔽' = map-inv-associative-Σ _ _ _

Families of inhabited types

Fam-Inhabited-Types-𝔽 :
  {l1 : Level} → (l2 : Level) → (X : 𝔽 l1) → UU (l1 ⊔ lsuc l2)
Fam-Inhabited-Types-𝔽 l2 X = type-𝔽 X → Inhabited-𝔽 l2

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

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

  finite-type-Fam-Inhabited-Types-𝔽 : type-𝔽 X → 𝔽 l2
  pr1 (finite-type-Fam-Inhabited-Types-𝔽 x) = type-Fam-Inhabited-Types-𝔽 x
  pr2 (finite-type-Fam-Inhabited-Types-𝔽 x) = is-finite-Inhabited-𝔽 (Y x)

  is-inhabited-type-Fam-Inhabited-Types-𝔽 :
    (x : type-𝔽 X) → is-inhabited (type-Fam-Inhabited-Types-𝔽 x)
  is-inhabited-type-Fam-Inhabited-Types-𝔽 x =
    is-inhabited-type-Inhabited-𝔽 (Y x)

  total-Fam-Inhabited-Types-𝔽 : 𝔽 (l1 ⊔ l2)
  total-Fam-Inhabited-Types-𝔽 = Σ-𝔽 X finite-type-Fam-Inhabited-Types-𝔽

compute-Fam-Inhabited-𝔽 :
  {l1 l2 : Level} → (X : 𝔽 l1) →
  Fam-Inhabited-Types-𝔽 l2 X ≃
    Σ ( Fam-Inhabited-Types l2 (type-𝔽 X))
      ( λ Y → ((x : (type-𝔽 X)) → is-finite (type-Inhabited-Type (Y x))))
compute-Fam-Inhabited-𝔽 X =
   ( distributive-Π-Σ ∘e
    ( equiv-Π
      ( λ _ → Σ (Inhabited-Type _) ( is-finite ∘ type-Inhabited-Type))
      ( id-equiv)
      ( λ _ → compute-Inhabited-𝔽)))

Proposition

Equality in inhabited finite types

eq-equiv-Inhabited-𝔽 :
  {l : Level} → (X Y : Inhabited-𝔽 l) →
  type-Inhabited-𝔽 X ≃ type-Inhabited-𝔽 Y → X ＝ Y
eq-equiv-Inhabited-𝔽 X Y e =
  eq-type-subtype
    ( λ X → is-inhabited-Prop (type-𝔽 X))
    ( eq-equiv-𝔽
      ( finite-type-Inhabited-𝔽 X)
      ( finite-type-Inhabited-𝔽 Y)
      ( e))

Every type in `UU-Fin (succ-ℕ n)` is a inhabited finite type

is-finite-and-inhabited-type-UU-Fin-succ-ℕ :
  {l : Level} → (n : ℕ) → (F : UU-Fin l (succ-ℕ n)) →
  is-finite-and-inhabited (type-UU-Fin (succ-ℕ n) F)
pr1 (is-finite-and-inhabited-type-UU-Fin-succ-ℕ n F) =
  is-finite-type-UU-Fin (succ-ℕ n) F
pr2 (is-finite-and-inhabited-type-UU-Fin-succ-ℕ n F) =
  is-inhabited-type-UU-Fin-succ-ℕ n F