Finite types

module univalent-combinatorics.finite-types where
Imports
open import elementary-number-theory.equality-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.0-connected-types
open import foundation.1-types
open import foundation.connected-components-universes
open import foundation.contractible-types
open import foundation.coproduct-types
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.equivalences
open import foundation.functions
open import foundation.functoriality-coproduct-types
open import foundation.functoriality-dependent-pair-types
open import foundation.functoriality-propositional-truncation
open import foundation.identity-types
open import foundation.inhabited-types
open import foundation.mere-equivalences
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.raising-universe-levels
open import foundation.sets
open import foundation.subtypes
open import foundation.subuniverses
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.type-arithmetic-empty-type
open import foundation.unit-type
open import foundation.univalence
open import foundation.universe-levels

open import univalent-combinatorics.counting
open import univalent-combinatorics.standard-finite-types

Idea

A type is finite if it is merely equivalent to a standard finite type.

Definition

Finite types

is-finite-Prop :
  {l : Level}  UU l  Prop l
is-finite-Prop X = trunc-Prop (count X)

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

abstract
  is-prop-is-finite :
    {l : Level} (X : UU l)  is-prop (is-finite X)
  is-prop-is-finite X = is-prop-type-Prop (is-finite-Prop X)

abstract
  is-finite-count :
    {l : Level} {X : UU l}  count X  is-finite X
  is-finite-count = unit-trunc-Prop

The type of all finite types of a universe level

𝔽 : (l : Level)  UU (lsuc l)
𝔽 l = Σ (UU l) is-finite

type-𝔽 : {l : Level}  𝔽 l  UU l
type-𝔽 X = pr1 X

is-finite-type-𝔽 :
  {l : Level} (X : 𝔽 l)  is-finite (type-𝔽 X)
is-finite-type-𝔽 X = pr2 X

Types with cardinality k

has-cardinality-Prop :
  {l : Level}    UU l  Prop l
has-cardinality-Prop k X = mere-equiv-Prop (Fin k) X

has-cardinality :
  {l : Level}    UU l  UU l
has-cardinality k X = mere-equiv (Fin k) X

The type of all types of cardinality k of a given universe leve l

UU-Fin : (l : Level)    UU (lsuc l)
UU-Fin l k = Σ (UU l) (mere-equiv (Fin k))

type-UU-Fin : {l : Level} (k : )  UU-Fin l k  UU l
type-UU-Fin k X = pr1 X

abstract
  has-cardinality-type-UU-Fin :
    {l : Level} (k : ) (X : UU-Fin l k) 
    mere-equiv (Fin k) (type-UU-Fin k X)
  has-cardinality-type-UU-Fin k X = pr2 X

Types of finite cardinality

has-finite-cardinality :
  {l : Level}  UU l  UU l
has-finite-cardinality X = Σ   k  has-cardinality k X)

number-of-elements-has-finite-cardinality :
  {l : Level} {X : UU l}  has-finite-cardinality X  
number-of-elements-has-finite-cardinality = pr1

abstract
  mere-equiv-has-finite-cardinality :
    {l : Level} {X : UU l} (c : has-finite-cardinality X) 
    type-trunc-Prop (Fin (number-of-elements-has-finite-cardinality c)  X)
  mere-equiv-has-finite-cardinality = pr2

Properties

Finite types are closed under equivalences

abstract
  is-finite-equiv :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A  B) 
    is-finite A  is-finite B
  is-finite-equiv e =
    map-universal-property-trunc-Prop
      ( is-finite-Prop _)
      ( is-finite-count  (count-equiv e))

abstract
  is-finite-is-equiv :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A  B} 
    is-equiv f  is-finite A  is-finite B
  is-finite-is-equiv is-equiv-f =
    map-universal-property-trunc-Prop
      ( is-finite-Prop _)
      ( is-finite-count  (count-equiv (pair _ is-equiv-f)))

abstract
  is-finite-equiv' :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A  B) 
    is-finite B  is-finite A
  is-finite-equiv' e = is-finite-equiv (inv-equiv e)

Finite types are closed under mere equivalences

abstract
  is-finite-mere-equiv :
    {l1 l2 : Level} {A : UU l1} {B : UU l2}  mere-equiv A B 
    is-finite A  is-finite B
  is-finite-mere-equiv e H =
    apply-universal-property-trunc-Prop e
      ( is-finite-Prop _)
      ( λ e'  is-finite-equiv e' H)

The empty type is finite

abstract
  is-finite-empty : is-finite empty
  is-finite-empty = is-finite-count count-empty

empty-𝔽 : 𝔽 lzero
pr1 empty-𝔽 = empty
pr2 empty-𝔽 = is-finite-empty

empty-UU-Fin : UU-Fin lzero zero-ℕ
pr1 empty-UU-Fin = empty
pr2 empty-UU-Fin = unit-trunc-Prop id-equiv

The empty type has finite cardinality

has-finite-cardinality-empty : has-finite-cardinality empty
pr1 has-finite-cardinality-empty = zero-ℕ
pr2 has-finite-cardinality-empty = unit-trunc-Prop id-equiv

Empty types are finite

abstract
  is-finite-is-empty :
    {l1 : Level} {X : UU l1}  is-empty X  is-finite X
  is-finite-is-empty H = is-finite-count (count-is-empty H)

Empty types have finite cardinality

has-finite-cardinality-is-empty :
  {l1 : Level} {X : UU l1}  is-empty X  has-finite-cardinality X
pr1 (has-finite-cardinality-is-empty f) = zero-ℕ
pr2 (has-finite-cardinality-is-empty f) =
  unit-trunc-Prop (equiv-count (count-is-empty f))

The unit type is finite

abstract
  is-finite-unit : is-finite unit
  is-finite-unit = is-finite-count count-unit

abstract
  is-finite-raise-unit :
    {l1 : Level}  is-finite (raise-unit l1)
  is-finite-raise-unit {l1} =
    is-finite-equiv (compute-raise-unit l1) is-finite-unit

unit-𝔽 : 𝔽 lzero
pr1 unit-𝔽 = unit
pr2 unit-𝔽 = is-finite-unit

unit-UU-Fin : UU-Fin lzero 1
pr1 unit-UU-Fin = unit
pr2 unit-UU-Fin = unit-trunc-Prop (left-unit-law-coprod unit)

Contractible types are finite

abstract
  is-finite-is-contr :
    {l1 : Level} {X : UU l1}  is-contr X  is-finite X
  is-finite-is-contr H = is-finite-count (count-is-contr H)

abstract
  has-cardinality-is-contr :
    {l1 : Level} {X : UU l1}  is-contr X  has-cardinality 1 X
  has-cardinality-is-contr H =
    unit-trunc-Prop (equiv-is-contr is-contr-Fin-one-ℕ H)

The standard finite types are finite

abstract
  is-finite-Fin : (k : )  is-finite (Fin k)
  is-finite-Fin k = is-finite-count (count-Fin k)

Fin-𝔽 :   𝔽 lzero
pr1 (Fin-𝔽 k) = Fin k
pr2 (Fin-𝔽 k) = is-finite-Fin k

has-cardinality-raise-Fin :
  {l : Level} (k : )  has-cardinality k (raise-Fin l k)
has-cardinality-raise-Fin {l} k = unit-trunc-Prop (compute-raise-Fin l k)

Fin-UU-Fin : (l : Level) (k : )  UU-Fin l k
pr1 (Fin-UU-Fin l k) = raise-Fin l k
pr2 (Fin-UU-Fin l k) = has-cardinality-raise-Fin k

Fin-UU-Fin' : (k : )  UU-Fin lzero k
pr1 (Fin-UU-Fin' k) = Fin k
pr2 (Fin-UU-Fin' k) = unit-trunc-Prop id-equiv

Every type of cardinality k is finite

abstract
  is-finite-type-UU-Fin :
    {l : Level} (k : ) (X : UU-Fin l k) 
    is-finite (type-UU-Fin k X)
  is-finite-type-UU-Fin k X =
    is-finite-mere-equiv
      ( has-cardinality-type-UU-Fin k X)
      ( is-finite-Fin k)

finite-type-UU-Fin : {l : Level} (k : )  UU-Fin l k  𝔽 l
pr1 (finite-type-UU-Fin k X) = type-UU-Fin k X
pr2 (finite-type-UU-Fin k X) = is-finite-type-UU-Fin k X

Having a finite cardinality is a proposition

abstract
  all-elements-equal-has-finite-cardinality :
    {l1 : Level} {X : UU l1}  all-elements-equal (has-finite-cardinality X)
  all-elements-equal-has-finite-cardinality {l1} {X} (pair k K) (pair l L) =
    eq-type-subtype
      ( λ k  mere-equiv-Prop (Fin k) X)
      ( apply-universal-property-trunc-Prop K
        ( pair (Id k l) (is-set-ℕ k l))
        ( λ (e : Fin k  X) 
          apply-universal-property-trunc-Prop L
            ( pair (Id k l) (is-set-ℕ k l))
            ( λ (f : Fin l  X)  is-injective-Fin ((inv-equiv f) ∘e e))))

abstract
  is-prop-has-finite-cardinality :
    {l1 : Level} {X : UU l1}  is-prop (has-finite-cardinality X)
  is-prop-has-finite-cardinality =
    is-prop-all-elements-equal all-elements-equal-has-finite-cardinality

has-finite-cardinality-Prop :
  {l1 : Level} (X : UU l1)  Prop l1
pr1 (has-finite-cardinality-Prop X) = has-finite-cardinality X
pr2 (has-finite-cardinality-Prop X) = is-prop-has-finite-cardinality

A type has a finite cardinality if and only if it is finite

module _
  {l : Level} {X : UU l}
  where

  abstract
    is-finite-has-finite-cardinality : has-finite-cardinality X  is-finite X
    is-finite-has-finite-cardinality (pair k K) =
      apply-universal-property-trunc-Prop K
        ( is-finite-Prop X)
        ( is-finite-count  (pair k))

  abstract
    is-finite-has-cardinality : (k : )  has-cardinality k X  is-finite X
    is-finite-has-cardinality k H =
      is-finite-has-finite-cardinality (pair k H)

  has-finite-cardinality-count : count X  has-finite-cardinality X
  pr1 (has-finite-cardinality-count e) = number-of-elements-count e
  pr2 (has-finite-cardinality-count e) = unit-trunc-Prop (equiv-count e)

  abstract
    has-finite-cardinality-is-finite : is-finite X  has-finite-cardinality X
    has-finite-cardinality-is-finite =
      map-universal-property-trunc-Prop
        ( has-finite-cardinality-Prop X)
        ( has-finite-cardinality-count)

  number-of-elements-is-finite : is-finite X  
  number-of-elements-is-finite =
    number-of-elements-has-finite-cardinality  has-finite-cardinality-is-finite

  abstract
    mere-equiv-is-finite :
      (f : is-finite X)  mere-equiv (Fin (number-of-elements-is-finite f)) X
    mere-equiv-is-finite f =
      mere-equiv-has-finite-cardinality (has-finite-cardinality-is-finite f)

  abstract
    compute-number-of-elements-is-finite :
      (e : count X) (f : is-finite X) 
      Id (number-of-elements-count e) (number-of-elements-is-finite f)
    compute-number-of-elements-is-finite e f =
      ind-trunc-Prop
        ( λ g 
          Id-Prop ℕ-Set
            ( number-of-elements-count e)
            ( number-of-elements-is-finite g))
        ( λ g 
          ( is-injective-Fin ((inv-equiv (equiv-count g)) ∘e (equiv-count e))) 
          ( ap pr1
            ( eq-is-prop' is-prop-has-finite-cardinality
              ( has-finite-cardinality-count g)
              ( has-finite-cardinality-is-finite (unit-trunc-Prop g)))))
        ( f)

  has-cardinality-is-finite :
    (H : is-finite X)  has-cardinality (number-of-elements-is-finite H) X
  has-cardinality-is-finite H =
    pr2 (has-finite-cardinality-is-finite H)

number-of-elements-𝔽 : {l : Level}  𝔽 l  
number-of-elements-𝔽 X = number-of-elements-is-finite (is-finite-type-𝔽 X)

If a type has cardinality k and cardinality l, then k = l

eq-cardinality :
  {l1 : Level} {k l : } {A : UU l1} 
  has-cardinality k A  has-cardinality l A  Id k l
eq-cardinality H K =
  apply-universal-property-trunc-Prop H
    ( Id-Prop ℕ-Set _ _)
    ( λ e 
      apply-universal-property-trunc-Prop K
        ( Id-Prop ℕ-Set _ _)
        ( λ f  is-injective-Fin (inv-equiv f ∘e e)))

Any finite type is a set

abstract
  is-set-is-finite :
    {l : Level} {X : UU l}  is-finite X  is-set X
  is-set-is-finite {l} {X} H =
    apply-universal-property-trunc-Prop H
      ( is-set-Prop X)
      ( λ e  is-set-count e)

is-set-type-𝔽 : {l : Level} (X : 𝔽 l)  is-set (type-𝔽 X)
is-set-type-𝔽 X = is-set-is-finite (is-finite-type-𝔽 X)

set-𝔽 : {l : Level}  𝔽 l  Set l
pr1 (set-𝔽 X) = type-𝔽 X
pr2 (set-𝔽 X) = is-set-is-finite (is-finite-type-𝔽 X)

Any type of cardinality k is a set

is-set-has-cardinality :
  {l1 : Level} {X : UU l1} (k : )  has-cardinality k X  is-set X
is-set-has-cardinality k H = is-set-mere-equiv' H (is-set-Fin k)

is-set-type-UU-Fin :
  {l : Level} (k : ) (X : UU-Fin l k)  is-set (type-UU-Fin k X)
is-set-type-UU-Fin k X =
  is-set-has-cardinality k (has-cardinality-type-UU-Fin k X)

set-UU-Fin : {l1 : Level} (k : )  UU-Fin l1 k  Set l1
pr1 (set-UU-Fin k X) = type-UU-Fin k X
pr2 (set-UU-Fin k X) = is-set-type-UU-Fin k X

A finite type is empty if and only if it has 0 elements

abstract
  is-empty-is-zero-number-of-elements-is-finite :
    {l1 : Level} {X : UU l1} (f : is-finite X) 
    is-zero-ℕ (number-of-elements-is-finite f)  is-empty X
  is-empty-is-zero-number-of-elements-is-finite {l1} {X} f p =
    apply-universal-property-trunc-Prop f
      ( is-empty-Prop X)
      ( λ e 
        is-empty-is-zero-number-of-elements-count e
          ( compute-number-of-elements-is-finite e f  p))

A finite type is contractible if and only if it has one element

is-one-number-of-elements-is-finite-is-contr :
  {l : Level} {X : UU l} (H : is-finite X) 
  is-contr X  is-one-ℕ (number-of-elements-is-finite H)
is-one-number-of-elements-is-finite-is-contr H K =
  eq-cardinality
    ( has-cardinality-is-finite H)
    ( has-cardinality-is-contr K)

is-contr-is-one-number-of-elements-is-finite :
  {l : Level} {X : UU l} (H : is-finite X) 
  is-one-ℕ (number-of-elements-is-finite H)  is-contr X
is-contr-is-one-number-of-elements-is-finite H p =
  apply-universal-property-trunc-Prop H
    ( is-contr-Prop _)
    ( λ e 
      is-contr-equiv'
        ( Fin 1)
        ( ( equiv-count e) ∘e
          ( equiv-tr Fin
            ( inv p  inv (compute-number-of-elements-is-finite e H))))
        ( is-contr-Fin-one-ℕ))

is-decidable-is-contr-is-finite :
  {l : Level} {X : UU l} (H : is-finite X)  is-decidable (is-contr X)
is-decidable-is-contr-is-finite H =
  is-decidable-iff
    ( is-contr-is-one-number-of-elements-is-finite H)
    ( is-one-number-of-elements-is-finite-is-contr H)
    ( has-decidable-equality-ℕ (number-of-elements-is-finite H) 1)

The type of all pairs consisting of a natural number k and a type of cardinality k is equivalent to the type of all finite types

map-compute-total-UU-Fin : {l : Level}  Σ  (UU-Fin l)  𝔽 l
pr1 (map-compute-total-UU-Fin (pair k (pair X e))) = X
pr2 (map-compute-total-UU-Fin (pair k (pair X e))) =
  is-finite-has-finite-cardinality (pair k e)

compute-total-UU-Fin : {l : Level}  Σ  (UU-Fin l)  𝔽 l
compute-total-UU-Fin =
  ( equiv-tot
    ( λ X 
      equiv-prop
        ( is-prop-has-finite-cardinality)
        ( is-prop-is-finite X)
        ( is-finite-has-finite-cardinality)
        ( has-finite-cardinality-is-finite))) ∘e
  ( equiv-left-swap-Σ)

Finite types are either inhabited or empty

is-inhabited-or-empty-is-finite :
  {l1 : Level} {A : UU l1}  is-finite A  is-inhabited-or-empty A
is-inhabited-or-empty-is-finite {l1} {A} f =
  apply-universal-property-trunc-Prop f
    ( is-inhabited-or-empty-Prop A)
    ( is-inhabited-or-empty-count)

Finite types of cardinality greater than one are inhabited

is-inhabited-type-UU-Fin-succ-ℕ :
  {l1 : Level} (n : ) (A : UU-Fin l1 (succ-ℕ n)) 
  is-inhabited (type-UU-Fin (succ-ℕ n) A)
is-inhabited-type-UU-Fin-succ-ℕ n A =
   apply-universal-property-trunc-Prop
    ( pr2 A)
    ( is-inhabited-Prop (type-UU-Fin (succ-ℕ n) A))
    ( λ e  unit-trunc-Prop (map-equiv e (zero-Fin n)))

If X is finite, then its propositional truncation is decidable

is-decidable-type-trunc-Prop-is-finite :
  {l1 : Level} {A : UU l1}  is-finite A  is-decidable (type-trunc-Prop A)
is-decidable-type-trunc-Prop-is-finite H =
  map-coprod
    ( id)
    ( map-universal-property-trunc-Prop empty-Prop)
      ( is-inhabited-or-empty-is-finite H)

If a type is finite, then its propositional truncation is finite

abstract
  is-finite-type-trunc-Prop :
    {l1 : Level} {A : UU l1}  is-finite A  is-finite (type-trunc-Prop A)
  is-finite-type-trunc-Prop = map-trunc-Prop count-type-trunc-Prop

trunc-Prop-𝔽 : {l : Level}  𝔽 l  𝔽 l
pr1 (trunc-Prop-𝔽 A) = type-trunc-Prop (type-𝔽 A)
pr2 (trunc-Prop-𝔽 A) = is-finite-type-trunc-Prop (is-finite-type-𝔽 A)

We characterize the identity type of 𝔽

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

id-equiv-𝔽 : {l : Level}  (X : 𝔽 l)  equiv-𝔽 X X
id-equiv-𝔽 X = id-equiv

extensionality-𝔽 : {l : Level}  (X Y : 𝔽 l)  Id X Y  equiv-𝔽 X Y
extensionality-𝔽 = extensionality-subuniverse is-finite-Prop

is-contr-total-equiv-𝔽 :
  {l : Level}  (X : 𝔽 l)  is-contr (Σ (𝔽 l) (equiv-𝔽 X))
is-contr-total-equiv-𝔽 {l} X =
  is-contr-equiv'
    ( Σ (𝔽 l) (Id X))
    ( equiv-tot (extensionality-𝔽 X))
    ( is-contr-total-path X)

equiv-eq-𝔽 : {l : Level}  (X Y : 𝔽 l)  Id X Y  equiv-𝔽 X Y
equiv-eq-𝔽 X Y = map-equiv (extensionality-𝔽 X Y)

eq-equiv-𝔽 : {l : Level}  (X Y : 𝔽 l)  equiv-𝔽 X Y  Id X Y
eq-equiv-𝔽 X Y = map-inv-equiv (extensionality-𝔽 X Y)

We characterize the identity type of families of finite types

equiv-fam-𝔽 : {l1 l2 : Level} {X : UU l1} (Y Z : X  𝔽 l2)  UU (l1  l2)
equiv-fam-𝔽 Y Z = equiv-fam (type-𝔽  Y) (type-𝔽  Z)

id-equiv-fam-𝔽 : {l1 l2 : Level} {X : UU l1}  (Y : X  𝔽 l2)  equiv-fam-𝔽 Y Y
id-equiv-fam-𝔽 Y x = id-equiv

extensionality-fam-𝔽 :
  {l1 l2 : Level} {X : UU l1} (Y Z : X  𝔽 l2)  Id Y Z  equiv-fam-𝔽 Y Z
extensionality-fam-𝔽 = extensionality-fam-subuniverse is-finite-Prop

We characterize the identity type of UU-Fin

equiv-UU-Fin :
  {l1 l2 : Level} (k : )  UU-Fin l1 k  UU-Fin l2 k  UU (l1  l2)
equiv-UU-Fin k X Y = type-UU-Fin k X  type-UU-Fin k Y

id-equiv-UU-Fin :
  {l : Level} {k : } (X : UU-Fin l k)  equiv-UU-Fin k X X
id-equiv-UU-Fin X = id-equiv-component-UU-Level X

equiv-eq-UU-Fin :
  {l : Level} (k : ) {X Y : UU-Fin l k}  Id X Y  equiv-UU-Fin k X Y
equiv-eq-UU-Fin k p = equiv-eq-component-UU-Level p

abstract
  is-contr-total-equiv-UU-Fin :
    {l : Level} {k : } (X : UU-Fin l k) 
    is-contr (Σ (UU-Fin l k) (equiv-UU-Fin k X))
  is-contr-total-equiv-UU-Fin {l} {k} X =
    is-contr-total-equiv-component-UU-Level X

abstract
  is-equiv-equiv-eq-UU-Fin :
    {l : Level} (k : ) (X Y : UU-Fin l k) 
    is-equiv (equiv-eq-UU-Fin k {X = X} {Y})
  is-equiv-equiv-eq-UU-Fin k X =
    is-equiv-equiv-eq-component-UU-Level X

eq-equiv-UU-Fin :
  {l : Level} (k : ) (X Y : UU-Fin l k) 
  equiv-UU-Fin k X Y  Id X Y
eq-equiv-UU-Fin k X Y =
  eq-equiv-component-UU-Level X Y

equiv-equiv-eq-UU-Fin :
  {l : Level} (k : ) (X Y : UU-Fin l k) 
  Id X Y  equiv-UU-Fin k X Y
pr1 (equiv-equiv-eq-UU-Fin k X Y) = equiv-eq-UU-Fin k
pr2 (equiv-equiv-eq-UU-Fin k X Y) = is-equiv-equiv-eq-UU-Fin k X Y

The type UU-Fin l k is a 1-type

is-1-type-UU-Fin : {l : Level} (k : )  is-1-type (UU-Fin l k)
is-1-type-UU-Fin k X Y =
  is-set-equiv
    ( equiv-UU-Fin k X Y)
    ( equiv-equiv-eq-UU-Fin k X Y)
    ( is-set-equiv-is-set
      ( is-set-type-UU-Fin k X)
      ( is-set-type-UU-Fin k Y))

UU-Fin-1-Type : (l : Level) (k : )  1-Type (lsuc l)
pr1 (UU-Fin-1-Type l k) = UU-Fin l k
pr2 (UU-Fin-1-Type l k) = is-1-type-UU-Fin k

The type UU-Fin is connected

abstract
  is-0-connected-UU-Fin :
    {l : Level} (n : )  is-0-connected (UU-Fin l n)
  is-0-connected-UU-Fin {l} n =
    is-0-connected-mere-eq
      ( Fin-UU-Fin l n)
      ( λ A 
        map-trunc-Prop
          ( ( eq-equiv-UU-Fin n (Fin-UU-Fin l n) A) 
            ( map-equiv
              ( equiv-precomp-equiv
                ( inv-equiv (compute-raise l (Fin n)))
                ( type-UU-Fin n A))))
          ( pr2 A))
  equiv-has-cardinality-id-number-of-elements-is-finite :
    {l : Level} (X : UU l) ( H : is-finite X) (n : ) 
    ( has-cardinality n X  Id (number-of-elements-is-finite H) n)
  pr1 (equiv-has-cardinality-id-number-of-elements-is-finite X H n) Q =
    ap
      ( number-of-elements-has-finite-cardinality)
      ( all-elements-equal-has-finite-cardinality
        ( has-finite-cardinality-is-finite H)
        ( pair n Q))
  pr2 (equiv-has-cardinality-id-number-of-elements-is-finite X H n) =
    is-equiv-is-prop
      ( is-prop-type-trunc-Prop)
      ( is-set-ℕ (number-of-elements-is-finite H) n)
      ( λ p 
        tr ( λ m  has-cardinality m X)
           ( p)
           ( pr2 (has-finite-cardinality-is-finite H)))