# The concrete quaternion group

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

Created on 2022-03-12.

module finite-group-theory.concrete-quaternion-group where

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

open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.isolated-points
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import univalent-combinatorics.complements-isolated-points
open import univalent-combinatorics.cubes
open import univalent-combinatorics.equality-finite-types
open import univalent-combinatorics.equivalences-cubes


## Definition

equiv-face-cube :
(k : ℕ) (X Y : cube (succ-ℕ k)) (e : equiv-cube (succ-ℕ k) X Y)
(d : dim-cube (succ-ℕ k) X) (a : axis-cube (succ-ℕ k) X d) →
equiv-cube k
( face-cube k X d a)
( face-cube k Y
( map-dim-equiv-cube (succ-ℕ k) X Y e d)
( map-axis-equiv-cube (succ-ℕ k) X Y e d a))
equiv-face-cube k X Y e d a =
pair
( equiv-complement-point-UU-Fin k
( pair (dim-cube-UU-Fin (succ-ℕ k) X) d)
( pair
( dim-cube-UU-Fin (succ-ℕ k) Y)
( map-dim-equiv-cube (succ-ℕ k) X Y e d))
( dim-equiv-cube (succ-ℕ k) X Y e)
( refl))
( λ d' →
( equiv-tr
( axis-cube (succ-ℕ k) Y)
( inv
( natural-inclusion-equiv-complement-isolated-point
( dim-equiv-cube (succ-ℕ k) X Y e)
( pair d
( λ z →
has-decidable-equality-has-cardinality
( succ-ℕ k)
( has-cardinality-dim-cube (succ-ℕ k) X)
( d)
( z)))
( pair
( map-dim-equiv-cube (succ-ℕ k) X Y e d)
( λ z →
has-decidable-equality-has-cardinality
( succ-ℕ k)
( has-cardinality-dim-cube (succ-ℕ k) Y)
( map-dim-equiv-cube (succ-ℕ k) X Y e d)
( z)))
( refl)
( d')))) ∘e
( axis-equiv-cube (succ-ℕ k) X Y e
( inclusion-complement-point-UU-Fin k
( pair (dim-cube-UU-Fin (succ-ℕ k) X) d) d')))

cube-with-labeled-faces :
(k : ℕ) → UU (lsuc lzero)
cube-with-labeled-faces k =
Σ ( cube (succ-ℕ k))
( λ X →
(d : dim-cube (succ-ℕ k) X) (a : axis-cube (succ-ℕ k) X d) →
labelling-cube k (face-cube k X d a))

cube-cube-with-labeled-faces :
(k : ℕ) → cube-with-labeled-faces k → cube (succ-ℕ k)
cube-cube-with-labeled-faces k X = pr1 X

labelling-faces-cube-with-labeled-faces :
(k : ℕ) (X : cube-with-labeled-faces k)
(d : dim-cube (succ-ℕ k) (cube-cube-with-labeled-faces k X))
(a : axis-cube (succ-ℕ k) (cube-cube-with-labeled-faces k X) d) →
labelling-cube k (face-cube k (cube-cube-with-labeled-faces k X) d a)
labelling-faces-cube-with-labeled-faces k X = pr2 X

equiv-cube-with-labeled-faces :
{k : ℕ} (X Y : cube-with-labeled-faces k) → UU lzero
equiv-cube-with-labeled-faces {k} X Y =
Σ ( equiv-cube (succ-ℕ k)
( cube-cube-with-labeled-faces k X)
( cube-cube-with-labeled-faces k Y))
( λ e → ( d : dim-cube (succ-ℕ k) (cube-cube-with-labeled-faces k X))
( a : axis-cube (succ-ℕ k) (cube-cube-with-labeled-faces k X) d) →
htpy-equiv-cube k
( standard-cube k)
( face-cube k
( cube-cube-with-labeled-faces k Y)
( map-dim-equiv-cube (succ-ℕ k)
( cube-cube-with-labeled-faces k X)
( cube-cube-with-labeled-faces k Y)
( e)
( d))
( map-axis-equiv-cube (succ-ℕ k)
( cube-cube-with-labeled-faces k X)
( cube-cube-with-labeled-faces k Y)
e d a))
( comp-equiv-cube k
( standard-cube k)
( face-cube k (pr1 X) d a)
( face-cube k (pr1 Y)
( map-dim-equiv-cube (succ-ℕ k) (pr1 X) (pr1 Y) e d)
( map-axis-equiv-cube (succ-ℕ k) (pr1 X) (pr1 Y) e d a))
( equiv-face-cube k (pr1 X) (pr1 Y) e d a)
( labelling-faces-cube-with-labeled-faces k X d a))
( labelling-faces-cube-with-labeled-faces k Y
( map-dim-equiv-cube (succ-ℕ k)
( cube-cube-with-labeled-faces k X)
( cube-cube-with-labeled-faces k Y)
e d)
( map-axis-equiv-cube (succ-ℕ k)
( cube-cube-with-labeled-faces k X)
( cube-cube-with-labeled-faces k Y)
e d a)))