# The groupoid of main classes of Latin squares

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

Created on 2022-05-01.

module univalent-combinatorics.main-classes-of-latin-squares where

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

open import foundation.mere-equivalences
open import foundation.set-truncations
open import foundation.universe-levels

open import univalent-combinatorics.main-classes-of-latin-hypercubes
open import univalent-combinatorics.pi-finite-types
open import univalent-combinatorics.standard-finite-types


## Idea

The groupoid of main classes of latin squares consists of unordered triples of inhabited types equipped with a ternary 1-1 correspondence.

## Definition

### Main classes of general latin squares

Main-Class-Latin-Squares : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
Main-Class-Latin-Squares l1 l2 = Main-Class-Latin-Hypercube l1 l2 2


### Main classes of latin squares of fixed finite order

Main-Class-Latin-Square-of-Order : (m : ℕ) → UU (lsuc lzero)
Main-Class-Latin-Square-of-Order m =
Main-Class-Latin-Hypercube-of-Order 2 m


## Properties

### The groupoid of main classes of latin squares of fixed order is π-finite

is-π-finite-Main-Class-Latin-Square-of-Order :
(k m : ℕ) → is-π-finite k (Main-Class-Latin-Square-of-Order m)
is-π-finite-Main-Class-Latin-Square-of-Order k m =
is-π-finite-Main-Class-Latin-Hypercube-of-Order k 2 m


### The sequence of the number of main classes of latin squares of finite order

The following sequence defines A003090 in the OEIS.

number-of-main-classes-of-Latin-squares-of-order : ℕ → ℕ
number-of-main-classes-of-Latin-squares-of-order =
number-of-main-classes-of-Latin-hypercubes-of-order 2

mere-equiv-number-of-main-classes-of-Latin-squares-of-order :
(m : ℕ) →
mere-equiv
( Fin (number-of-main-classes-of-Latin-squares-of-order m))
( type-trunc-Set (Main-Class-Latin-Square-of-Order m))
mere-equiv-number-of-main-classes-of-Latin-squares-of-order =
mere-equiv-number-of-main-classes-of-Latin-hypercubes-of-order 2