# Latin squares

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

Created on 2022-04-29.

module univalent-combinatorics.latin-squares where

Imports
open import foundation.binary-equivalences
open import foundation.dependent-pair-types
open import foundation.inhabited-types
open import foundation.universe-levels


## Idea

Latin squares are multiplication tables in which every element appears in every row and in every column exactly once. Latin squares are considered to be the same if they are isotopic. We therefore define the type of all Latin squares to be the type of all inhabited types A, B, and C, equipped with a binary equivalence f : A → B → C. The groupoid of main classes of latin squares is defined in main-classes-of-latin-squares.

## Definition

Latin-Square : (l1 l2 l3 : Level) → UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3)
Latin-Square l1 l2 l3 =
Σ ( Inhabited-Type l1)
( λ A →
Σ ( Inhabited-Type l2)
( λ B →
Σ ( Inhabited-Type l3)
( λ C →
Σ ( type-Inhabited-Type A → type-Inhabited-Type B →
type-Inhabited-Type C)
( is-binary-equiv))))

module _
{l1 l2 l3 : Level} (L : Latin-Square l1 l2 l3)
where

inhabited-type-row-Latin-Square : Inhabited-Type l1
inhabited-type-row-Latin-Square = pr1 L

row-Latin-Square : UU l1
row-Latin-Square = type-Inhabited-Type inhabited-type-row-Latin-Square

inhabited-type-column-Latin-Square : Inhabited-Type l2
inhabited-type-column-Latin-Square = pr1 (pr2 L)

column-Latin-Square : UU l2
column-Latin-Square = type-Inhabited-Type inhabited-type-column-Latin-Square

inhabited-type-symbol-Latin-Square : Inhabited-Type l3
inhabited-type-symbol-Latin-Square = pr1 (pr2 (pr2 L))

symbol-Latin-Square : UU l3
symbol-Latin-Square = type-Inhabited-Type inhabited-type-symbol-Latin-Square

mul-Latin-Square :
row-Latin-Square → column-Latin-Square → symbol-Latin-Square
mul-Latin-Square = pr1 (pr2 (pr2 (pr2 L)))

mul-Latin-Square' :
column-Latin-Square → row-Latin-Square → symbol-Latin-Square
mul-Latin-Square' x y = mul-Latin-Square y x

is-binary-equiv-mul-Latin-Square :
is-binary-equiv mul-Latin-Square
is-binary-equiv-mul-Latin-Square = pr2 (pr2 (pr2 (pr2 L)))