Equality in finite types

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Victor Blanchi.

Created on 2022-02-13.
Last modified on 2023-05-25.

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

open import foundation.decidable-equality
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.universe-levels

open import univalent-combinatorics.counting
open import univalent-combinatorics.decidable-propositions
open import univalent-combinatorics.equality-standard-finite-types
open import univalent-combinatorics.finite-types

Idea

Any finite type is a set because it is merely equivalent to a standard finite type. Moreover, any finite type has decidable equality. In particular, this implies that the type of identifications between any two elements in a finite type is finite.

Properties

Any finite type has decidable equality

has-decidable-equality-is-finite :
  {l1 : Level} {X : UU l1} → is-finite X → has-decidable-equality X
has-decidable-equality-is-finite {l1} {X} is-finite-X =
  apply-universal-property-trunc-Prop is-finite-X
    ( has-decidable-equality-Prop X)
    ( λ e →
      has-decidable-equality-equiv'
        ( equiv-count e)
        ( has-decidable-equality-Fin (number-of-elements-count e)))

Any type of finite cardinality has decidable equality

has-decidable-equality-has-cardinality :
  {l1 : Level} {X : UU l1} (k : ℕ) →
  has-cardinality k X → has-decidable-equality X
has-decidable-equality-has-cardinality {l1} {X} k H =
  apply-universal-property-trunc-Prop H
    ( has-decidable-equality-Prop X)
    ( λ e → has-decidable-equality-equiv' e (has-decidable-equality-Fin k))

The type of identifications between any two elements in a finite type is finite

abstract
  is-finite-eq :
    {l1 : Level} {X : UU l1} →
    has-decidable-equality X → {x y : X} → is-finite (Id x y)
  is-finite-eq d {x} {y} = is-finite-count (count-eq d x y)

is-finite-eq-𝔽 :
  {l : Level} → (X : 𝔽 l) {x y : type-𝔽 X} → is-finite (x ＝ y)
is-finite-eq-𝔽 X =
  is-finite-eq (has-decidable-equality-is-finite (is-finite-type-𝔽 X))

Id-𝔽 : {l : Level} → (X : 𝔽 l) (x y : type-𝔽 X) → 𝔽 l
pr1 (Id-𝔽 X x y) = Id x y
pr2 (Id-𝔽 X x y) = is-finite-eq-𝔽 X

Recent changes