Tetrahedra in 3-dimensional space

module finite-group-theory.tetrahedra-in-3-space where

Imports

open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.universe-levels

open import univalent-combinatorics.2-element-decidable-subtypes
open import univalent-combinatorics.cyclic-types
open import univalent-combinatorics.finite-types

Idea

The type of tetrahedra in 3-dimensional space is a type of tetrahedra that can be rotated, but not reflected. In other words, the symmetry group of the tetrahedra in 3-dimensional space is the alternating group A₄.

Note that any rotation of a tetrahedron in 3-space induces a rotation on the set of opposing pairs of edges. There are three such pairs of edges.

Definition

tetrahedron-in-3-space : UU (lsuc lzero)
tetrahedron-in-3-space =
  Σ ( UU-Fin lzero 4)
    ( λ X →
      cyclic-structure 3
        ( Σ ( 2-Element-Decidable-Subtype lzero
              ( 2-Element-Decidable-Subtype lzero
                ( type-UU-Fin 4 X)))
            ( λ Q →
              (x : type-UU-Fin 4 X) →
              is-empty
                ( (P : type-2-Element-Decidable-Subtype Q) →
                  is-in-2-Element-Decidable-Subtype
                    (pr1 P)
                    ( x)))))

module _
  (T : tetrahedron-in-3-space)
  where

  vertex-tetrahedron-in-3-space : UU lzero
  vertex-tetrahedron-in-3-space = type-UU-Fin 4 (pr1 T)

  cyclic-structure-tetrahedron-in-3-space :
    cyclic-structure 3
      ( Σ ( 2-Element-Decidable-Subtype lzero
            ( 2-Element-Decidable-Subtype lzero
              ( vertex-tetrahedron-in-3-space)))
          ( λ Q →
            (x : vertex-tetrahedron-in-3-space) →
            is-empty
              ( (P : type-2-Element-Decidable-Subtype Q) →
                is-in-2-Element-Decidable-Subtype
                  (pr1 P)
                  ( x))))
  cyclic-structure-tetrahedron-in-3-space = pr2 T