Decidable equivalence relations on finite types

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

Created on 2022-06-23.

module univalent-combinatorics.decidable-equivalence-relations where

Imports
open import elementary-number-theory.natural-numbers

open import foundation.binary-relations
open import foundation.cartesian-product-types
open import foundation.decidable-equality
open import foundation.decidable-equivalence-relations
open import foundation.decidable-relations
open import foundation.decidable-types
open import foundation.equivalence-relations
open import foundation.equivalences
open import foundation.function-types
open import foundation.functoriality-cartesian-product-types
open import foundation.functoriality-dependent-pair-types
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.type-arithmetic-cartesian-product-types
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

open import univalent-combinatorics.cartesian-product-types
open import univalent-combinatorics.counting
open import univalent-combinatorics.decidable-propositions
open import univalent-combinatorics.dependent-function-types
open import univalent-combinatorics.dependent-pair-types
open import univalent-combinatorics.finite-types
open import univalent-combinatorics.function-types
open import univalent-combinatorics.standard-finite-types
open import univalent-combinatorics.surjective-maps


Idea

A decidable equivalence relation on a finite type is an equivalence relation R such that each R x y is a decidable proposition.

Definition

Decidable-equivalence-relation-𝔽 :
{l1 : Level} (l2 : Level) (X : 𝔽 l1) → UU (l1 ⊔ lsuc l2)
Decidable-equivalence-relation-𝔽 l2 X =
Decidable-equivalence-relation l2 (type-𝔽 X)

module _
{l1 l2 : Level} (X : 𝔽 l1) (R : Decidable-equivalence-relation-𝔽 l2 X)
where

decidable-relation-Decidable-equivalence-relation-𝔽 :
Decidable-Relation l2 (type-𝔽 X)
decidable-relation-Decidable-equivalence-relation-𝔽 =
decidable-relation-Decidable-equivalence-relation R

relation-Decidable-equivalence-relation-𝔽 :
type-𝔽 X → type-𝔽 X → Prop l2
relation-Decidable-equivalence-relation-𝔽 =
relation-Decidable-equivalence-relation R

sim-Decidable-equivalence-relation-𝔽 : type-𝔽 X → type-𝔽 X → UU l2
sim-Decidable-equivalence-relation-𝔽 =
sim-Decidable-equivalence-relation R

is-prop-sim-Decidable-equivalence-relation-𝔽 :
(x y : type-𝔽 X) → is-prop (sim-Decidable-equivalence-relation-𝔽 x y)
is-prop-sim-Decidable-equivalence-relation-𝔽 =
is-prop-sim-Decidable-equivalence-relation R

is-decidable-sim-Decidable-equivalence-relation-𝔽 :
(x y : type-𝔽 X) → is-decidable (sim-Decidable-equivalence-relation-𝔽 x y)
is-decidable-sim-Decidable-equivalence-relation-𝔽 =
is-decidable-sim-Decidable-equivalence-relation R

is-equivalence-relation-Decidable-equivalence-relation-𝔽 :
is-equivalence-relation relation-Decidable-equivalence-relation-𝔽
is-equivalence-relation-Decidable-equivalence-relation-𝔽 =
is-equivalence-relation-Decidable-equivalence-relation R

equivalence-relation-Decidable-equivalence-relation-𝔽 :
equivalence-relation l2 (type-𝔽 X)
equivalence-relation-Decidable-equivalence-relation-𝔽 =
equivalence-relation-Decidable-equivalence-relation R

refl-Decidable-equivalence-relation-𝔽 :
is-reflexive sim-Decidable-equivalence-relation-𝔽
refl-Decidable-equivalence-relation-𝔽 =
refl-Decidable-equivalence-relation R

symmetric-Decidable-equivalence-relation-𝔽 :
is-symmetric sim-Decidable-equivalence-relation-𝔽
symmetric-Decidable-equivalence-relation-𝔽 =
symmetric-Decidable-equivalence-relation R

transitive-Decidable-equivalence-relation-𝔽 :
is-transitive sim-Decidable-equivalence-relation-𝔽
transitive-Decidable-equivalence-relation-𝔽 =
transitive-Decidable-equivalence-relation R

module _
{l1 l2 : Level} (A : 𝔽 l1) (R : Decidable-Relation l2 (type-𝔽 A))
where

is-finite-relation-Decidable-Relation-𝔽 :
(x : type-𝔽 A) → (y : type-𝔽 A) → is-finite (rel-Decidable-Relation R x y)
is-finite-relation-Decidable-Relation-𝔽 x y =
unit-trunc-Prop
( count-Decidable-Prop
( relation-Decidable-Relation R x y)
( is-decidable-Decidable-Relation R x y))

is-finite-is-reflexive-Dec-Relation-Prop-𝔽 :
is-finite (is-reflexive-Relation-Prop (relation-Decidable-Relation R))
is-finite-is-reflexive-Dec-Relation-Prop-𝔽 =
is-finite-Π
( is-finite-type-𝔽 A)
(λ x → is-finite-relation-Decidable-Relation-𝔽 x x)

is-finite-is-symmetric-Dec-Relation-Prop-𝔽 :
is-finite (is-symmetric-Relation-Prop (relation-Decidable-Relation R))
is-finite-is-symmetric-Dec-Relation-Prop-𝔽 =
is-finite-Π
( is-finite-type-𝔽 A)
( λ x →
is-finite-Π
( is-finite-type-𝔽 A)
( λ y →
is-finite-function-type
( is-finite-relation-Decidable-Relation-𝔽 x y)
( is-finite-relation-Decidable-Relation-𝔽 y x)))

is-finite-is-transitive-Dec-Relation-Prop-𝔽 :
is-finite (is-transitive-Relation-Prop (relation-Decidable-Relation R))
is-finite-is-transitive-Dec-Relation-Prop-𝔽 =
is-finite-Π
( is-finite-type-𝔽 A)
( λ x →
is-finite-Π
( is-finite-type-𝔽 A)
( λ y →
is-finite-Π
( is-finite-type-𝔽 A)
( λ z →
is-finite-function-type
( is-finite-relation-Decidable-Relation-𝔽 y z)
( is-finite-function-type
( is-finite-relation-Decidable-Relation-𝔽 x y)
( is-finite-relation-Decidable-Relation-𝔽 x z)))))

is-finite-is-equivalence-Dec-Relation-Prop-𝔽 :
is-finite (is-equivalence-relation (relation-Decidable-Relation R))
is-finite-is-equivalence-Dec-Relation-Prop-𝔽 =
is-finite-product
( is-finite-is-reflexive-Dec-Relation-Prop-𝔽)
( is-finite-product
is-finite-is-symmetric-Dec-Relation-Prop-𝔽
is-finite-is-transitive-Dec-Relation-Prop-𝔽)


Properties

The type of decidable equivalence relations on A is equivalent to the type of surjections from A into a finite type

equiv-Surjection-𝔽-Decidable-equivalence-relation-𝔽 :
{l1 : Level} (A : 𝔽 l1) →
Decidable-equivalence-relation-𝔽 l1 A ≃
Surjection-𝔽 l1 A
equiv-Surjection-𝔽-Decidable-equivalence-relation-𝔽 {l1} A =
( equiv-Σ-equiv-base
( λ X → (type-𝔽 A) ↠ (type-𝔽 X))
( equiv-Σ
( is-finite)
( id-equiv)
( λ X →
inv-equiv is-finite-iff-∃-surjection-has-decidable-equality)) ∘e
( ( inv-associative-Σ
( UU l1)
( λ X →
has-decidable-equality X ×
type-trunc-Prop (Σ ℕ (λ n → Fin n ↠ X)))
( λ X → type-𝔽 A ↠ pr1 X)) ∘e
( ( equiv-Σ
(λ X →
Σ ( has-decidable-equality X ×
type-trunc-Prop (Σ ℕ (λ n → Fin n ↠ X)))
( λ _ → pr1 A ↠ X))
( id-equiv)
( λ X →
( ( inv-equiv
( associative-product
( has-decidable-equality X)
( type-trunc-Prop (Σ ℕ (λ n → Fin n ↠ X)))
( type-𝔽 A ↠ X))) ∘e
( ( equiv-product id-equiv commutative-product) ∘e
( ( associative-product
( has-decidable-equality (map-equiv id-equiv X))
( type-𝔽 A ↠ X)
( type-trunc-Prop (Σ ℕ (λ n → Fin n ↠ X)))) ∘e
( ( equiv-product commutative-product id-equiv) ∘e
( is-prop-type-trunc-Prop)
( λ x →
apply-universal-property-trunc-Prop
( is-finite-type-𝔽 A)
( trunc-Prop ( Σ ℕ (λ n → Fin n ↠ X)))
( λ count-A →
unit-trunc-Prop
( number-of-elements-count count-A ,
( ( map-surjection (pr1 x) ∘
map-equiv-count count-A) ,
is-surjective-precomp-equiv
( is-surjective-map-surjection (pr1 x))
( equiv-count count-A)))))))))))) ∘e
( equiv-Surjection-Into-Set-Decidable-equivalence-relation
( type-𝔽 A))))))


The type of decidable equivalence relations on a finite type is finite

is-finite-Decidable-Relation-𝔽 :
{l1 : Level} (A : 𝔽 l1) →
is-finite (Decidable-Relation l1 (type-𝔽 A))
is-finite-Decidable-Relation-𝔽 A =
is-finite-Π
( is-finite-type-𝔽 A)
( λ a →
is-finite-Π
( is-finite-type-𝔽 A)
( λ b → is-finite-Decidable-Prop))

is-finite-Decidable-equivalence-relation-𝔽 :
{l1 : Level} (A : 𝔽 l1) →
is-finite (Decidable-equivalence-relation-𝔽 l1 A)
is-finite-Decidable-equivalence-relation-𝔽 A =
is-finite-Σ
( is-finite-Decidable-Relation-𝔽 A)
( is-finite-is-equivalence-Dec-Relation-Prop-𝔽 A)


The number of decidable equivalence relations on a finite type is a Stirling number of the second kind

This remains to be characterized. #745