Latin squares

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)))