Cubes

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

Created on 2022-03-20.

module univalent-combinatorics.cubes where

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

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

open import univalent-combinatorics.complements-isolated-elements
open import univalent-combinatorics.finite-types


Definitions

Cubes

cube : ℕ → UU (lsuc lzero)
cube k = Σ (UU-Fin lzero k) (λ X → type-UU-Fin k X → UU-Fin lzero 2)

module _
(k : ℕ) (X : cube k)
where

dim-cube-UU-Fin : UU-Fin lzero k
dim-cube-UU-Fin = pr1 X

dim-cube : UU lzero
dim-cube = type-UU-Fin k dim-cube-UU-Fin

has-cardinality-dim-cube : has-cardinality k dim-cube
has-cardinality-dim-cube = pr2 dim-cube-UU-Fin

has-finite-cardinality-dim-cube : has-finite-cardinality dim-cube
has-finite-cardinality-dim-cube =
pair k (pr2 dim-cube-UU-Fin)

is-finite-dim-cube : is-finite dim-cube
is-finite-dim-cube =
is-finite-has-finite-cardinality has-finite-cardinality-dim-cube

axis-cube-UU-2 : dim-cube → UU-Fin lzero 2
axis-cube-UU-2 = pr2 X

axis-cube : dim-cube → UU lzero
axis-cube d = type-UU-Fin 2 (axis-cube-UU-2 d)

has-cardinality-axis-cube : (d : dim-cube) → has-cardinality 2 (axis-cube d)
has-cardinality-axis-cube d = pr2 (axis-cube-UU-2 d)

has-finite-cardinality-axis-cube :
(d : dim-cube) → has-finite-cardinality (axis-cube d)
has-finite-cardinality-axis-cube d =
pair 2 (has-cardinality-axis-cube d)

is-finite-axis-cube : (d : dim-cube) → is-finite (axis-cube d)
is-finite-axis-cube d =
is-finite-has-cardinality 2 (has-cardinality-axis-cube d)

vertex-cube : UU lzero
vertex-cube = (d : dim-cube) → axis-cube d


The standard cube

dim-standard-cube-UU-Fin : (k : ℕ) → UU-Fin lzero k
dim-standard-cube-UU-Fin k = Fin-UU-Fin' k

dim-standard-cube : ℕ → UU lzero
dim-standard-cube k = type-UU-Fin k (dim-standard-cube-UU-Fin k)

axis-standard-cube-UU-Fin : (k : ℕ) → dim-standard-cube k → UU-Fin lzero 2
axis-standard-cube-UU-Fin k d = Fin-UU-Fin' 2

axis-standard-cube : (k : ℕ) → dim-standard-cube k → UU lzero
axis-standard-cube k d = type-UU-Fin 2 (axis-standard-cube-UU-Fin k d)

standard-cube : (k : ℕ) → cube k
standard-cube k =
pair (dim-standard-cube-UU-Fin k) (axis-standard-cube-UU-Fin k)

{-
mere-equiv-standard-cube :
{k : ℕ} (X : cube k) → type-trunc-Prop (equiv-cube (standard-cube k) X)
mere-equiv-standard-cube {k} (pair (pair X H) Y) =
apply-universal-property-trunc-Prop H
( trunc-Prop (equiv-cube (standard-cube k) (pair (pair X H) Y)))
( λ e →
{! finite-choice-count (pair k e) ?!})
-}


Faces of cubes

face-cube :
(k : ℕ) (X : cube (succ-ℕ k)) (d : dim-cube (succ-ℕ k) X)
(a : axis-cube (succ-ℕ k) X d) → cube k
pr1 (face-cube k X d a) =
complement-element-UU-Fin k (pair (dim-cube-UU-Fin (succ-ℕ k) X) d)
pr2 (face-cube k X d a) d' =
axis-cube-UU-2 (succ-ℕ k) X
( inclusion-complement-element-UU-Fin k
( pair (dim-cube-UU-Fin (succ-ℕ k) X) d) d')