# Ferrers diagrams (unlabeled partitions)

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

Created on 2022-04-26.

module univalent-combinatorics.ferrers-diagrams where

Imports
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.equality-dependent-function-types
open import foundation.equivalences
open import foundation.fundamental-theorem-of-identity-types
open import foundation.identity-types
open import foundation.mere-equivalences
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.structure-identity-principle
open import foundation.subtype-identity-principle
open import foundation.torsorial-type-families
open import foundation.univalence
open import foundation.universe-levels

open import univalent-combinatorics.finite-types


## Idea

Unlabeled partitions, also known as Ferrers diagrams, of a type A record the number of ways in which A can be decomposed as the dependent pair type of a family of inhabited types. More precisely, a Ferrers diagram of a type A consists of a type X and a family Y of inhabited types over X such that Σ X Y is merely equivalent to A. A finite Finite ferrers diagram of a finite type A consists of a finite type X and a family Y of inhabited finite types over X such that Σ X Y is merely equivalent to A. The number of finite Ferrers diagrams of A is the partition number of the cardinality of A.

## Definition

### Ferrers diagrams of arbitrary types

ferrers-diagram :
{l1 : Level} (l2 l3 : Level) (A : UU l1) → UU (l1 ⊔ lsuc l2 ⊔ lsuc l3)
ferrers-diagram l2 l3 A =
Σ ( UU l2)
( λ X →
Σ ( X → UU l3)
( λ Y →
((x : X) → type-trunc-Prop (Y x)) × mere-equiv A (Σ X Y)))

module _
{l1 l2 l3 : Level} {A : UU l1} (D : ferrers-diagram l2 l3 A)
where

row-ferrers-diagram : UU l2
row-ferrers-diagram = pr1 D

dot-ferrers-diagram : row-ferrers-diagram → UU l3
dot-ferrers-diagram = pr1 (pr2 D)

is-inhabited-dot-ferrers-diagram :
(x : row-ferrers-diagram) → type-trunc-Prop (dot-ferrers-diagram x)
is-inhabited-dot-ferrers-diagram = pr1 (pr2 (pr2 D))

mere-equiv-ferrers-diagram :
mere-equiv A (Σ row-ferrers-diagram dot-ferrers-diagram)
mere-equiv-ferrers-diagram = pr2 (pr2 (pr2 D))


### Finite Ferrers diagrams of finite types

ferrers-diagram-𝔽 :
{l1 : Level} (l2 l3 : Level) (A : 𝔽 l1) → UU (l1 ⊔ lsuc l2 ⊔ lsuc l3)
ferrers-diagram-𝔽 {l} l2 l3 A =
Σ ( 𝔽 l2)
( λ X →
Σ ( type-𝔽 X → 𝔽 l3)
( λ Y →
((x : type-𝔽 X) → type-trunc-Prop (type-𝔽 (Y x))) ×
mere-equiv (type-𝔽 A) (Σ (type-𝔽 X) (λ x → type-𝔽 (Y x)))))

module _
{l1 l2 l3 : Level} (A : 𝔽 l1) (D : ferrers-diagram-𝔽 l2 l3 A)
where

row-ferrers-diagram-𝔽 : 𝔽 l2
row-ferrers-diagram-𝔽 = pr1 D

type-row-ferrers-diagram-𝔽 : UU l2
type-row-ferrers-diagram-𝔽 = type-𝔽 row-ferrers-diagram-𝔽

is-finite-type-row-ferrers-diagram-𝔽 : is-finite type-row-ferrers-diagram-𝔽
is-finite-type-row-ferrers-diagram-𝔽 =
is-finite-type-𝔽 row-ferrers-diagram-𝔽

dot-ferrers-diagram-𝔽 : type-row-ferrers-diagram-𝔽 → 𝔽 l3
dot-ferrers-diagram-𝔽 = pr1 (pr2 D)

type-dot-ferrers-diagram-𝔽 : type-row-ferrers-diagram-𝔽 → UU l3
type-dot-ferrers-diagram-𝔽 x = type-𝔽 (dot-ferrers-diagram-𝔽 x)

is-finite-type-dot-ferrers-diagram-𝔽 :
(x : type-row-ferrers-diagram-𝔽) → is-finite (type-dot-ferrers-diagram-𝔽 x)
is-finite-type-dot-ferrers-diagram-𝔽 x =
is-finite-type-𝔽 (dot-ferrers-diagram-𝔽 x)

is-inhabited-dot-ferrers-diagram-𝔽 :
(x : type-row-ferrers-diagram-𝔽) →
type-trunc-Prop (type-dot-ferrers-diagram-𝔽 x)
is-inhabited-dot-ferrers-diagram-𝔽 = pr1 (pr2 (pr2 D))

mere-equiv-ferrers-diagram-𝔽 :
mere-equiv
( type-𝔽 A)
( Σ (type-row-ferrers-diagram-𝔽) (type-dot-ferrers-diagram-𝔽))
mere-equiv-ferrers-diagram-𝔽 = pr2 (pr2 (pr2 D))

ferrers-diagram-ferrers-diagram-𝔽 : ferrers-diagram l2 l3 (type-𝔽 A)
pr1 ferrers-diagram-ferrers-diagram-𝔽 = type-row-ferrers-diagram-𝔽
pr1 (pr2 ferrers-diagram-ferrers-diagram-𝔽) = type-dot-ferrers-diagram-𝔽
pr1 (pr2 (pr2 ferrers-diagram-ferrers-diagram-𝔽)) =
is-inhabited-dot-ferrers-diagram-𝔽
pr2 (pr2 (pr2 ferrers-diagram-ferrers-diagram-𝔽)) =
mere-equiv-ferrers-diagram-𝔽


### Equivalences of Ferrers diagrams

module _
{l1 l2 l3 : Level} {A : UU l1} (D : ferrers-diagram l2 l3 A)
where

equiv-ferrers-diagram :
{l4 l5 : Level} (E : ferrers-diagram l4 l5 A) → UU (l2 ⊔ l3 ⊔ l4 ⊔ l5)
equiv-ferrers-diagram E =
Σ ( row-ferrers-diagram D ≃ row-ferrers-diagram E)
( λ e →
(x : row-ferrers-diagram D) →
dot-ferrers-diagram D x ≃ dot-ferrers-diagram E (map-equiv e x))

id-equiv-ferrers-diagram : equiv-ferrers-diagram D
pr1 id-equiv-ferrers-diagram = id-equiv
pr2 id-equiv-ferrers-diagram x = id-equiv

equiv-eq-ferrers-diagram :
(E : ferrers-diagram l2 l3 A) → Id D E → equiv-ferrers-diagram E
equiv-eq-ferrers-diagram .D refl = id-equiv-ferrers-diagram

is-torsorial-equiv-ferrers-diagram :
is-torsorial equiv-ferrers-diagram
is-torsorial-equiv-ferrers-diagram =
is-torsorial-Eq-structure
( is-torsorial-equiv (row-ferrers-diagram D))
( pair (row-ferrers-diagram D) id-equiv)
( is-torsorial-Eq-subtype
( is-torsorial-equiv-fam (dot-ferrers-diagram D))
( λ Y →
is-prop-product
( is-prop-Π (λ x → is-prop-type-trunc-Prop))
( is-prop-mere-equiv A (Σ (row-ferrers-diagram D) Y)))
( dot-ferrers-diagram D)
( λ x → id-equiv)
( pair
( is-inhabited-dot-ferrers-diagram D)
( mere-equiv-ferrers-diagram D)))

is-equiv-equiv-eq-ferrers-diagram :
(E : ferrers-diagram l2 l3 A) → is-equiv (equiv-eq-ferrers-diagram E)
is-equiv-equiv-eq-ferrers-diagram =
fundamental-theorem-id
is-torsorial-equiv-ferrers-diagram
equiv-eq-ferrers-diagram

eq-equiv-ferrers-diagram :
(E : ferrers-diagram l2 l3 A) → equiv-ferrers-diagram E → Id D E
eq-equiv-ferrers-diagram E =
map-inv-is-equiv (is-equiv-equiv-eq-ferrers-diagram E)


### Equivalences of finite ferrers diagrams of finite types

module _
{l1 l2 l3 : Level} (A : 𝔽 l1) (D : ferrers-diagram-𝔽 l2 l3 A)
where

equiv-ferrers-diagram-𝔽 :
{l4 l5 : Level} → ferrers-diagram-𝔽 l4 l5 A → UU (l2 ⊔ l3 ⊔ l4 ⊔ l5)
equiv-ferrers-diagram-𝔽 E =
equiv-ferrers-diagram
( ferrers-diagram-ferrers-diagram-𝔽 A D)
( ferrers-diagram-ferrers-diagram-𝔽 A E)

id-equiv-ferrers-diagram-𝔽 : equiv-ferrers-diagram-𝔽 D
id-equiv-ferrers-diagram-𝔽 =
id-equiv-ferrers-diagram (ferrers-diagram-ferrers-diagram-𝔽 A D)

equiv-eq-ferrers-diagram-𝔽 :
(E : ferrers-diagram-𝔽 l2 l3 A) → Id D E → equiv-ferrers-diagram-𝔽 E
equiv-eq-ferrers-diagram-𝔽 .D refl = id-equiv-ferrers-diagram-𝔽

is-torsorial-equiv-ferrers-diagram-𝔽 :
is-torsorial equiv-ferrers-diagram-𝔽
is-torsorial-equiv-ferrers-diagram-𝔽 =
is-torsorial-Eq-structure
( is-torsorial-Eq-subtype
( is-torsorial-equiv (type-row-ferrers-diagram-𝔽 A D))
( is-prop-is-finite)
( type-row-ferrers-diagram-𝔽 A D)
( id-equiv)
( is-finite-type-row-ferrers-diagram-𝔽 A D))
( pair (row-ferrers-diagram-𝔽 A D) id-equiv)
( is-torsorial-Eq-subtype
( is-torsorial-Eq-Π
( λ x →
is-torsorial-Eq-subtype
( is-torsorial-equiv (type-dot-ferrers-diagram-𝔽 A D x))
( is-prop-is-finite)
( type-dot-ferrers-diagram-𝔽 A D x)
( id-equiv)
( is-finite-type-dot-ferrers-diagram-𝔽 A D x)))
( λ x →
is-prop-product
( is-prop-Π (λ x → is-prop-type-trunc-Prop))
( is-prop-mere-equiv (type-𝔽 A) _))
( dot-ferrers-diagram-𝔽 A D)
( λ x → id-equiv)
( pair
( is-inhabited-dot-ferrers-diagram-𝔽 A D)
( mere-equiv-ferrers-diagram-𝔽 A D)))

is-equiv-equiv-eq-ferrers-diagram-𝔽 :
(E : ferrers-diagram-𝔽 l2 l3 A) → is-equiv (equiv-eq-ferrers-diagram-𝔽 E)
is-equiv-equiv-eq-ferrers-diagram-𝔽 =
fundamental-theorem-id
is-torsorial-equiv-ferrers-diagram-𝔽
equiv-eq-ferrers-diagram-𝔽

eq-equiv-ferrers-diagram-𝔽 :
(E : ferrers-diagram-𝔽 l2 l3 A) → equiv-ferrers-diagram-𝔽 E → Id D E
eq-equiv-ferrers-diagram-𝔽 E =
map-inv-is-equiv (is-equiv-equiv-eq-ferrers-diagram-𝔽 E)


## Properties

### The type of Ferrers diagrams of any finite type is π-finite

This remains to be shown. #746