Partitions of finite types

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

Created on 2022-06-20.
Last modified on 2024-02-06.

module univalent-combinatorics.partitions where

Imports

open import elementary-number-theory.natural-numbers

open import foundation.binary-relations
open import foundation.cartesian-product-types
open import foundation.equality-cartesian-product-types
open import foundation.equivalence-extensionality
open import foundation.equivalence-relations
open import foundation.equivalences
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.sets
open import foundation.structure-identity-principle
open import foundation.type-arithmetic-cartesian-product-types
open import foundation.universe-levels

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

Idea

A partition of a finite type X can be defined in several equivalent ways:

A partition is a subset P of the powerset of X such that each U ⊆ X in P is inhabited and each element x : X is in exactly one subset U ⊆ X in P.
A partition is an equivalence relation on X
A partition is a decomposition of X into a type of the form Σ A B where A is finite and B is a family of inhabited finite types, i.e., it consists of such A and B and an equivalence X ≃ Σ A B.

Note that the last description is subtly different from the notion of unlabeled partition (i.e., Ferrers diagram), because it only uses mere equivalences.

Definition

Partitions

partition-𝔽 : {l1 : Level} (l2 l3 : Level) → 𝔽 l1 → UU (l1 ⊔ lsuc l2 ⊔ lsuc l3)
partition-𝔽 l2 l3 X =
  Σ ( 𝔽 l2)
    ( λ Y →
      Σ ( type-𝔽 Y → 𝔽 l3)
        ( λ Z →
          ( (y : type-𝔽 Y) → type-trunc-Prop (type-𝔽 (Z y))) ×
          ( equiv-𝔽 X (Σ-𝔽 Y Z))))

module _
  {l1 l2 l3 : Level} (X : 𝔽 l1) (P : partition-𝔽 l2 l3 X)
  where

  finite-indexing-type-partition-𝔽 : 𝔽 l2
  finite-indexing-type-partition-𝔽 = pr1 P

  indexing-type-partition-𝔽 : UU l2
  indexing-type-partition-𝔽 = type-𝔽 finite-indexing-type-partition-𝔽

  is-finite-indexing-type-partition-𝔽 : is-finite indexing-type-partition-𝔽
  is-finite-indexing-type-partition-𝔽 =
    is-finite-type-𝔽 finite-indexing-type-partition-𝔽

  number-of-elements-indexing-type-partition-𝔽 : ℕ
  number-of-elements-indexing-type-partition-𝔽 =
    number-of-elements-is-finite is-finite-indexing-type-partition-𝔽

  finite-block-partition-𝔽 : indexing-type-partition-𝔽 → 𝔽 l3
  finite-block-partition-𝔽 = pr1 (pr2 P)

  block-partition-𝔽 : indexing-type-partition-𝔽 → UU l3
  block-partition-𝔽 i = type-𝔽 (finite-block-partition-𝔽 i)

  is-finite-block-partition-𝔽 :
    (i : indexing-type-partition-𝔽) → is-finite (block-partition-𝔽 i)
  is-finite-block-partition-𝔽 i = is-finite-type-𝔽 (finite-block-partition-𝔽 i)

  number-of-elements-block-partition-𝔽 : indexing-type-partition-𝔽 → ℕ
  number-of-elements-block-partition-𝔽 i =
    number-of-elements-is-finite (is-finite-block-partition-𝔽 i)

  is-inhabited-block-partition-𝔽 :
    (i : indexing-type-partition-𝔽) → type-trunc-Prop (block-partition-𝔽 i)
  is-inhabited-block-partition-𝔽 = pr1 (pr2 (pr2 P))

  conversion-partition-𝔽 :
    equiv-𝔽 X (Σ-𝔽 finite-indexing-type-partition-𝔽 finite-block-partition-𝔽)
  conversion-partition-𝔽 = pr2 (pr2 (pr2 P))

  map-conversion-partition-𝔽 :
    type-𝔽 X → Σ indexing-type-partition-𝔽 block-partition-𝔽
  map-conversion-partition-𝔽 = map-equiv conversion-partition-𝔽

  rel-partition-𝔽-Prop : type-𝔽 X → type-𝔽 X → Prop l2
  rel-partition-𝔽-Prop x y =
    Id-Prop
      ( set-𝔽 finite-indexing-type-partition-𝔽)
      ( pr1 (map-conversion-partition-𝔽 x))
      ( pr1 (map-conversion-partition-𝔽 y))

  rel-partition-𝔽 : type-𝔽 X → type-𝔽 X → UU l2
  rel-partition-𝔽 x y = type-Prop (rel-partition-𝔽-Prop x y)

  is-prop-rel-partition-𝔽 : (x y : type-𝔽 X) → is-prop (rel-partition-𝔽 x y)
  is-prop-rel-partition-𝔽 x y = is-prop-type-Prop (rel-partition-𝔽-Prop x y)

  refl-rel-partition-𝔽 : is-reflexive rel-partition-𝔽
  refl-rel-partition-𝔽 x = refl

  symmetric-rel-partition-𝔽 : is-symmetric rel-partition-𝔽
  symmetric-rel-partition-𝔽 x y = inv

  transitive-rel-partition-𝔽 : is-transitive rel-partition-𝔽
  transitive-rel-partition-𝔽 x y z r s = s ∙ r

  equivalence-relation-partition-𝔽 : equivalence-relation l2 (type-𝔽 X)
  pr1 equivalence-relation-partition-𝔽 = rel-partition-𝔽-Prop
  pr1 (pr2 equivalence-relation-partition-𝔽) = refl-rel-partition-𝔽
  pr1 (pr2 (pr2 equivalence-relation-partition-𝔽)) = symmetric-rel-partition-𝔽
  pr2 (pr2 (pr2 equivalence-relation-partition-𝔽)) = transitive-rel-partition-𝔽