Semisimplicial Types

The following is allegedly a definition of semisimplicial types in type theory, specifically in Agda. Since this is supposed to be an open problem, and the definition I have below is fairly simple, I expect it's probably wrong in some way. Perhaps understanding why it's mistaken is a good puzzle.

The code described here, plus examples and further lemmas, is in this github repo.

First we have the standard Agda module header.

{-# OPTIONS --without-K #-}
module SemiSimplicialType where

We define equality in the usual way.

data _≡_ {ℓ} {A : Set ℓ} : (a b : A) → Set ℓ where refl : {a : A} → a ≡ a

We define the square of a type; Sq A is just A × A.

record Sq (A : Set) : Set where constructor ⟨_,_⟩ ; field fst snd : A
open Sq

We define a notion of $n$-dimensional cubes in a type $C$. A value of Cube C is a value of type $C^{2^n}$ for some $n$.

data Cube : (C : Set) → Set1 where
 leaf : {C : Set} → C → Cube C
 node : {C : Set} → Cube (Sq C) → Cube C

We can depict these as tables. Here's an example 3-dimensional cube, assuming $c_0, \ldots, c_7$ are some values in $C$:

$\chi \quad=$	$c_0$	$c_1$		$c_4$	$c_5$
$\chi \quad=$	$c_2$	$c_3$		$c_6$	$c_7$

This would be represented in Agda syntax as

node (node (node (leaf ⟨ ⟨ ⟨ c0 ,  c1 ⟩ , ⟨ c2 , c3 ⟩ ⟩ ,
                         ⟨ ⟨ c4 ,  c5 ⟩ , ⟨ c6 , c7 ⟩ ⟩ ⟩)))

We define a map combinator on Cube which hits every leaf with a given function.

cmap : {C D : Set} → (f : C → D) → Cube C → Cube D
cmap f (leaf x) = leaf (f x)
cmap f (node c) = node (cmap (λ (⟨ x , y ⟩) → ⟨ f x , f y ⟩) c)

Next we define a "subcube" relation between a pair of Cubes that says that the former arises from the latter by maybe deleting some dimensions, and leaving only the data that's closer to the "upper-left" corner of the cube.

data _≤_ : {C : Set} → Cube C → Cube C → Set1 where
  ε : {C : Set} {c : C} → leaf c ≤ leaf c
  Y_ : {C : Set} {χ χ' : Cube (Sq C)} → χ ≤ χ' → node χ ≤ node χ'
  N_ : {C : Set} {χ χ' : Cube (Sq C)} → χ ≤ χ' → cmap fst χ ≤ node χ'

So for example, the subcubes of $\chi$ above consist of the 0-dimensional cube that contains only $c_0$, the three 1-dimensional cubes $(c_0\ c_1)$, $(c_0\ c_2)$, and $(c_0\ c_4)$, the three 2-dimensional cubes

$c_0$	$c_1$	,	$c_0$	$c_2$	,	$c_0$	$c_1$
$c_2$	$c_3$	,	$c_4$	$c_6$	,	$c_4$	$c_5$

and finally $\chi$ itself.

Next we define a function that helps us get the "upper-left-most" cell and "lower-right-most" cell in a cube.

pole : {C : Set} → ({C : Set} → Sq C → C) → Cube C → C
pole f (leaf c) = c
pole f (node s) = f (pole f s)

We call the "upper-left-most" cell the "nadir" and "lower-right-most" cell the "apex".

nadir = λ {C : Set} → pole {C} fst
apex = λ {C : Set} → pole {C} snd

We can now define the (large) type of semisimplicial types.

record SemiSimplicialType : Set1 where
  constructor sst
  field
    C : Set
    ⋆ : C
    ∂ : (c : C) → Cube C
    apex-axiom : (c : C) → apex (∂ c) ≡ c
    nadir-axiom : (c : C) → nadir (∂ c) ≡ ⋆
    reduce-axiom : (c : C) {χ : Cube C} → χ ≤ ∂ c → ∂ (apex χ) ≡ χ

We require:

a type C of cells, lumping all cells of various dimensions together in "untyped" fashion.
an element ⋆ which is to be the unique (-1)-dimensional cell to get the induction going.
a map ∂ which for every cell gives its complete boundary as a cube. This specifies the dimension, and all vertices, edges, faces, etc. of a simplex all at once. As yet we don't know that those subcells fit together in any coherent way. That is the job of the following three axioms.
(For the sake of illustrating the axioms, suppose we want to represent a 2-simplex named abc which is supposed to be the triangle whose vertices are a, b, c and whose edges are named ab, bc, ac. Then the boundary of abc ought to be the 3-cube

∂ abc = ⋆ a c ac

b ab ab abc

)
The apex-axiom says that the apex of the boundary of any cell is that cell itself. In the example above, we see that the bottom-right-most cell of ∂ abc = is indeed abc itself.
The nadir-axiom says that the nadir of the boundary of any cell is the cell ⋆. In the example above, we see that the top-left-most cell of ∂ abc = is indeed ⋆.
Finally, the reduce-axiom says that any subcube of a boundary cube is also a valid cube — that is, it really is the boundary cube of its apex. In our example, this requires things such as ∂ a = (⋆ a) and

∂ ac = ⋆ a

c ac

This captures that a, b, c really are vertices of the semisimplicial type — for their boundaries are 1-dimensional cubes — and that the putative edge cells ab, bc, ac really are valid edges of the type, for their boundaries are 2-dimensional cubes that hereditarily satisfy reduce-axiom as well.

`∂ abc =`	`⋆`	`a`		`c`	`ac`
`∂ abc =`	`b`	`ab`		`ab`	`abc`

`∂ ac =`	`⋆`	`a`
`∂ ac =`	`c`	`ac`