From Cubes to Twisted Cubes via Graph Morphisms in Type Theory
Gun Pinyo Nicolai Kraus


Bootstrapping quantum process tomography via a perturbative ansatz
    H. Krovi
    
==================================================================




  Cube categories are used to encode higher-dimensional
  categorical structures.  They have recently gained significant
  attention in the community of homotopy type theory and univalent
  foundations, where types carry the structure of higher groupoids.
  Bezem, Coquand, and Huber <cit.> have
  presented a constructive model of univalence using a specific cube
  category, which we call the BCH cube category.
  
  The higher categories encoded with the BCH cube category have the
  property that all morphisms are invertible, mirroring the fact that
  equality is symmetric.  This might not always be desirable: the
  field of directed type theory considers a notion of equality
  that is not necessarily invertible.
  
  This motivates us to suggest a category of twisted cubes
  which avoids built-in invertibility.  Our strategy is to first
  develop several alternative (but equivalent) presentations of the
  BCH cube category using morphisms between suitably defined graphs.
  Starting from there, a minor modification allows us to define our
  category of twisted cubes.  We prove several first results about
  this category, and our work suggests that twisted cubes combine
  properties of cubes with properties of globes and simplices
  (tetrahedra).




§ INTRODUCTION AND MOTIVATION


A cube category is a category whose objects are (or represent)
finite-dimensional cubes, and whose morphisms are mappings of some
sort between these cubes.  There are many different cube
categories <cit.>, and they are used to encode higher
categorical structures.

Homotopy type theory <cit.> is a variation of
Martin-Löf's intensional type theory.  The characteristic and novel
view adapted in homotopy type theory is that types carry the structure
of higher categories, or, to be precise, higher groupoids (i.e. all
morphisms are invertible).  This view supports Voevodsky's
univalence principle which should be seen as a central concept
of homotopy type theory.  The first model of such a type theory, given
by Voevodsky <cit.> (see also
the presentation by Kapulkin and
Lumsdaine <cit.>), uses simplicial sets.
However, it is still an open question how simplicial sets can be used
to build a constructive model of type theory with univalent
universes <cit.>.  Using cubical sets,
this has been achieved by Bezem, Coquand, and
Huber <cit.>.  Starting from there, cubes
have gathered a lot of attention in the type theory community, leading
to various cubical type theories which have univalence not as
an axiom but as a built-in derivable
principle <cit.>.  Many different cube categories have
been considered in this context.

The important cube category used by Bezem, Coquand, and
Huber <cit.> (from now on referred to as
the BCH cube category) uses finite sets of variable names as
objects, and a morphism from a set I to a set J is a function
f : I → J ∪{0,1} which is “injective on the left part”,
i.e. f(i_1) = f(i_2) = j with j : J implies i_1 = i_2.  One
goal of this paper is to develop several alternative presentations of
this category, mainly using graph morphisms.  We have two main
motivations to do this.  The first is that, as we hope, our
alternative and intuitive (but equivalent) definitions enable new
views on the category and facilitate the discovery of further
observations.  The second motivation is that a minor change in the
definition will allow us to construct a new cube category, the
twisted cubes from the title. We will come back to this in a
moment.

The standard way to create models (of both higher categories and type
theories) using simplicial or cubical index categories is to take
presheaves and equip them with certain Kan-filling conditions.
These filling conditions entail composition of morphisms as well as
associativity and all higher coherence laws that one needs.  A typical
such Kan-filling condition for the 2-cube
[While Bezem, Coquand, and
  Huber <cit.> define their index
  category to have finite sets of variables as objects, it is possible
  to simply use natural numbers as objects.  The n-cube, or
  n-dimensional cube, is then the object of the presheaf
  category that is represented by the object n of the index
  category.], as shown on the left of <ref>, says that,
given the “partial square” of three solid edges on the right, one
can always find the dashed edge (together with an actual filler for
the square).



One important observation here is that, in the case of the BCH cube
category and other cube categories, invertibility of morphisms is
built-in.  Consider the partial square, as shown on the middle of
<ref>, where two of the three solid edges are identities
and the third is an actual non-trivial morphism (or equality) p from
x to y.  Using the Kan filling operation described above, we get a
morphism from y to x, which serves as the inverse of p.

The invertibility of morphisms is useful for most forms of type
theory, where equaliy is symmetric.  This however is not always the
case, cf. the proposals for directed type theories by Licata
and Harper <cit.>, Nuyts <cit.>, Riehl
and Shulman <cit.>, North <cit.>, and
others.  Their aim is to generalise type theory by replacing
(higher) groupoids by general (higher) categories.  In a
nutshell, this means that “equality” (or whatever takes the place of
equality) is not necessarily invertible.

We think that a very valuable long-term goal would be to make the
connection of directed type theories with cubical type theories and
create some sort of directed cubical type theory.  This is at
the moment certainly out of reach, and we do not know how such a type
theory could be built.  Nevertheless, it motivates us to explore
variations of the BCH cube category which do not have the described
built-in equality.

To avoid invertibility, we “twist” the left-most edge of the
2-dimensional cube, as shown on the right of <ref>, to
ensure that the construction from before becomes impossible. This
might seems artificial and specific to the 2-dimensional case but by
using our graph morphisms that we develop for the BCH cube category,
it becomes very easy to define the twisting version for cubes of all
dimensions.

To construct a twisted n-cube from a twisted (n-1)-cube, we first
expand the original cube along a new dimension (we call this
thickening): this is same as constructing a standard n-cube
form a standard (n-1)-cube, which is just a construction of its
cylinder object. We then reverse all dimensions at the starting
point of the new dimension (we call this twisting).
<Ref> illustrates this
thickening-and-twisting process up to dimension 3, where the
existing dimensions are shifted by one in order to allow the new
dimension to be the first dimension.



One important property of standard cubes which twisted cubes retain is
that every face of a [twisted] n-cube is a [twisted] (n-1)-cube.
An interesting example is the case n = 3: In order to construct a
twisted 3-cube, we thicken the twisted 2-cube as illustrate in
<ref> where the left and the
right face are already twisted 2-cubes, while the rest are thickened
1-cubes.  The right face is unaffected during the twisting, but the
left face is reversed entirely.  Nevertheless, it is still a 2-cube
(just flipped backwards).






Twisted cubes do not only remove the discussed source of
invertibility, but they also change the way we view composition of
morphisms.  The filling of a “standard” square can be interpreted as
saying that the composition of two edges equals the composition of the
other two edges, and if we want to see the lid as the composite of the
three other edges, then one has to be inverted.  In contrast, in the
twisted square, the lid can be seen directly as the single composite
of the three other edges.  The right half of <ref>
shows the projection of the twisted 3-cube, and the smallest square
(011, 001, 101, 111) is the lid.  As for the square, this lid should
be seen as the composite of the other (here five) faces.  Intuitively,
one starts with the biggest square, composes it with the top and the
bottom squares, then with the left and the right square, and thus
arrives at the smallest square.  <Ref> shows the
analogous situation for the 4-dimensional twisted cube, where one
starts with the inner 3-cube, then extends to the front and the
back, to the top and the bottom, and finally to the left and the
right.

The “twisting” pattern also appears in the twisted arrow
  category <cit.>, also known as the
category of factorisations <cit.>.
However, it is unclear how to generalise this idea to more than
squares; it has been developed to solve a different problem.

In the main body of the paper, we first introduce the framework of
graph morphisms for standard (non-twisted) cubes.  We consider the
properties of meet/join and dimension preservation of graph morphisms,
and conclude that both of these are suitable refinements to ensure
that the category of graph morphisms matches the BCH cube category. The
proof of this is the main result of <ref>.  We use
this development to introduce and examine twisted cubes in
<ref>.  We will see that they have many
characteristic properties that standard cubes are lacking.  Some of
them, such as a Hamiltonian path through the cube and the fact that
vertices are totally ordered,
are familiar from simplicial structures but
not from cubical ones.  Another interesting feature, neither familiar
from cubical nor from simplicial but from globular structures, is
that surjective maps are unique (i.e. there is only one way to
degenerate a twisted cube).  These and other observations allow us to
define a further representation of the category of twisted cubes which
does not make use of graphs.



    Setting
 We use a standard version of Martin-Löf's
dependent type theory as our meta-language.  We assume function
extensionality, but we do not require other axioms or features since
we mostly work with finite sets, which are extremely well-behaved by
default.  In particular, it does not matter for us whether UIP/Axiom K
is assumed or not, and the development would be identical in
extensional dependent type theory.



    Summary of Contributions

Our main contributions are as follows:

 
  * We give several alternative but equivalent presentations of the
   BCH cube category.
 
  * We introduce twisted cubes, a variation of the BCH cube
   category which allows for filling conditions without built-in
   invertibility.
 
  * We show several results about twisted cubes.  These include
   connections to simplices (a unique Humiliation path and the
   property of being a Reedy category) and to globes (unique
   surjective maps and degeneracies).




§ A STANDARD CUBE CATEGORY
 

In this section, we discuss various representations of the cube
category .  This category was used by Bezem, Coquand, and
Huber to present a constructive model of
univalence <cit.>.  In
<ref>, we will see how minimal modifications lead to
a category of twisted cubes.

Keeping in mind that we use type theory as the language in which the
results are presented (i.e. as our meta-theory), we use the following
notations:  are the natural numbers, including 0.  For n :,
the set n is the finite set with elements
{0, 1, …, n-1}.  In particular, 2 is the set of
booleans.  As usual, n^ m is simply the function
set m → n.  We denote elements of
2^ n by binary sequences as in
0 · 1 · 1 · 0.  This means such a function f is
denoted by f(0) · f(1) · f(2)… f(n-1).  If there is no
risk of confusion, we omit the · and simply use juxtaposition as
in 0110.

In several situations, we want to consider a type of functions into a
coproduct which is injective “on the left part of the
codomain”.  To make this precise, we introduce a notation:
  Assume A, B,
  and C are given types.  For a function f : A → (B+C), we say
  that f is injective on the left part if
 
    (f) Π(x,y : A, z : B). (f(x) = (z)) → (f(y) = (z)) → x = y.

 We write the type of functions which are injective on the left part as
 
    (A  B+C) Σ (f: A → (B+C)). (f).



In the next lemma, a function f : A → B +  1 is called a
partial function, with 1 being the “undefined”
part.[
  Technically, these are of course only the partial functions from A
  to B with decidable support. Since we only work with finite types,
  it is not surprising that we only need to consider the decidable
  case.]  The following simple but useful (and well-known) result will
be necessary.  It could be formulated in higher generality, but a
version which is sufficient for us is this:

  Given m,n :, injective
  partial functions from m to n are in bijection
  with injective partial functions from n to m.
  In other words, we have an equivalence

    ( m  n +  1) ≃( n  m +  1).



  The equivalence can be constructed directly. Given an
  f :  m  n +  1, we have to construct
  a function g :  n  m +  1.  For
  i :  n, we can decide whether there is a k such that
  f(k) = (i).  If so, then this k is unique due to
  injectivity, and we set g(i) (k); otherwise, we set
  g(i) (0).  Checking that this is an equivalence is
  routine.


The presentation of the cube category in question that we start with
is the one given by Bezem, Coquand, and
Huber <cit.> (which is the same as in
Huber's PhD thesis <cit.>).  Since it is sufficient for
our purposes, we use a skeletal variation: our objects are not finite
sets but rather natural numbers.

 
  The category  has natural numbers as objects and, for
  m, n :, a morphism in (m,n) is a function
  f :  m → n +  2 which is injective on the
  n-part.  In type-theoretic notation:
 
    (m,n)  m  n +  2

 Composition g ∘ f is defined to be the set-theoretic
 composition (g + 𝗂𝖽_2) ∘ f.


What we will need is the opposite of this category, .
While the above definition is short and abstract, a description close
to the intuitive idea of cubes is helpful for our later developments.
Let us consider graphs G = (V, E) of nodes (vertices) and
edges, where V is a set with decidable equality and E is a subset
of V × V.  A standard way to implement this is to let E be a
family of “mere propositions”[Recall that a mere
    proposition, or a subsingleton, is a type with at most one
  element.], indexed twice over V.  However, we write (s,t) : E
for E(s,t) and assume that E is given in the “total space”
formulation.  Furthermore, in our cases E will always be a
decidable subset.

E being a subset means that our graphs do not have multiple
parallel edges, i.e. for any pair of vertices, there is at most one
edge between them, and it is decidable whether there is an edge
between two given vertices.

Given a graph, we construct a new graph as follows.  Note that the
“total space” of the edges of the new graph is E + E + V, but in
order to make clear which vertices these new edges connect, we use
“set theory style” notation:
  Given G = (V, E), the
  graph-prism of G, denoted as 

  (G)  (  (V),   (E))
  is another graph where
  
    (V)      × V
        
      (E)      { ( (0,  s),  (0, t) )   |   (s, t) : E }
    ∪    { ( (1,  s),  (1, t) )   |   (s, t) : E }
    ∪    { ( (0,  v),  (1, v) )   |   v : V }.



This allows us to define the standard cube as a graph:[Most
  of graphs in this paper are reflexive graphs to support degeneracies
  as graph morphisms.]
 
  Given n :, the standard cube n is defined as follows:
  
    0     (1,   {(0, 0)})                    n + 1      (n)
  

Another way of defining n, without recursion, is the
following.  Here, we give the “total space” of edges
𝖾𝖽𝗀𝖾𝗌( n) together with functions
𝗌𝗋𝖼, 𝗍𝗋𝗀 : 𝖾𝖽𝗀𝖾𝗌( n) →𝗇𝗈𝖽𝖾𝗌( n):
  In the following,
  our convention is that -1 is empty (i.e. the same as
  0):
 
    𝗇𝗈𝖽𝖾𝗌( n)             ^ n
       𝖾𝖽𝗀𝖾𝗌( n)             ^ n 
         + ( n ×^n-1) 
       𝗌𝗋𝖼((v))     𝗍𝗋𝗀((v))              v 
       𝗌𝗋𝖼((i, x_0x_1… x_n-2))              x_0x_1… x_i-1 0 x_i … x_n-2
       𝗍𝗋𝗀((i, x_0x_1… x_n-2))              x_0x_1… x_i-1 1 x_i … x_n-2



The number of total edges in (<ref>) comes
from the following calculation.  We have n dimension, thus 2^n
nodes, which come with self-loops giving rise to the summand
^ n.  For ever node, we further have an edge in each
dimension.  Avoiding double counting, this gives the summand
n ×^n-1.
<Ref> shows drawings for 0 to
3.


<Ref> and <ref> 
define isomorphic graph structures. 

This observation allows us to use whichever is more convenient in any
given situation.



A graph morphism from G = (V,E) to G' = (V',E') is, as
usual, a function between the node types which preserves the edges:

    (V,E)(V',E')Σ (f : V → V'). Π(v_0, v_1 : V). E(v_0,v_1) → E'(f(v_0),f(v_1))


We can now consider the following category:
 
  The category  has natural numbers as objects. 
 A
  morphism between m and n is a graph morphism from m to
  n, as in:
 
    (m,n)  m n

 Composition is composition of graph morphisms.


The category  has more morphisms than .  One
example would be the morphism in 2 1 which
maps the three nodes 00, 01, 10 all to 0 and 11 to 1.
Another example is the morphism which maps 00 to 0, and 01,
10, 11 all to 1.  Both of these morphisms do not have analogues
in .  In other words,  has connections.
Since, in the current paper, we are looking for alternative
definitions of the category , we refine the definition of
the morphisms in  to resolve the mismatch.  Let us
formulate the following auxiliary definitions.

 
  For a given graph G = (V,E), we write G^* = (V, E^*) for the
  free preorder generated by it.  G^* has V as objects and, for
  v,u : V, we have v ⩽ u if there is a chain of edges
  starting in v and ending in u.
 
  When talking about nodes in G, we borrow the notions of
  meet (product) and join (coproduct) from preorders.
  If they exist in G^*, we write them as v  u and
  v  u.


It is easy to see that, in the case of n, all meets and joins
exist and can be calculated directly: From the programming
perspective, they correspond to the bitwise operators ''
and ''.  Thus, when talking about n, we can view
 and  as actual functions calculating the binary meet
and join:

    ,  : V × V → V

Given a graph morphism g :  m n, it is easy
to define what it means that it preserves binary meets resp. joins:

    (g) Π (u,v : ^ m). g(u  v) = g(u)  g(v) 
       (g) Π (u,v : ^ m). g(u  v) = g(u)  g(v)

Note that preserving meets and joins is a property (a “mere
proposition”) of morphisms.  For general morphisms between graphs
which might not have all meets or joins, the definition is more subtle
but still straightforward; one can always define the property of
being a meet (join) and then say that any vertex which has this
property is mapped to one which also has it.  We omit the precise
type-theoretic formulation.

The two mentioned examples of morphisms which are “too much” in
 do not preserve binary meets resp. joins.

  The
  category  has  as objects and, as morphisms, graph
  morphisms between standard cubes which preserve meets and joins
  (𝖼𝗈𝗇𝗍 for continuous):
 
    (m,n) Σ (g :  m n).
         (g) ×(g)



This gives us a category which is indeed equivalent (in fact
isomorphic) to :

  The categories
   and  are isomorphic.  The isomorphism on the
  object part is the identity, i.e. the equivalence is given by a
  family e as in:
 
    e : Π(m,n : ). (m,n) ≃(m,n).




Before giving a proof, we formulate the following:
  Consider the full subgraph
  of n which has exactly (n+1) vertices, namely the
  “origin” 00… 0 and the “base vectors” which have exactly
  one 1.  We call this subgraph B_n, where the B stands for
  “base”, and it comes with the inclusion
  i : B_n ↪ n.  For any m, “forgetting” the
  property of preserving the joins and composing with i as in
 
    λ g. i ∘ (𝗉𝗋𝗈𝗃_1(g)) :  (Σ (g :  m n. (g))  → B_m n

 is an equivalence.  Moreover, g preserves meets if and only if
 i ∘ (𝗉𝗋𝗈𝗃_1(g)) does.


.75

  The only binary joins that B_m has are trivial, so every morphism
  B_m n is join-preserving. Thus, the first claim
  of the lemma is that every such morphism can be extended in a unique
  way as shown in the diagram to the right.  Every node of m
  which is not in B_m, i.e. every node which is not the origin or a
  base vector, can be written as a join of base vectors.  Since we
  need to preserve joins, it is therefore determined where the node
  has to be sent to.  The map defined in this way preserves all binary
  joins, and it preserves binary meets if and only if the input does.


.20
[x=2cm,y=-2cm,baseline=(current bounding box.center)]
 (Gn) at (0,0) B_m;
 (Cm) at (1,0) n;
 (Cn) at (0,1) m;

 [->] (Gn) to node  (Cm);
 [right hook->] (Gn) to node  (Cn);
 [->,dashed] (Cn) to node  (Cm);




  We first give the overview of the argument as a chain of
  equivalences, then we justify each step [S1 – S5].

                         (m,n) 

             ≡       Σ(g : mn). (g) ×(g) 

     1        ≃       Σ(g : B_mn). (g) 

     2        ≃       Σ(z : 2^n, d : m n + 1). Π(i:m, j : n). (d(i) = (j)) →(z(j) = 0) 

     3        ≃       Σ(z : 2^n, e : n m + 1). Π(i:m, j : n). (e(j) = (i)) →(z(j) = 0) 

     4        ≃       Σ(z : 2^n, e : n →(m + 1)). (e) ×Π(i:m, j : n). (e(j) = (i)) →(z(j) = 0) 

     5        ≃       Σ(α: Π(j : n). Σ(e : m + 1, z : 2). Π(i : m).(e = (i)) →z = 0). (𝗉𝗋𝗈𝗃_1 ∘α) 

     6        ≃       Σ(α: Π(j : n). m + 2). (α) 

             ≡       (m,n) 


Step 1 holds by <ref>.  Let us look at Step 2.
Giving a graph homomorphism between B_m and n corresponds to
choosing where the origin is mapped to, and choosing where each
(non-trivial) edge of B_m is mapped to.  For the origin, we use the
component z :  2^ n.  There are m non-trivial
edges in B_m, and z is an endpoint (or starting point) of n
non-trivial edges and one trivial edge in n.  This gives us up
to m → n +  1 possible functions, but since
we only consider meet-preserving morphisms, every function needs to be
injective on the left part, leading to
d :  m  n +  1.  Moreover, if
d(i) = (j) for some i,j, then the image of the origin must be
the starting point of the edge in dimension j, i.e.z(j) = 0.  Step 3 is an application of <ref>
(it essentially swaps the roles of m and n).  Step 4 only unfolds
the definition of .

In Step 5, the usual distributivity between Σ and Π (under
the propositions-as-types view referred to as the “axiom of choice”)
is used: z, e, and the unnamed last component can all be seen as
(dependent) functions with domain n.  The dependent function
α combines them into a single dependent function with domain
n and a codomain that consists of multiple components which,
again, are called e, z, with the last one being unnamed.  Only the
component expressing the “injectivity on the left part”-property
cannot be seen as a function in n.  In Step 6, we massage
the codomain of α: We have e :  m +  1 and also
z :  2, but the condition says that z is determined unless
e = (0); thus, the type is equivalent to
m +  2.

We omit the calculation which shows that the constructed equivalence
preserves composition of morphisms in the categories.


In <ref>, we will switch from standard cubes to
twisted cubes.  The directions of some edges will be reversed.  It is
therefore an advantage to formulate a condition similar to the one
about meets and joins without referring to the direction of edges.
This is indeed possible:

  Given the standard cube
  n, where we use the non-recursive definition as in
  <ref>, the dimension of an edge is
  defined as follows:
 
    : 𝖾𝖽𝗀𝖾𝗌( n) → n +  1
             ((v))          (0) 
              ((i, x_0… x_n-2) (i)

 We say that a morphism f :  m n is
 dimension-preserving if f maps edges of the same dimension
 to edges of the same dimension,
 
    (f) Π(e_1,e_2 : 𝖾𝖽𝗀𝖾𝗌( n)). ((e_1) = (e_2)) → ((f(e_1)) = (f(e_2))).

 The category  makes use of these concepts:
 
    𝗈𝖻𝗃()    (m,n) Σ (g :  m n). (g)



As (g) and (g), preserving the dimension as
in (<ref>) is a proposition in the sense of homotopy
type theory (has at most one proof).

  For a graph morphism f
  as in the definition above, the following condition says that f is
  “injective on dimensions” (on the non-trivial part):
 
    (f) Π(e_1,e_2 : 𝖾𝖽𝗀𝖾𝗌( m), j :  n) . 
        ( (f(e_1)) = (j) ×(f(e_2)) = (j) ) 
       → ((e_1) = (e_2)).

 However, note that this follows directly from (f): Assume
 e_1, e_2 are edges such that (f(e_1)) and
 (f(e_2)) are equal and non-trivial.  If e_1 and e_2 are
 not “parallel” (i.e. not in the same dimension), then we can find
 e_1' in the same dimension as e_1 such that e_1' and e_2 are
 adjacent (i.e. the endpoint of one is the starting point of the
 other). It is clear that f(e_1') and f(e_2) cannot go into the
 same non-trivial direction, since we can only go one step into a
 given direction before going back.
 

The connection to meet- and join-preserving is given by the following result:
  A morphism
  f :  m n is join-and-meet-preserving
  exactly if it is dimension-preserving.


  This follows easily by going via morphisms B_mC_n as
  in <ref>.  The graph B_m has exactly one
  edge for every non-trivial dimension, and the proof is analogous to
  the one of <ref>.



  The categories , , and  are
  isomorphic. 




§ A CATEGORY OF TWISTED CUBES
 

As discussed in the introduction, we build on our framework of graph
morphisms to define a category of twisted cubes.  A variation
of <ref> gives us these twisted cubes.  The
critical change can be seen in (<ref>), which should
be compared with (<ref>):

  Given a graph
  G = (V,E), the twisted graph-prism of G, 
 denoted as
  (G)  (  (V),    (E)) is the graph defined by
  
    (V)      × V  
      (E)      { ( (0,  t),  (0, s) )   |   (s, t) : E }
    ∪    { ( (1,  s),  (1, t) )   |   (s, t) : E }
    ∪    { ( (0,  v),  (1, v) )   |   v : V }.



We then define:
 
  Given n :, the twisted cube n is defined as follows:
  
    0     (1,   {(0, 0)})                    n + 1      (n)
  


Alternatively, we can tweak <ref> to get a
non-recursive definition. As before, the convention is that
-1 is empty.
 
 The non-recursive definition of n is as follows:
 
    𝗇𝗈𝖽𝖾𝗌( n)             ^ n
       𝖾𝖽𝗀𝖾𝗌( n)             ^ n 
         + ( n ×^n-1) 
       𝗌𝗋𝖼((v))     𝗍𝗋𝗀((v))              v 
       𝗌𝗋𝖼((i, x_0x_1… x_n-2))              x_0x_1… x_i-1· b · x_i … x_n-2
       𝗍𝗋𝗀((i, x_0x_1… x_n-2))              x_0x_1… x_i-1· (1 - b) · x_i … x_n-2

 where b = 1 if the total number of zeros in x_0x_1… x_i-1
 is odd, and b = 0 otherwise.

This means that an edge is reversed (compared to the standard cubes
discussed before) exactly if the number of zeros in dimensions that
come before the edge is odd (note that the condition talks
about x_i-1, not x_n-2).  The twisted cubes of dimension up to
3 are illustrated in <ref>; see also
<ref> in the introduction.


  <Ref> and <ref>
  define isomorphic graph structures. 





n has an interesting property that the standard cube
n does not have: The induced preorder n^* on the
vertices is a total order.  This observation was originally suggested
by Paolo Capriotti and Jakob von Raumer in a discussion with the first
author of this paper. Note that this observation should not be
misunderstood to mean that n itself is uninteresting.  Its
edges give it a unique structure, as visualised in
<ref>.



The idea behind this result is that  preserves the
property of having a preorder that is total.  To elaborate on this, if
G^* is a total order, then (  G)^* consists of
two copies of G^*, where the first copy is “turned around”.  One
of the edges added in (<ref>) links the
largest node in the first copy to the smallest node in the second
copy, thus every element of the second copy is larger than all the
elements of the first copy.  In other words,
(  G)^* is the join of the two copies.
[Join in the sense of the join of categories <cit.>, which should not be confused with the join (coproduct) of objects in a preorder (cf. <ref>).]

  For all n :, the preorder
  n^* is isomorphic to the total order
  ( 2^ n, <).


Note that <ref> is a property which one usually
expects for simplicial structures, but not for cubical ones.


  There are
  two binary numbers for each node in <ref>.  The bottom
  one represents each node name according
  to <ref> whereas the top one represents
  the total order of 3.  It is impossible to unify these two
  binary numbers for n ⩾ 2 since, for each edge e, the
  numbers 𝗌𝗋𝖼(e) and 𝗌𝗋𝖼(e) only differ by (at
  most) one single bit by <ref>, while
  incrementing a binary number can flip more than one bit.


Another related observation is that we can find a path from the
smallest vertex to the largest vertex of n which respects
the direction of the edges, and which visits each vertex exactly
once. Recall that such a path is called a Hamiltonian path.  We
record this:

  For all n :, there is
  exactly one Hamiltonian path through n+1.  This path
  contains exactly one edge in the first dimension (i.e. the one
  which is added when going from n to n+1).
  Moreover, this single edge in the new dimension connects the
  Hamiltonian paths through the two copies of n of which
  n+1 consists by definition, cf. (<ref>).


  As before, we denote elements of 2^ n as
  sequences such as 00101 (binary representation with most
  significant bit first) or, for clarity, by
  0 · 0 · 1 · 0 · 1.  We use the endofunction
   on 2^ n, which simply replaces each 0
  in a sequence by a 1 and vice versa; i.e. it sends the number i
  to 2^n - 1 - i (note that  does not reverse the sequence,
  but the ordering on 2^ n).
 
  Let us define endofunctions f_n and g_n on
  2^ n, by induction on n. Note that, at this
  point, we do not talk about graph morphisms but only about functions
  between sets.  The base cases of the induction are uniquely
  determined. We define f and g by
 
    f_n+1 (0 ·x⃗)  0 · f_n((x⃗))        g_n+1 (0 ·x⃗)  0 ·(g_n(x⃗)) 
        f_n+1 (1 ·x⃗)  1 · f_n(x⃗)         g_n+1 (1 ·x⃗)  1 · g_n(x⃗).


 It is easy to calculate that, by induction, f and g are inverse
 to each other.  We want to show that they extend to morphisms between
 preorders,
 
    f̂_n : ( 2^ n, <) → n^*
         ĝ_n :  n^* → ( 2^ n, <).


 To construct f̂_n and the Hamiltonian path through the
 cube, it suffices to show: for x,y :  2^ n with
 x+1=y, we have an edge f_n(x) → f_n(y).
 
 We do induction on n. For n = 0, this is vacuously true (such
 x,y do not exist).  For n = n' + 1, there are multiple cases:
 
 
  * case x = 0 · x' and y = 0 · y': Then, the
   assumption gives us x'+1=y' and we have to find an edge
   0 · f_n((x')) → 0 · f_n((y')).  Looking
   at <ref>, we can get this if we have
   f_n((y')) → f_n((x')).  This holds by induction,
   since  reverses the order which gives us
   (y')+1 = (x').
 
  * case x = 1 · x' and y = 1 · y': Similar to the
   previous case, but nothing gets reversed.
 
  * case x = 0 · x' and y = 1 · y': In this case, we
   have x = 0111… and y = 1000….  We need to find an
   edge 0 · f((111…)) → 1 · f(000…),
   which simplifies to
   0 · f(000…) → 1 · f(000…).  This edge is
   directly given in (<ref>).
 
  * case x = 1 · x' and y = 0 · y': Contradicts with
   the assumption x+1 = y.
 
 This shows that there is a Hamiltonian path, and it is given by
 f̂_n.  The definition of f as in
 (<ref>,<ref>) also shows that f_n+1
 consists of two copies of f_n, implying the last claim of
 <ref>.  In order to prove <ref>, we
 need to construct ĝ_n.  It is enough to show that, for an edge
 from u to v in n, we have g(u) ⩽ g(v).  This
 follows by straightforward induction, going through the edges in
 <ref>.  But <ref> implies that
 there is at most one Hamiltonian path.



  Note that every vertex v in n is an endpoint of n
  non-trivial edges.  The number of zeros in the binary representation
  in the “order number” of v (i.e. the value g_n(v) in the
  proof of <ref>) equals the number of
  outgoing edges.  <Ref> shows this.


Analogously to <ref>, we can now define the
category of twisted graph morphisms:

 
  The category  has natural numbers as objects, and
  morphisms from m to n are graph morphisms between twisted cubes:
 
    (m,n)  m n



It is easy to see that the category  has a version of
connections.  Since we are looking for a “twisted analogue” of
, we need to refine it further.  In
<ref>, we have discussed the restriction to (meet
and join)-preserving morphisms, and to dimension-preserving morphisms.
It follows directly from <ref> that every morphism in
 preserves all binary meets and joins, so this condition
becomes trivial; it does not avoid connections.  However, preserving
dimensions is still a non-trivial condition which does avoid
connections.  The definition of equation (<ref>)
still works.


  The category  has dimension-preserving maps between
  twisted cubes as morphisms:
 
    𝗈𝖻𝗃()    (m,n) Σ (g :  m n). (g)



Note that the explanation of <ref> holds for the
twisted cube category as well.

A consequence of <ref> is that morphisms in
 cannot “swap dimensions”.  But an even stronger result
holds, namely that surjective morphisms are unique:
 
 There is exactly one surjective morphism in (m,n) 
 for m ⩾ n. 
 (Clearly, there is none if m < n.)


  The key to the proof is <ref>.  Clearly, the
  Hamiltonian path in m goes through all vertices.  Due to
  surjectivity, its image has to go through all vertices of
  n.  In other words, the m-Hamiltonian path has
  to be mapped to the n-Hamiltonian path.  Since the graph
  morphisms that we consider preserve the dimension, the only edge in
  the m-path which can be mapped to the single edge in the
  first dimension in the n-path is just this single edge in
  the first dimension in the m-path; i.e. the middle edge
  has to be mapped to the middle edge.  From here, it follows by
  induction that there can only be at most one surjective graph
  morphism.
 
  What is left to show is that there actually is a surjective graph
  morphism if m ⩾ n.  It is enough to construct a surjective
  graph morphism f : (n+1,n), from where we get any other
  by (m-n)-fold composition (0-fold composition is the identity).
  Such a graph morphism is given by
 
    f(x_0 … x_n-1 x_n)  (x_0 … x_n-1).

 Since the directions of the edges do not depend on the very last
 dimension, this works (cf. <ref>).


An important consequence of the above result is that there is a unique
way to degenerate a twisted cube.  We do not go into the details here,
but see the conclusions at the end of the paper.  For now, we go into
a different direction.

Let us write  (“interval”) for the finite set
{0,1,⋆}.  Of course,  is isomorphic to 3, but
referring to the last element as ⋆ helps the intuition, we hope.


  A face of the twisted n-cube n is a function
  f :  n →.  The dimension of a face, written
  (f), equals the number of times f takes ⋆ as value
  (i.e. the size of f^-1(⋆)).  The type of faces of dimension
  k is written as 𝖿𝖺𝖼𝖾𝗌(n, k).


The face f :  n → represents the full subgraph of
n of vertices on which f “matches” (a vertex
x_0x_1…x_n-1 is matched if, for every i, we have
f(i) = x_i or f(i) = ⋆).

 
 The image of f : (m,n) is a face.


  This follows from the property of preserving the dimension as
  defined in (<ref>).


 
 The m-faces are the only injective maps (m,n):
 
    𝖿𝖺𝖼𝖾𝗌(n, m)  ≃ Σ(f : (m,n)).(f).



  Every face gives rise to a canonical injective dimension-preserving
  morphism in the sense of <ref>, as dictated by the
  inclusion of the full subgraph that the face represents into
  n.  The fact that these are the only ones follows from
  <ref> (we cannot “swap dimensions”) and
  <ref>.


As with <ref> before, <ref> is a
result which is usually found in simplicial structures, but not in
cubical ones.  In any case, we now easily get:
  Given a morphism
  f : (m,n), there is exactly one way to write it as the
  composition f = 𝗂𝗇𝗃(f) ∘𝗌𝗎𝗋𝗃(f) of a
  surjective dimension preserving graph morphism followed by an
  injective one.  This means that the map
 
    (Σ (k : )  . (Σ (h : (k,n)). (h)) ×(Σ (g : (m,k)). (g)) ) →(m,n)
    
        (k,(h,i),(g,s)) ↦ h ∘ g

 is an equivalence.  Moreover, morphisms (m,n) are in
 1-to-1 correspondence with faces of n of dimension
 ⩽ m.


  A consequence of <ref> is that the factorisation
  on the level of sets of vertices works.  The second claim follows
  from the first: In (<ref>), the k and the
  surjective map are uniquely determined (i.e. contractible
  components) by <ref>.  By
  <ref>, injective maps correspond to faces.



  It follows from <ref> and the proof of
  <ref> that all the non-empty fibres of a
  dimension-preserving morphism between twisted cubes have the same
  size. The reverse is the case as well: a morphism between twisted
  graphs where all non-empty fibres have the same size is
  dimension-preserving.


Another consequence of the above results is that  can be
given the structure of a Reedy category
(cf. <cit.>).  Recall that a Reedy category is a
category R with a degree function d : → and
two subcategories R^+ and R^-, such that:[Degrees can
  more generally be arbitrary ordinals, but  is sufficient in our
  case.]

 
  * both subcategories are wide, i.e. contain all the objects of R;
 
  * every nonidentity morphism in R^+ raises the degree;
 
  * every nonidentity morphism in R^- lowers the degree;
 
  * and every morphism of R can be written as a morphisms in
   R^- followed by a morphism in R^+ in a unique way.

The reason why Reedy categories are interesting is that they enable
certain inductive constructions.  In the setting of type theory, they
have been discussed by Shulman <cit.>.


  The category  is a Reedy category where the degree of
  an object is the object itself (recall that objects are natural
  numbers).  ^+ is the subcategory of injective
  morphisms, and ^- is the subcategory of surjective
  morphisms.


  The first three properties are clear, and the factorisation is given
  by <ref>.


Finally, let us record an alternative representation of the category
 which does not go via graph morphisms.


  The category  has natural numbers as objects, and a
  morphism from m to n is a function n → which
  takes ⋆ at most m times as image:
 
    (m,n) Σ (f :  n →). f^-1(⋆) ⩽ m

 The identity morphisms are the functions that are constantly ⋆.
 To define the composition of f : (k,m) and
 g : (m,n), we need to define a function
 g ∘ f :  n → (which is ⋆ at most k
 times).  We define (g ∘ f)(i) by recursion on i,
 simultaneously with the values i' and b_i, as follows:
 
    (g ∘ f)(i) 
        g(i)                        if  g(i) ∈{0,1}
    
        (f(i'))  𝗑𝗈𝗋  b_i    if  g(i) = ⋆ and  f(i') ∈{0,1}
    ⋆   if  g(i) = ⋆ and  f(i') = ⋆

 where 
 
  * i' is the number of occurrences of ⋆ in the sequence
   g(0), g(1), …, g(i-1);
 
  * b_i is 1 if the number of zeros in the sequence
   (g ∘ f)(0), (g ∘ f)(1), …, (g ∘ f)(i-1) is odd,
   and 0 if it is even.
       


Note that a morphism in (m,n) can be represented as
a sequence such as 01010 of length n which
contains the symbol ⋆ at most m times, which is why we
refer to it as ternary notation.

  There is a category of
  twisted semi-cubes, denoted by ^+, which is exactly the
  same as  except that the number of ⋆ in the
  sequence must be exactly m, i.e. “⩽” is changed to
  “=” in the definition of (m,n). This category
  is equivalent to the sub-category of , denoted as
  ^+, which consists of injective
  dimension-preserving graph homomorphisms.  Note that this
  injectivity condition is equivalent to removing the reflexive edges
  from <ref>.

  If we remove the expression (𝗑𝗈𝗋  b_i) in the
  definition of morphisms of ^+, then the category becomes
  equivalent to the category of standard cubes but without
  degeneracies and swapping dimensions. In other words, the expression
  (𝗑𝗈𝗋  b_i) characterises “twisted-ness”.



  The categories , and  are isomorphic, with
  the object part being the identity.  In particular, we have:
 
    (m,n) ≃(m,n)



  As the following chain of equivalences:
  
            (m,n) 

  [<Ref>]       ≃          Σ(k : )  . (Σ(h : (k,n)). (h)) ×(Σ(g : (m,k)). (g)) 

  [<Ref>]       ≃          Σ(k : )  . (Σ(h : (k,n)). (h)) ×(k ⩽m) 

  [<Ref>]       ≃          Σ(k : )  .   𝖿𝖺𝖼𝖾𝗌(n, k) ×(k ⩽m) 

  [simplification]       ≃          Σ(f : n →). f^-1(⋆) ⩽m 

         ≡          (m,n)
 
 When transported along this isomorphism, the composition of
  gets mapped to the composition of , as
 required.




§ CONCLUSIONS AND FUTURE DIRECTIONS


We have suggested new representations of the BCH cube category and
introduced a category of twisted cubes.  It is natural to further
study the similarities and differences between standard and twisted
cube categories, and some new results will be presented in the
upcoming PhD thesis of the first author.

As future work, we plan to examine algebraic descriptions via
generators and relations.  Such presentations exist for many different
cube categories in the literature but, as far as we are aware, not for
the BCH cube category.  The closest suggestions available are the
presentations by Antolini <cit.> and
Newstead <cit.>, which seem to be fairly
easy to adapt to the BCH cube category.  Interestingly, further
adapting the generators to the twisted setting simplifies them
significantly, which mirrors the fact that morphisms between twisted
cubes cannot swap dimensions.  Moreover, our
<ref> implies that degeneracies are unique: there
is only one single way in which a twisted n-cube can be degenerated
to get a twisted (n+1)-cube.  A consequence is that we do not need
to impose relations between different degeneracies.

This, we hope, will make it possible to develop the higher categorical
structures that can be encoded as presheaves on the category of
twisted cubes.  An ultimate goal would be to model some form of
directed cubical type theory mirroring the model by Bezem,
Coquand, and Huber <cit.>.

Another possible application of our twisted cube categories might be
building a syntax for a parametric type theory or cubical type theory
without an interval as suggested by Altenkirch and
Kaposi <cit.>.  A major difficulty
in their development was the presence of multiple degeneracies, a
problem which does not occur in the current work.

A further direction which may be worth exploring is to not consider
set-valued presheaves, but type-valued presheaves instead.  To
facilitate this, we can consider the category of twisted semi-cubes
mentioned in <ref>.  From there, type-valued
presheaves can be encoded as Reedy-fibrant diagrams in a known
style <cit.>.  We can then add a condition
reminiscent of Rezk's Segal-condition <cit.> by
stating that the projection from twisted semi-cubical types to the
sequence of types along the Hamiltonian path is an equivalence.  This
corresponds to saying that the partial n-cube with missing inner
part and lid (cf. <ref>) have a contractible type of
fillers.  It seems that this could be a first step towards the
construction of composition and higher coherences, although further
conditions seem to be necessary.  The relation to the (complete)
  semi-Segal types by Capriotti and others
 <cit.> remains to
be studied.



    Acknowledgements
 We would like to thank Paolo
Capriotti and Jakob von Raumer.  Both offered many suggestions during
fruitful exchanges.  In particular, the initial observation on which
<ref> is based was suggested by them, and the idea of
considering graph morphisms was found in one of our many interesting
discussions.  The first author would like to thank his PhD supervisor,
Thorsten Altenkirch, for helpful discussions.  We are also grateful
to the participants of TYPES'19 in Oslo and the summer school on
HTT/UF in Leeds. We thank in particular Emily Riehl, Christian
Sattler, and Steve Awodey for their help and their comments.  Special
thanks go to Andreas Nuyts, who has pointed out a mistake in an
earlier draft of this paper, and to the anonymous reviewers for their
careful reading and comments.



