# Tetrahedra in 3-dimensional space

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

Created on 2022-07-02.

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