10.6092/issn.1972-5787/5010
We formalise, in Coq, the opening sections of Parity Complexes [Street1991] up to and including the all important excision of extremals algorithm. Parity complexes describe the essential combinatorial structure exhibited by simplexes, cubes and globes, that enable the construction of free omega categories on such objects. The excision of extremals is a recursive algorithm that presents every cell in such a category as a composite of atomic cells, this is the sense in which the omega category is free. Due to the complicated multi-dimensional nature of this work, the detail of definitions and proofs can be hard to follow and verify. Indeed, some corrections [Street1994] were required some years following the original publication.Our formalisation verifies that all cases of each result operate as stated. In particular, we indicate which portions of the theory can be proved directly from definitions, and which require more subtle and complex arguments. By identifying results that require the most complicated proofs, we are able to investigate where this theory might benefit from further study and which results need to be considered most carefully in future work.
application/pdf
1972-5787
5010
1
en
Mitchell Buckley
Journal of Formalized Reasoning
excision of extremals
A formal verification of the theory of parity complexes
Text.Serial.Journal
https://jfr.unibo.it/
8
Articles
2015-11-05
2015-04-08
2015-01-26
2019-11-05
25-48
JFR
Mitchell Buckley
2015/11/05
10.6092/issn.1972-5787/5010
25
Macquarie University
1972-5787
1
excision of extremals
en
48
Dominic Verity. Complicial sets characterising the simplicial nerves of strict ω-categories. Mem. Amer. Math. Soc., 193(905):xvi+184, 2008.
A formal verification of the theory of parity complexes
https://jfr.unibo.it/article/download/5010/5282
8
Formalizing parity complexes
Mitchell Buckley


We formalise, in Coq, the opening sections of Parity Complexes [9] up to and including the
all important excision of extremals algorithm. Parity complexes describe the essential combina-
torial structure exhibited by simplexes, cubes and globes, that enable the construction of free
ω -categories on such objects. The excision of extremals is a recursive algorithm that presents
every cell in such a category as a (unique) composite of atomic cells. This is the sense in which
the ω -category is (freely) generated from its atoms. Due to the complicated multi-dimensional
nature of this work, the detail of denitions and proofs can be hard to follow and verify. Indeed,
some corrections were required some years following the original publication [10]. Our formal-
isation veries that all cases of each result operate as stated. In particular, we indicate which
portions of the theory can be proved directly from denitions, and which require more subtle and
complex arguments. By identifying results that require the most complicated proofs, we are able
to investigate where this theory might benet from further study and which results need to be
considered most carefully in future work.




1. INTRODUCTION
An n-simplex ∆n is a geometric gure that generalises the notion of triangle or
tetrahedron to n-dimensional space. Simplexes have a number of properties that
make them useful in algebraic topology, algebraic geometry and homotopy theory
where they often play a foundational role. Each n-simplex can be oriented in such
a way that it forms an n-category. We include below the cases for n = 1, 2 and 3.
                                                       G•                :/ •
                                  ?•
                   /•                                               
            •                                                      *4                (1)
                                          /
                           •                  •                           $/ 
                                                  •                                •
At low dimensions, it is not hard make each of these into an n-category. At higher
dimensions, say n > 3, it is quite hard to describe the n-category structure because
the source and target of each cell are large pasting diagrams in high dimensions.
   Beginning in the late 1970's Ross Street, together with John Roberts and Jack
Duskin, began investigating how this process could be rigorously extended to any
n. This was achieved in [8] where the process was described for the simplexes and
the corresponding categories were dubbed the orientals (referring to the fact that
they are oriented). The main motivation at this time stemmed from non-abelian
cohomology where various constructions rely on the orientals.
   At the same time, Iain Aitcheson was developing a similar series of results for
n-cubes: that each cube could be given an orientation in such a way that it forms an
n-category or even an ω -category [1]. A third example of this phenomenon is found
in n-globes where the corresponding n-categories have a very simple description.
For more on the usefulness of simplexes and cubes, see Street's survey [11].
   Following these successes, the goal was then to describe the general structure
of all oriented multi-dimensional structures for which it is possible to extract free
                                       Journal of Formalized Reasoning Vol. 8, No. 1, 2015, Pages 2548.
26     ·     Mitchell Buckley

ω -categories in the style of these three examples. The early 1990's yielded a number
of related solutions. Ross Street dened a structure called a parity complex and
gave an explicit description of the ω -category associated to each parity complex [9].
Some minor corrections were added in [10]. Richard Steiner contributed directed
complexes as a generalisation of directed graph. He showed that loop-free directed
complexes generated free ω -categories in the appropriate way [6]. Both of these
authors also showed that their respective structures were closed under product and
join and covered the three main examples of simplexes, cubes, and globes. Around
the same period Mike Johnson was working on a formal description of pasting
scheme for ω-categories [3, 4], and was able to describe the free ω-category on such
structures. He included the simplexes as his primary example, and there is a strong
sense in which this addressed the same problem. Further related work can be found
in [2, 7] and also in [12] where a conjecture of StreetRoberts is proved in the closing
chapter.
   Our interest centres on Parity Complexes which takes a particularly `hands-on'
approach and describes the combinatorics of this construction in full detail. Our
goal is to encode and verify the opening sections of the article up to the excision of
extremals algorithm. The theory shows how to build, for any parity complex C an
ω -category O(C). The excision of extremals algorithm shows that each cell can be
presented as a (unique) composite of atomic cells; this is the sense in which O(C)
is (freely) generated from the atoms. The algorithm can also be used to generate
explicit algebraic descriptions of the cells in O(C).
   Our motivation is two-fold. First, some of the combinatorial arguments in Street's
text can be dicult to follow and can easily conceal errors; this is illustrated by the
fact that corrections were later required. We will provide some conrmation that
the corrections have addressed all issues. Second, a computer-veried encoding
provides a good resource for understanding the intricacies of these complicated
structures and opens a path to further renements of the material. We have not
attempted to formalized the entirety of the theory. The essential combinatorics are
contained in sections 1 to 4 and culminate in the excision of extremals algorithm
which is the nal result that we encode.
   From this point on we often refer to [9] as `the original text', and to [10] as `the
corrigenda'. The content extracted directly from the original article is numbered
consecutively with the original name included parentheses. Sections within this
article are referred to as `Section n' and those of the original text are referred to as
`n' or `Section n of [9]'.
   We programmed everything in Coq [5] and the code is freely available for inspec-
tion at the following location.
      https://github.com/MitchellBuckley/Parity-Complexes
  In Section 2 we outline the foundational mathematics that needs to be introduced
for an encoding of parity complexes. We also outline how we chose to implement
this foundation. In Sections 3 to 7 we outline the main combinatorial content of [9]
section by section. At each stage we comment on the intuition underlying each result
and discuss our implementation of the denitions and results. We pay particular
attention to those parts of the material that were dicult to translate into Coq.
Though our encoding focuses on 1 to 4, we do comment on some material in
Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
                                                              Parity complexes        ·     27

5. In Section 8 we outline the few lessons we have learned in computer-veried
encoding of mathematics. Section 9 contains concluding remarks.

2. REQUIRED FOUNDATIONS
Parity complexes are described using basic set theory and partially ordered sets.
In particular, we must implement:
 •   sets;
 •   set union, set intersection, set dierence, etc.;
 •   nite sets;
 •   cardinality of nite sets;
 •   partial orders; and
 •   segments of partial orders.
Many of these structures are already encoded in dierent parts of the Coq standard
library but for various reasons we have chosen to reimplement much of that material.
2.1 Sets
We implemented sets using the Ensembles standard library. This involves a universe
type U : Type on which all our sets will be based. Then a set is an Ensemble : an
indexed proposition U → Prop. An element of the universe x : U is a member of a
set A : U → Prop when the corresponding proposition A x is true. Inclusion of sets
relies on logical implication.
Definition Ensemble := U → Prop .
Definition In ( A: Ensemble ) (x: U) : Prop := A x.
Definition Included (B C: Ensemble ) : Prop :=
  forall x:U , In B x → In C x.
Set operations union, intersection, and set dierence are all implemented using
point-wise logical operations:
Union A B        := fun x = > (A x ∨ B x)
Intersection A B := fun x => ( A x ∧ B x)
Setminus A B     := fun x => (A x ∧ ¬ (B x))
For the purposes of this section we suppose that we always work with a xed
universe U.
  The Coq language has a convenient feature that allows us to introduce notation
for these operations.
Notation    "x   ∈  B"       :=   ( In A x) ( at level 71) .
Notation    "A   ⊆  B"       :=   ( Included A B) ( at level 71) .
Notation    "A   ∪  B"       :=   ( Union A B ) ( at level 61) .
Notation    "A   ∩  B"       :=   ( Intersection A B) ( at level 61) .
Notation    "A   '\ ' B"     :=   ( Setminus A B ) ( at level 61) .
Each special symbol is introduced as a utf-8 character which Coq has no problem
recognising. This feature makes the code much more readable.
2.2 Finiteness and cardinality
Finiteness is implemented using the same basic idea as the Finite_sets standard
library. This library contains an inductively dened proposition Finite stating that
                                           Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
28     ·     Mitchell Buckley

a set S is nite when S = ∅, or S = {x} ∪ S 0 where S 0 is nite and x 6∈ S 0 . Cardi-
nality is implemented in a similar way: there is an inductively dened proposition
cardinal stating that a set S has cardinality 0 when it is empty and has cardinality
n + 1 when S = {x} ∪ S 0 , x 6∈ S 0 , and S 0 has cardinality n.
Inductive Finite : Ensemble U → Prop :=
  | Empty_is_finite : Finite ( Empty_set U)
  | Union_is_finite :
      forall A: Ensemble U ,
        Finite A → forall x :U , ¬ In U A x →
          Finite ( Add U A x).

Inductive cardinal : Ensemble U → nat → Prop :=
  | card_empty : cardinal ( Empty_set U) 0
  | card_add :
      forall (A: Ensemble U) (n: nat ) ,
        cardinal A n → forall x :U , ¬ In U A x →
          cardinal ( Add U A x) ( S n).

  Cardinality and niteness are related by the result forall S, (Finite S <-> exists
n, cardinal S n). When our universe has decidable equality we can show that nite-
ness interacts well with set operations, for example forall A B, Finite A ∧ Finite
B → Finite (A ∪ B). When our universe does not have decidable equality, there are
some classical results that may not hold for all nite sets. For example ¬¬S = S
and S ⊆ T → T = (T \ S) ∪ S . We don't know exactly how the theory will change
if this avenue is explored. Since most types of interest have decidable equality, we
are not worried about including this as an assumption in our formalisation.
   Note that the denitions we have given here are those contained in the standard
library while our implementation is slightly dierent; the dierences are explained
in Section 2.4 below.
2.3 Partial orders
Some material on partial orders is available in the Relations standard library. Our
particular requirements for orders were slightly more complicated than that library
allowed for and we found it simpler to explicitly prove basic results as they were
needed.
2.4 Equality of sets
We say that two sets S and T are equal when they are equal as terms of the type
Ensemble U; that is, they are equal as indexed propositions and forall x, S x = T x.
We write S = T to indicate that S and T are equal. This is the standard notion
that is built into Coq and allows us to replace S with T in any expression.
  There is another notion of equality: we say that S and T are the same when
they contain the same elements. This is the usual notion of set equality used in
mathematics. Equivalently, two sets are the same when they are equivalent as
indexed propositions ( forall x, S x ↔ T x), or when S ⊆ T and T ⊆ S. We write
Same_set S T or S == T to indicate that S and T are the same.
  If two sets are equal then they are certainly the same but two sets can be the
same without being equal. For example, the sets fun x => x = 0 and fun x => 1 +
x = x in Ensemble nat are the same but not equal. The standard library Ensembles
Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
                                                            Parity complexes        ·     29

contains an extensionality axiom stating that forall A B, A == B → A = B. In order
to keep our formalisation as constructive as possible we are careful never to use the
axiom in our formalisation.
   The standard facilities of Coq will allow for rewriting S with T whenever S is
equal to T . However, when S is the same as T we do not have any guarantee that
such rewrites are legitimate. In this situation, our type of sets Ensemble U becomes
a setoid : a set equipped with an equivalence relation. Then S == T implies that we
may rewrite S for T in any expression which is built up of operations that preserve
the equivalence relation. This rewrite facility is provided by the standard library
Setoid and requires us to prove that Same_set is an equivalence relation and that
the appropriate set operations preserve the equivalence.
   Without the extensionality axiom it is not possible to prove that Finite S and
S == T implies Finite T. Consider the usual inductive denition of Finite given
on page 28. By examining the constructors we can see that the proposition holds
for sets of the form Emptyset, Add Emptyset x, and Add (Add Emptyset x) y etc. It
is easy to describe sets that are nite, but not equal to sets of this kind. Take
fun n => (n < 2), or fun n => (S n = 0); while these sets are the same as Add (Add
Emptyset 0) 1 and Emptyset they are not equal to those sets, and thus not nite
under the usual denition. Something similar happens with the denition of nite
cardinality. This problem can be solved in more than one way. We chose to solve
this by adding a third constructor for Finite that explicitly introduces the property
that Finite S ∧ S == T → Finite T. This modication allows us to recover this basic
property of nite sets without the extensionality axiom.

2.5 More on niteness
In many cases we augmented the standard library with extra results about nite sets
that were not already present. We found that setting up this basic theory was often
tedious, but occasionally an enjoyable exercise in constructive mathematics. For
instance, it became clear at some point that certain basic results about sets could
not be proved without supposing that equality in U is decidable, i.e. forall (a b :
U), (a=b) ∨ ¬(a=b). Since none of the examples used here or in the literature need
a universe U without decidable equality, we have made this a further assumption
in our implementation.
   If one wanted to reason about, say sets of integer sequences, then the obvious
universes to use would be nat− > Int or StreamInt each of which lacks decidable
equality. In that case one would nd that various simple results concerning nite
sets would not hold.


We have now covered the essential mathematical foundations required for a formal-
isation of parity complexes. More details can be found by examining the code itself.
In the following three sections we summarise 1 to 4 of Parity Complexes together
with modications given in the corrigenda. This content is sucient to express the
excision of extremals algorithm (Theorem 22). As we progress through the mate-
rial we will reproduce denitions and terminology almost verbatim from [9, 10]. In
each case we will explain the underlying intuition of the material, comment on our
implementation, and indicate where our formalisation shed light on the underlying
                                         Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
30     ·     Mitchell Buckley

arguments. We also discuss some aspects of the nal sections (5 and 6) of [9] though
none of that material was been formalised.

3. DEFINITIONS AND THE SIMPLEX EXAMPLE
We begin by summarising the content of Section 1 of [9].
Denition 1 A parity complex is a graded set
                                                      ∞
                                                      X
                                              C=            Cn                        (2)
                                                      n=0

together with, for each x ∈ Cn+1 two disjoint, non-empty, nite sets x+ , x− ⊆ Cn
subject to Axioms 1, 2, 3A and 3B which appear below.
   From this point onward we will work exclusively within a single parity complex
C as described above. When we say S ⊆ C we mean that S is a subset of the
underlying graded set of the parity complex. When we say x ∈ C we mean that x
is an element of the underlying graded set of the parity complex.
   Before we list the axioms we will introduce some terminology. If x ∈ C then
elements of x− are called negative faces of x, and those of x+ are called positive
faces of x. We will sometimes refer to x− and x+ as face-sets of x. Given S ⊆ C ,
let S − denote the set of elements of C which occur as negative faces of some x ∈ S ,
and similarly for S + ; thus
                                [                    [
                          S− =     w− and S + =          w+ .                    (3)
                                      w∈S                            w∈S

Each subset S ⊆ C is graded via Sn = S ∩ Cn . The n-skeleton of S ⊆ C is dened
by
                                                       n
                                                       X
                                              S n :=          Sk .                    (4)
                                                       k=0
Call S n-dimensional when it is equal to its n-skeleton.
   The broad intuition is to see this structure as a generalisation of directed graph.
Elements of C0 are vertices, elements of C1 are directed edges, elements of C2 are
directed `faces', elements of C3 are directed `volumes', and so on. The usual notion
of source and target are replaced by face-sets x− and x+ . The following is a basic
example of this structure of dimension two.
                                      /•               /•      /•
                              ?•                       ?
                                                               
                        /•                                                     /•
               •                                            0•                        (5)
                                                              A            ?•
                                                 #
                                                                    / •
                                      •
Notice that elements above dimension 1 can have more than one source-face or
target-face.
  Without the axioms below, this structure is very general indeed and many un-
usual examples can be provided. When the axioms are applied, possible examples
Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
                                                                    Parity complexes        ·     31

become much better behaved. Examples of arbitrary dimension can be constructed
from simplexes, cubes, and other kinds of polytopes as seen below. Of course, the
simplexes provide the main motivation for understanding these kinds of structures.
   So far we have described the data of a parity complex: a graded set with a pair of
face-set maps (−)− , (−)+ : Cn+1 → P(Cn ). We now describe the required axioms.
Axiom 1 For all x ∈ C ,
                                   x++ ∪ x−− = x−+ ∪ x+−
where x++ = (x+ )+ etc.
This is a kind of globularity condition that ensures various face-sets are appropri-
ately related. The following diagram is an example where x ∈ C2 and both x− and
x+ have four elements.
                               8 ◦      / ◦      / ◦
                                                          &
                       \
                       ◦                     x             8 •                  (6)
                                &        / •\     / •\
                                  •\

Edges marked with a dotted line belong to x− , the other edges belong to x+ .
Vertices marked with a • belong to x++ , those marked with a ◦ belong to x−− ,
those marked with a       belong to x−+ , and those marked with a \ belong to x+− .
In particular, this axiom implies that x++ ⊆ x−+ ∪ x+− , that is, positive faces of
positive faces must be the negative face of a positive face, or the positive face of a
negative face.
   Notice that in both (5) and (6) the set of source (target) faces have all elements
aligned in a common direction and they do not branch apart. This behaviour is
guaranteed by introducing Axiom 2 below.
   Suppose that S and T are subsets of C . We write S ⊥ T when S − ∩ T − =
S ∩ T + = ∅. This extends to elements by x ⊥ y when x− ∩ y − = x+ ∩ y + = ∅ ∗ .
  +

A subset S ⊆ C is called well-formed when S0 has at most one element, and, for
all x, y ∈ Sn (n > 0), if x 6= y then x ⊥ y . Broadly speaking, a set is well-formed
when its elements do not form any branchings like
                   •                            8•       /•
                        x                                A
                           &                                     &
                             8•   or     •          x
                                                             y    8• ,            (7)
                        y                       &          
                   •                              •          •
and it contains at most one element of dimension 0. In each of the diagrams above
we can observe that {x, y} is not well-formed, while {x}, {y}, x+ , x− , y + , and y −
are all well-formed. This diagram depicts branchings in dimensions 1 and 2, but
well-formedness prevents branching in all dimensions. The condition on dimension
zero does not force parity complexes to have a single element of dimension zero, but
that (using the axiom below) elements of dimension 1 have a single source vertex
and a single target vertex.

∗ This   could equivalently be dened for elements rst and then extended to sets afterwards.

                                                 Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
32     ·     Mitchell Buckley

Axiom 2 For all x ∈ C , x− and x+ are well-formed.
If we think of the union x− ∪x+ as forming a boundary of x as in (6) above then this
axiom ensures that the boundary looks something like the boundary of a polytope.
For those familiar with higher categories, this condition ensures that the face-sets
look like valid pasting diagrams.
   Suppose that x, y ∈ C . We write x < y whenever x+ ∩ y − is non-empty. That is,
when x and y abut by having a common element in their respective sets of positive
and negative faces. This implies x 6= y since x− and x+ are always disjoint. We
then let  be the reexive transitive closure of <. An example is
                                                   '
                               •         ⇓x        6•
                                         (6 •      ⇓y        (6 •

                                      6•                    ⇓              (6 •            (8)
                        •              ⇓                   (6 •
                                      (•                                   (•
                                                           ⇓z              7
where x < y and y  z . In this case we often say that there is a path from x to z .
For all S ⊆ C we let S denote the reexive transitive closure of < restricted to S .
When x S z we often say there is a path from x to z in S .
  While Axioms 1 and 2 can be seen as imposing some of the basic structural
behaviour of graphs, the following axiom restricts us to certain `loop-free' graphs.
Axiom 3 For all x, y ∈ C ,
    A. x  y  x implies x = y.
    B. if x  y then ∀z ∈ C , ¬(x ∈ z + ∧ y ∈ z − ) and ¬(y ∈ z + ∧ x ∈ z − ).
Axiom 3A says that  is anti-symmetric, or, that there are no paths that loop within
a xed dimension. Axiom 3B says that there are no paths that cross between the
face-sets of any element z . That is, we avoid circumstances where a path can cross
from one face-set to the other face-set of an element z as in the diagram below.
                                 8•       /•      /•
                                  x
                                                                                      &
                              •                       z                              8•   (9)
                                           &
                                               •           /•     /   •
                                                                                  y


  These are all the axioms for a parity complex. The following examples come from
p.318319 of [9].
Example 1 A 1-dimensional parity complex is precisely a directed graph with no
circuits.
Example 2 The ω-glob is the parity complex G dened by Gn = {(, n) :  =
   or ⊕}, and (, n + 1)− = {( , n)} and (, n + 1)+ = {(⊕, n)}. Elements of
dimension 0, 1, and 2 are `n-discs'. There are precisely two elements at each di-


Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
                                                                                           Parity complexes                                        ·    33

mension, each of which has exactly one source face and exactly one target face.
                                                                                                      1

                                                           1

                                                                                                                                
                    ⊕1
                         / ⊕0                                   ⊕                                     *4 ⊕2
                                                                                                     ⊕3
                                                                                                                                ⊕                      (10)
                0                        0                ⊕2
                                                                A 0             0                2
                                                                                                                                C 0
                                                   ⊕1                                                    ~
                                                                                                     ⊕1

We use n and ⊕n as short-hand for ( , n) and (⊕, n).
Example 3 The ω-simplex is the parity complex ∆ described as follows. Let
∆n denote the set of (n + 1)-element subsets of the set of natural numbers N =
{0, 1, 2, . . . }. Each x ∈ ∆n is written as (x0 , x1 , . . . , xn ) where x0 < x1 < · · · < xn .
Let xδi denote the set obtained from x by deleting xi . Take x− to be {xδi : i odd}
and x+ to be {xδi : i even}. Elements of dimension 0, 1, and 2 are `n-simplexes'.
                                                                                                                         /: 2
                                                                                G1               12
                                  @1                                            012                                 123
                             01              12                                                                   
      0
          01   /1                     012                                01         02
                                                                                           0123*4
                                                                                                          13                    23                     (11)
                                                   
                         0                         /2
                                  02                                                          
                                                                                          023 013
                                                                                                                                      $/ 
                                                                      0                          03                                          3
We use abcd as short-hand for (a, b, c, d) and similarly at other dimensions.
Example 4 The ω-cube is the parity complex Q described as follows. The elements
are innite sequences of the three symbols , , ⊕ containing a nite number of
  's and ending with an innite string of 's. The dimension of an element is the
number of 's appearing in it. Let xδi− denote the sequence obtained from x by
replacing the i-th by when i is odd and by ⊕ when i is even. Similarly, xδi−
is dened by interchanging and ⊕ in the previous sentence. For x ∈ Qn , dene
x = {xδi : 1 < i < n}. The n-cube is the parity complex built the same way but
using only lists of length n (and that are not required to end with an innite string
of 's). The n-cubes of dimension 1, 2, and 3 are displayed below.
                                                                                                                                             /•
                                                                                           ? •O                                              ? O
                                                                                                 ⇓        ⊕

                                                                                                                         ⇒ ⊕
                                  ⊕
                                             ⊕
                                                       / ⊕⊕                •O                                            /•
                                  O                       O                                                               O
                                                                                                               7G
                    /⊕                        #                ⊕
                                                                               ⇒
                                                                                                                                ⇓⊕                     (12)
                                                       /⊕                                                                                    /•
                                                                                     ⇓
                                                                                           ?•                                                ?
                                                                                                      ⇒

                                                                           •                                             /•
Some labels have been omitted from the last diagram in order to keep it readable.
Remark 3.1 It might seem unusual to insist that elements of the ω-cube end with
an innite string of 's. If we omit this condition then the parity complex would
                                                                Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
34        ·        Mitchell Buckley

not contain any (nite) paths from      . . . to ⊕ ⊕ . . . and so it would become
somewhat disconnected. The underlying type for our implementation would also
become undecidable. We have not investigated the implications of this distinction.
  Before continuing our exposition of 1 we will comment briey on our implemen-
tation.
Implementation 3.2 The basic data for a parity complex without the axioms is
sometimes called a pre-parity complex. We chose to implement this concept rst,
as there are many trivial results about preparity complexes that we will later use. A
preparity complex is implemented as the following data:
C : Type
dim : C → nat
plus : C → Ensemble C
minus : C → Ensemble C
This data is technically dierent from our description above, but the essential struc-
ture is identical. There is a collection of objects C , each member of which has a
dimension and two face-sets† . A few axioms are introduced to ensure that face-sets
are nite, non-empty, and disjoint, and that they interact with dimension correctly.
forall        (x   y   : C) ,   x ∈ ( plus y) → dim y = dim x + 1
forall        (x   y   : C) ,   x ∈ ( minus y ) → dim y = dim x + 1
forall        (x   :   C) ,     Finite ( plus x)
forall        (x   :   C) ,     Finite ( minus x)
forall        (x   :   C) ,     dim x > 0 → Inhabited ( plus x)
forall        (x   :   C) ,     dim x > 0 → Inhabited ( minus x)
forall        (x   :   C) ,     dim x = 0 → plus x == Empty_set
forall        (x   :   C) ,     dim x = 0 → minus x == Empty_set
forall        (x   :   C) ,     Disjoint ( plus x ) ( minus x)

   These are given meaningful names such as plus_Finite, plus_dim, and plus_Inhabited.
Fundamental denitions for sets such as Sn and S n are also given and some trivial
statements are also proved here. For example,
Definition sub (R : Ensemble C) ( n : nat ) : Ensemble C
 := fun (x : C) => (x ∈ R ∧ ( dim x) = n ).

Lemma sub_Union :
 forall T R n ,
  sub ( T ∪ R) n == ( sub T n) ∪ ( sub R n).
More complicated denitions like well-formedness are also given and more powerful
(though almost trivial) results are also proved here. For example,
† In   the actual code the type C is called carrier.




Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
                                                               Parity complexes     ·     35


Definition well_formed (X : Ensemble C) : Prop :=
 ( forall (x y : C ) , x ∈ X ∧ y ∈ X
    → dim x = O → dim y = 0
    → x = y)
 ∧
 ( forall (x y : C ) , x ∈ X ∧ y ∈ X
     → ( forall (n : nat ) , dim x = S n → dim y = S n
     → ¬ ( perp x y) → x = y)) .

Lemma well_formed_by_dimension :
 forall X ,
  well_formed X <-> forall n , well_formed ( sub X n).
All other basic denitions and trivial results are encoded in a similar fashion.
  We now look at some basic properties of parity complexes.
  Given S ⊆ C , let S ∓ denote the set of negative faces of elements of S which are
not positive faces of any element of S , and similarly for S ± ; thus
                       S∓ = S− \ S+     and S ± = S + \ S − .
This extends to individual elements by x± := {x}± and x∓ := {x}∓ . These sets
capture the notion of purely positive and purely negative faces of an element x or
set S .
  The following propositions follow from Axioms 1, 2 and 3.
Proposition 2 (Proposition 1.1) For all x ∈ C ,
                           x++ ∩ x−− = x−+ ∩ x+− = ∅                                    (13)

                             x−∓ = x+∓ = x−− ∩ x+−                                      (14)

                             x−± = x+± = x−+ ∩ x++         .                            (15)
   Proposition 2 contains identities that one would expect from a polytope-like
structure and are much like Axiom 1. The meaning is reasonably clear when the
various face-sets are highlighted in an example like (6) above.
Proposition 3 (Proposition 1.2) For all u, v, x ∈ C , u  v and v ∈ x+ imply
                             u− ∩ x−+ = ∅ .                               (16)
   Proposition 3 indicates that if u branches out from the source of x then a path
from u to v can not end in the target of x. This is a consequence of Axiom 3B and
has three duals obtained by reversing the roles of u and v and reversing the roles
of x− and x+ . Proposition 3 and its duals are together equivalent to Axiom 3B.
   The following observation describes a convenient technical property of well-formed
sets.
Observation 4 (page 322 in [9]) For all T, Z ⊆ C , if T ∪ Z is well-formed and
T ∩ Z = ∅, then T ⊥ Z .
  We say a set R ⊆ C is tight when, for all u, v ∈ C , u  v and v ∈ R implies
u− ∩ R± is empty. This condition prevents a path from starting in R± and ending
in R. The following two results are required for somewhat technical reasons.
                                         Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
36     ·     Mitchell Buckley

Denition 5 Suppose that R, T ⊆ C . We say that R is a segment of T when for
all x, y, z ∈ T , x, z ∈ R and x  y  z implies y ∈ R.
Proposition 6 (Proposition 1.4) For all R, S ⊆ C , if R is tight, S is well-
formed, and R ⊆ S , then R is a segment of S .
Observation 7 (page 359 in [10]) For all x ∈ C , x+ and x− are tight.
  This concludes our exposition of 1. We have seen that the content of this section
could be implemented with very little deviation from the original text.
Remark 3.3 The notion of tightness was introduced in the Corrigenda [10]. It
appears to be entirely necessary, but we do not understand the full signicance of
the concept.
Implementation 3.4 Each axiom and proposition is readily encoded, for example
Axiom axiom1 :
 forall (x : C) ,
  ( Plus ( plus x)) ∪ ( Minus ( minus x)) ==
  ( Plus ( minus x)) ∪ ( Minus ( plus x)) .

Lemma Prop_1_2 :
 forall u v x ,
  triangle u v →
   v ∈ ( plus x ) →
    ( minus u ) ∩ ( Plus ( minus x)) == Empty_set .
We were able to prove each result from basic denitions and axioms. This is ex-
actly as described in the original work. The proof of Proposition 6 makes use of
Propositions 2 and 3.
   When we look ahead we nd that axioms 1 and 2 are used frequently throughout
the material. Axiom 3A is only used to prove that S is decidable and that nite
non-empty sets S have minimal and maximal elements under S . Axiom 3B is
used only to prove Propositions 2 and 3 and some disjointness conditions in the
proof of Lemma 17.
Remark 3.5 (Adjusting the axioms) In private conversation Christopher Nguyen
pointed out that Axiom 3B is only used to prove Proposition 2, and Proposition 3
and its duals. We have commented already that Proposition 3 and its duals are
equivalent to Axiom 3B. A quick examination of our code then reveals that Proposi-
tion 3 is only used to prove that x+ is tight and the disjointness condition described
on p327. We haven't investigated this in any detail, but it might be possible to
replace Axiom 3B with something slightly weaker (or stronger) but which has the
same implications in the relevant proofs. This is of particular use in light of the fact
that Axiom 3B is not always preserved under products and joins (see the remark on
page 334 of [9]).
4. MOVEMENT
In Section 2 of [9] the concept of movement is introduced. It is a concept that is
fundamental to describing cells in n-categories generated from parity complexes.
For three sets S, M, P ⊆ C , we say that S moves M to P , or M −
                                                                 S
                                                                 → P , when
                     M = (P ∪ S − ) \ S +       and P = (M ∪ S + ) \ S − .       (17)
Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
                                                                                                           Parity complexes        ·    37

Here are some examples of movement at dimensions 2 and 1:
                                                                 m
                                                                                      '
                                     9•                  ⇓s                           8•
                             m                                                                     m
       m    /•    m    /•                                &                                                 %    m   /•   m    /•
   •   p          p
                                     ⇓s                  8•                           ⇓s                   9•   p        p             (18)
                             p       %                                                &            p
                                         •               ⇓s                               7•
                                                                 p

                                                                 s
                                                                                  '
                                 s
                                         7•          s                   s
                                                                                  7•           s
        s   /•     s    /•                                   '                                         '        s   /•   s    /p
  m                                              s
                                                                 7•          s
                                                                                                       7•                              (19)
                                 s       '                                        '            s
                                             •                                        7•
                                                                 s

where lowercase labels m, p, s indicate which set each component belongs to (unla-
belled elements do not belong to M , P , or S ). This condition guarantees that the
face-sets of S , M and P are related in the basic way we would expect of pasting
diagrams in n-categories. The movement condition is intended to describe the basic
combinatorial shape of cells in our yet-to-be-dened ω -category. When those cells
are dened we will need to add basic niteness and well-formedness conditions to
ensure that various pathogical examples of movement are excluded.
  It is helpful to recognise that movement is a condition that applies dimension-by-
                             S                                                   Sn+1
dimension, that is, M −→ P if and only if Mn −−−→ Pn for all n. This not only aids
in various proofs, but it indicates there is nothing complicated happening across
dimensions.
Proposition 8 (Proposition 2.1) For all S, M ⊆ C , there exists                                                          P ⊆ C         with
  → P if and only if
   S
M−
                      S ∓ ⊆ M and M ∩ S + = ∅ .                                                                                        (20)
  Proposition 8 illuminates a fundamental meaning of movement: that M contains
the purely negative faces of S and none of the positive faces. This is illustrated
below where elements of S2∓ are indicated by squiggly arrows and those of S2+ are
indicated by dashed arrows.
                                                                 m
                                                                                      '
                                     9•                  ⇓s                           8•
                             m                                                                     m
       m    /•    m    /•                                &                                                 %    m   /•   m    /•
   •   p          p
                                     ⇓s                  8•                           ⇓s                   9•   p        p             (21)
                             p       %                                                &            p
                                         •               ⇓s                               7•
                                                                 p

Observe that     S2∓
                  ⊆ M1 and M1 ∩     = ∅ as indicated by the proposition. Propo-
                                                 S2+
sition 8 has a dual where M and P play opposite roles.
                                                                      Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
38       ·    Mitchell Buckley

Proposition 9 (Proposition 2.2) Suppose S, M, P, X, Y ⊆ C , M −→
                                                               S
                                                                 P and
X ⊆ M has S ∩ X = ∅. If Y ∩ S = ∅, and Y ∩ S = ∅, then (M ∪Y )∩¬X −
             ∓                +                −                    S
                                                                    →
(P ∪Y )∩¬X .
Proposition 9 indicates that some elements of M and P can be added or removed
without disturbing the movement condition. The conditions on X and Y indicate
that they are disjoint from the faces of S in a suitable way. Sets X and Y should
be thought of as sets that are added to or removed from the movement as below.
                                                               m
                                                                               &
                                 m
                                          8•                   s                   8•          m
             x    /•   x    /•                             &                                         &            y
                                                                                                                       /•   y
                                                                                                                                 /•
         •                                    s            8•                          s             8•                                    (22)
                                     p    &                                        &           p
                                              •                s               8•
                                                               p


Proposition 10 (Proposition 2.3) Suppose M, P, Q, S, T                                                                ⊆ C   where M −→
                                                                                                                                     S
                                                                                                                                       P
and P −→
       T
         Q. If S − ∩ T + = ∅ then M −−−→ Q.
                                     S∪T


  Proposition 10 describes the condition under which movements can be `composed'
or `pasted' together. The following diagram depicts an example. Elements of sets
M, S, P, T, Q are labelled with the corresponding lower-case letters.
                                                       m
                                                                   &
                            m
                                     8•                s               8•              m
         m   /•   m    /•                          &                                       &
     •   p
         q
                  p
                  q
                                     s             8•                      s               8•             m
                             p
                                 &                                     &
                                                                                       p                 p
                                                                                                              &                            (23)
                            q
                                     •                 s               9•                      t              9•
                                                                                                                       m
                                                                                                                       p    /•   m
                                                                                                                                 p    /•
                                                                                                                       q         q
                                               p               p
                                              q    %                                       %             q
                                                       •                   t               8•
                                                                           q


Proposition 11 (Proposition 2.4) Suppose M                                                         T ∪Z
                                                                                               −−−→ P                 with Z ± ⊆ P . If T ⊥
Z then there exists N such that M −  → P.
                                  T  Z
                                  →N −
  Proposition 11 describes a condition under which movement can be decomposed.
In particular, if T ∪ Z is well-formed then T ⊥ Z as required in the proposition.
Implementation 4.1 The denition of movement and the propositions above are
readily encoded. For example:




Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
                                                             Parity complexes        ·        39


Definition moves_def (S M P : Ensemble C) : Prop :=
  P == (( M ∪ ( Plus S)) ∩ ( Complement ( Minus S)))
  ∧
  M == (( P ∪ ( Minus S )) ∩ ( Complement ( Plus S))) .

Notation " S ' moves ' M 'to ' P " := ( moves_def S M P) ( at level
    89) .

Lemma Prop_2_3 : forall (S M P T Q : Ensemble C) ,
  S moves M to P →
  T moves P to Q →
  ( Disjoint ( Minus S ) ( Plus T )) →
     (S ∪ T) moves M to Q.
The Notation command in Coq allows us to use the statement S moves M to P in
place of the somewhat awkward moves_def S M P.
  It did not take long to verify that the proofs in this section proceed precisely as
indicated in the original text.
  Proposition 8 is proved by appealing to denitions and basic manipulation of sets.
Propositions 9 to 11 are proved using Proposition 8 and basic manipulation of sets.
Propositions 8 and 11 have duals that are not displayed here but are required later;
they are implemented separately in our code. It is worth noting that none of these
results require axioms 1, 2 or 3. In our implementation, we prove these results
before the axioms are even introduced.
  This concludes our exposition of 2. Again, the content of this section was
implemented with very little deviation from the original text.

5. THE ω -CATEGORY OF A PARITY COMPLEX
Having described the basic properties of parity complexes and the more advanced
notion of movement, Section 3 of [9] describes the cells of an ω -category O(C)
associated with any parity complex C .
Denition 12 A cell of a parity complex C is a pair (M, P ) of non-empty, well-
formed, nite, subsets of C with the property that M and P both move M to P .
If this is interpreted dimension by dimension, we get the following picture at di-
mension 2,
                                             m
                                                    '
                               8•      m⇓p          8•
                           m                                 m
        m   /•   m    /•                 &                       &    m    /•    m       /p
   m    p        p
                               m⇓p       8•       m⇓p            8•   p          p
                           p   &                    &        p
                                   •   m⇓p              7•
                                             p
                                                                            (24)
where lowercase labels m, p, s indicate which set the elements belong to. Notice
that M1 and P1 are neither equal nor disjoint, but each move M0 to P0 . Notice
also that M2 = P2 . This kind of behaviour is uniform through all dimensions.
Notice also that, aside from the movement condition, we only require that M and
                                         Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
40     ·     Mitchell Buckley

P be non-empty, well-formed and nite. Call (M, P ) an n-cell when M ∪ P is
n-dimensional. In this case we have Mn = Pn as above.
Denition 13 The           n-source   and n-target of a pair of sets (M, P ) are dened by
                           sn (M, P ) = (M n−1 ∪ Mn , P n−1 ∪ Mn )                    (25)
and
                            tn (M, P ) = (M n−1 ∪ Pn , P n−1 ∪ Pn )   .               (26)
If (M, P ) is a cell we can show that sn (M, P ) and tn (M, P ) are also cells, and
that they are n-dimensional. Notice that (M, P ), sn (M, P ) and tn (M, P ) contain
exactly the same elements in dimension n − 1 and below. We encourage the reader
to consider the 1-source and 1-target of the cell depicted in (24).
Denition 14 A pair of cells (M, P ), (N, Q) are           n-composable   when
                                      tn (M, P ) = sn (N, Q)   ,                      (27)
in which case their n-composite is
                (N, Q) ∗n (M, P ) := (M ∪ (N ∩ ¬Nn ), (P ∩ ¬Pn ) ∪ Q)         .       (28)
Notice that (27) implies that the two cells agree from dimensions 0 to n − 1 and
that Pn = Nn at dimension n. The resulting composite is almost exactly the pair-
wise union of (M, P ) and (N, Q); the set-dierence ensures correct behaviour at
dimension n. It is not surprising that some form of set-dierence is required since
most forms of composition will forget the point of contact: A → B → C composes
to A → C .
  For any parity complex C , let O(C) be the set of cells of C . We will see later
(Theorem 19) that O(C) is an ω -category. Before this can be achieved, we need to
establish some basic properties of cells.
Denition 15 A set S ⊆ C is receptive when for all x ∈ C ,
        if x−+ ∩ x++ ⊆ S and S ∩ x−− = ∅ then S ∩ x+− = ∅
and
        if x+− ∩ x−− ⊆ S and S ∩ x++ = ∅ then S ∩ x−+ = ∅ .
A cell is receptive when it is receptive at every dimension.
Remark 5.1 The notion of receptivity is somehow important, we nd later that
all cells are receptive and it is a necessary condition for some central results. It
appears to be entirely necessary, but we do not have an intuitive understanding of
its meaning.
                                                                          +
Lemma 16 (Lemma 3.1) For all                 M, P ⊆ C , x ∈ C ,    if M −x−→ P and M is
                       −
receptive then M −x−→ P .
Lemma 16 is proved using denitions, basic manipulation of sets and Propositions 2
and 8. It has a dual which we implement in our code. We will nd later that since
all cells are receptive, it is not hard to nd receptive subsets M of C . In fact, it is a
bit dicult to illustrate why receptivity is even required because the most obvious
Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
                                                                                             Parity complexes    ·    41

examples of x, M, P satisfying the movement condition above are also part of a cell
structure.
Lemma 17 (Lemma 3.2) Suppose m, n ∈ N, all cells are receptive and (M, P )
is an n-cell. Suppose also that X ⊆ Cn+1 , |X| = m and X is well-formed with
X ± ⊆ Mn . Put Y = (Mn ∪ X − ) ∩ ¬X + , then:
      B. (M n−1 ∪ Y, P n−1 ∪ Y ) is a cell and and X − ∩ Mn = ∅.
      C. (M n−1 ∪ Y ∪ X, P ∪ X) is a cell.
Lemma 17 originally contained a part A which was removed in [10]. Lemma 17C
indicates that, if X is a well-formed set of dimension n + 1, (M, P ) is an n-cell, and
X abuts (M, P ) in the sense that X ± ⊆ Mn , then we can form an (n+1)-cell whose
top-dimension elements are those of X and whose target is (M, P ). The source of
this cell has Y at its top dimension. The following diagram is labelled to illustrate
this scenario.
                                                               y
                                                                       $
                                           y       <•      ⇓x          <•           y
                      my
                            /•   my
                                      /•                   "                            "    my
                                                                                                  /•   my
                                                                                                            /•
                  •    p          p
                                               ⇓x          <•         ⇓x                <•    p         p
                                                                                                                     (29)
                                               m                                m
                                           p       "                   "            p
                                                       •   ⇓x
                                                               m
                                                                           :•
                                                               p

There is a dual lemma obtained by reversing the direction of X in the diagram
above.
  This kind of result does not seem unusual, but it is surprisingly hard to prove
(see Implementation 5.3 below). The proof itself is done in three steps. To quickly
summarise:
(1) Lemma 17B implies Lemma 17C. The proof is somewhat direct and proceeds
    as indicated in the original paper.
(2) Lemma 17B with m = 1 implies Lemma 17B in general. This is done by
    induction on m and follows from basic denitions and axioms.
(3) Lemma 17B holds for m = 1. This is done by induction on n and the argument
    relies on Proposition 18. The construction works as indicated, though it is not
    a short argument. There are particular disjointness conditions that must be
    established (p327 of [9]) and require their own special argument.
Proposition 18 (Proposition 3.3) For all n ∈ N, all n-cells in C are receptive.
This is a somewhat technical result, it is not immediately clear to us how the notion
of receptivity ts naturally into the combinatorics. The proof of this result relies
on Lemma 17B.
Theorem 19 (Theorem 3.6) If C is any parity complex then O(C) is an ω-
category. Furthermore, if (M, P ), (N, Q) are n-composable cells‡ then (Mk ∪Pk )− ∩
(Nk ∪ Qk )+ = ∅ for all k > n.

‡ t (M, P )   = sn (N, Q)
   n

                                                               Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
42     ·     Mitchell Buckley

   Theorem 19 is a central result in [9] since it achieves one of the main goals of the
paper. In order to implement Theorem 19 we would need to implement a notion of
ω -category which is not trivial. Since there is little question that this result holds,
and it is not required to prove Theorem 22, we have chosen not to implement it.
We similarly omit Propositions 3.4 and 3.5 which are preliminary results leading
up to Theorem 19.
Remark 5.2 Perceptive readers will have noticed that Lemma 17B and Proposi-
tion 18 seem to logically rely on one another. At rst glance this appears to be a
circular argument and therefore unsound. However, if we look closely we can see
that each result proceeds by induction and that the two proofs can be woven together
to produce a proof of both results simultaneously. Proposition 18 is restated as: for
all n, every n-dimensional cell (M, P ) is receptive. The two results are proved by
mutual induction on n, the dimension of (M, P ). Included in that argument is an
induction on m = |X|. The following statements hold and are enough to show that
both results hold for all n and m.
   i. Lemma 17B holds when m = 1 and n = 0.
  ii. For a xed n, if Lemma 17B holds when m = 1 then it holds when m > 1 (by
      induction on m).
iii. Proposition 18 holds when n = 0.
 iv. If Lemma 17B and Proposition 18 hold for n = k, then Lemma 17B holds for
      n = k + 1 and m = 1.
   v. If Lemma 17B holds for n = k + 1 and Proposition 18 holds for n = k, then
      Proposition 18 holds for n = k + 1.
This understanding is not explicit in [9].
Implementation 5.3 As in earlier sections, the denitions and statement of re-
sults are readily encoded. The main diculty arises in encoding the proofs.
    The proofs of Lemma 17 and Proposition 18 are by far the most dicult part
of the entire project and consumed most of our programming eort. Consider the
components of the proof given above. Each of the components follow the argument
provided by Street in his paper. However the disjointness condition in (iv) has a
dual, and (i), (ii), and (iv) each have duals. Finally, we needed to uncover the
logical dependence that allows us to weave these things together to produce a non-
cyclic argument.
    It is worth noting that the original proof of Proposition 18 uses an argument
about skeletons of parity complexes (treating separate parity complexes as objects
of the argument). We have translated the argument so that it is internal to any
given parity complex. The combinatorial logic of our argument is exactly the same
as Street's, we have only adjusted the setting slightly.
Remark 5.4 (Understanding receptivity and tightness) This section of [9]
is harder to follow than the others and the proofs here are not straight-forward.
In particular, the notions of tightness and receptivity are both a bit opaque and
Lemma 17 is very hard to prove. This provides some motivation to closely re-
examine the result and see whether alternative arguments might be made to prove
it.
Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
                                                                                   Parity complexes   ·    43

  This concludes our exposition of 3. In formalizing this section we have seen
some of the most complicated arguments made in the original text and seen that
Lemma 17 (Lemma 3.2) is not easy to prove.

6. FREENESS OF THE ω -CATEGORY
Having built the ω -category O(C) from a parity complex C , we now prove that it
is generated from atoms. The following content comes from 4.
   In any parity complex C we expect that any individual element x of dimension p
is the top element of some cell whose lower-dimensional structure can be computed
by examining the face-sets of x and recursively taking face-sets of face-sets. This is
made explicit in the following denition.
Denition 20 For each             x ∈ Cp ,        two subsets µ(x), π(x) ⊆ C p are dened induc-
tively as follows
                        µ(x)p = {x}       and µ(x)k−1 = µ(x)∓
                                                            k, 1≤k≤p

                               and π(x)k−1 = π(x)±
                        π(x)p = {x}              k, 1≤k≤p
The pair (µ(x), π(x)) is denoted by hxi.
  Take the following diagram for example. If x ∈ C has dimension 2 and has
boundary as illustrated in below then hxi = ({x, p, q, r, a}, {x, s, t, e})
                                                        q
                                                                 /b
                                                   @c
                                          p                           r
                                                            x                                            (30)
                                      a            /d                     /   e
                                              s                  t

A priori, we have no guarantee that such a pair is actually a cell.
Denition 21 An element x ∈ Cp is called relevant when hxi is a cell. This
amounts to saying that µ(x)n and π(x)n are well-formed for 0 ≤ n < p − 1, and
                            µ(x)n−1 = π(x)∓
                                          n,                     π(x)n−1 = µ(x)±
                                                                               n

for 0 < n < p − 1. Call a cell (M, P ) an atom when it is equal to hxi for some
x ∈ C . In that case we say that (M, P ) is atomic.
  In all of our main examples, every hxi is a cell (all elements are relevant).
Theorem 22 (Theorem 4.1: excision of extremals) Suppose that µ(x) is tight
for all x ∈ C . Suppose (M, P ) is an n-cell and u ∈ Mn (= Pn ) is such that
(M, P ) 6= hui . Then (M, P ) can be decomposed as
                    



                                    (M, P ) = (N, Q) ∗m (L, R)                                            (31)
where m < n, and (N, Q) and (L, R) are n-cells of dimension greater than m.
This is another central result of the paper. If this algorithm is applied recursively
then it shows how to present an arbitrary n-cell as a composite of atoms. Thus
O(C) is not only an ω -category, but it is generated from its atoms
  The algorithm takes an n-cell (M, P ) and runs as follows.
§ Alternatively,   let (M, P ) be a non-atomic n-cell.
                                                        Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
44     ·      Mitchell Buckley

(1) Find the largest m < n with (Mm+1 , Pm+1 ) 6= (µ(u)m+1 , π(u)m+1 ). This
    amounts to discovering the highest dimension at which the criterion for being
    atomic does not hold¶ . In this case, there exists w ∈ Mm+1 ∩ Pm+1 .
(2) We want to decompose our cell by pulling o a cell of dimension m + 1. Let x
    be a minimal element of Mm+1 less than w, and let y be a maximal element of
    Mm+1 greater than w.
(3) At least one of x or y must belong to Mm+1 ∩ Pm+1 . This relies on the fact
    that µ(u)m+1 is a segment of Mm+1 , which itself relies on µ(u)m+1 being tight.
(4) If x ∈ Mm+1 ∩ Pm+1 then we get a decomposition of (M, P ) as
                   N = M m ∪ {x}            Q = P m−1 ∪ ((Mm ∪ x+ ) ∩ ¬x− ) ∪ {x}              (32)

                        L = ((M ∩ ¬{x}) ∪ x+ ) ∩ ¬x−                  R = P ∩ ¬{x}             (33)
     Notice that (N, Q) is an (m + 1)-cell whose single element at top dimension is
     x, and (L, R) is the n-cell obtained by cutting x out of (M, P ).
                                                       m
                                                             '
                                        8•        m⇓p        8•
                                  m                                     m
            x      /•    m   /•                    &                         &    m   /•   m   /•
       •    mp           p
                                      m⇓p          8•      m⇓p               8•   p        p
                                  p     &                    &           p
                                            •     m⇓p            7•
                                                       p
                                                                                               (34)
(5) If y ∈ Mm+1 ∩ Pm+1 then we get a decomposition of (M, P ) as
                        N = M ∩ ¬{y}            Q = ((P ∩ ¬{y}) ∪ y − ) ∩ ¬y +                 (35)

                    L = M m−1 ∪ ((Pm ∪ y − ) ∩ ¬y + ) ∪ {y}              R = P m ∪ {y}         (36)
     This is dual to the case for x. Notice that (L, R) is an (m + 1)-cell whose single
     element at top dimension is y , and (N, Q) is the cell obtained by cutting y out
     of (M, P ).
   The two hardest parts of this algorithm are parts (3) and (4). In part (3) we must
show that either x or y belong to Mm+1 ∩Pm+1 . This relies on the fact that µ(x)m+1
is a segment of Mm+1 , but this follows from Proposition 11 and the assumption
that each µ(x) is tight. In part (4) we need to show that (N, Q) and (L, R) are well-
dened cells. The various conditions of niteness and well-formedness follow quite
directly. The diculty comes in showing that the movement conditions hold. We
investigate the cells dimension by dimension and nd that the movement conditions
can be proved using Proposition 11 and Lemma 17.
   How do we know that this algorithm terminates? The original text denes the
rank of an n-cell (M, P ) to be the cardinality of M ∪ P . The algorithm produces
two cells of smaller rank, so therefore must terminate. It is also possible to dene

¶ Alternatively,   nd the largest m < n with Mm+1 ∩ Pm+1 6= ∅.

Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
                                                                   Parity complexes    ·     45

the rank by
                                                n
                                                X
                                rank(M, P ) =         |Mk ∩ Pk |                           (37)
                                                k=0

In this case every n-cell has a rank of at least 1 since Mn ∩ Pn is non-empty. A cell
of rank 1 must be atomic. A cell of rank k > 1 can be decomposed using excision
of extremals into two cells whose individual ranks are less than or equal to k − 1.
Again, this is sucient to guarantee termination.
Implementation 6.1 As already indicated, Theorem 22 is readily proved using the
argument given above.
Remark 6.2 In order to show that O(C) is freely generated from its atoms we
must show that there are no equalities among composites of cells that are not a
consequence of the ω-category axioms. This is achieved in Street's Theorem 4.2 but
has not been reproduced here and we have not included it in our formalisation.
Remark 6.3 Many of these theorems and lemmas come with a condition concern-
ing tightness and receptivity of various sets. We can show that these conditions are
satised by appealing to various other results. At the end of the day there may be
some confusion about which conditions are ultimately required. To summarise, if a
parity complex C has the property that µ(x) is tight for every x ∈ C , then all of the
theorems up to this point will hold.
  At this stage, we have not shown that every hxi is a cell. In fact, we have no
guarantee that any cells exist at all. This is something of a loose end, it is accounted
for in the following section.
  This concludes our exposition of 4. As already mentioned, the central theorem
Theorem 22 (Theorem 4.1) is readily proved using the content of previous sections.

7. PRODUCT AND JOIN
Though we have not formalised Section 5 of [9], some of the content is relevant to
our investigation. In 5 Street describes, for any two parity complexes C and D,
their product C × D and their join C • D. This section also describes two kinds
of duals for parity complexes obtained by reversing the roles of (−)+ and (−)− in
all dimensions or in odd dimensions only. This is of particular interest since the
diagrams involved in descent are products of globes with simplexes; this is explored
in 6.
   This section also addresses some issues that are, as yet, unresolved. First, we
don't know that any elements are relevant (consequently we don't know if any cells
exist at all). Second, Lemma 17 relies on the fact that all µ(x) are tight, and this
was never established.
   Consider the following stronger forms of Axioms 1 and 2.
                   For all x,
                   (R1)     µ(x)− ∪ π(x)+ = µ(x)+ ∪ π(x)− and
                            µ(x)− ∩ π(x)+ = µ(x)+ ∩ π(x)− = ∅
                   (R2)     µ(x) and π(x) are well formed.
                                            Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
46     ·     Mitchell Buckley

These axioms hold for ∆, G , and Q.
Remark 7.1 If a parity complex C satises these axioms then every hxi is a cell
(every x is relevant). Thus all elements of ∆, G , and Q are relevant.
  This solves the rst problem in the primary examples of interest. Now what
about tightness of µ(x)?
  In a parity complex C , write x ≺ y when either y ∈ x+ or x ∈ y − . Let J denote
the reexive transitive closure of the relation ≺. Notice that x < y means there
exists z ∈ x+ ∩ y − , so this implies x ≺ y . Hence, x  y implies x J y . Where the
rst ordering  describes paths in a xed dimension, this new ordering J zig-zags
up and down with ≺ to describe paths across multiple dimensions. We introduce
the following as an optional axiom.
                                (AS)       J is anti-symmetric.                    (38)
This axiom holds in ∆, G , and Q where J is also total.
Proposition 23 (Proposition 5.2) If each x is relevant and (AS) holds then
each µ(x) is tight. Thus, every µ(x) in ∆, G , and Q are tight.
   This solves the second problem in the primary examples. Unfortunately we nd
that there are examples of parity complexes where J is not antisymmetric (p337
of [9]). These are small pasting diagrams that are explicitly illustrated in the article
and are quite elementary. These stronger conditions do not appear to be unreason-
able, but it is not clear what classes of examples are exluded as a consequence.
Remark 7.2 To summarise again, if a parity complex C satises (R1), (R2) and
(AS) then every theorem and proposition covered here will work. In particular,
every theorem and proposition holds for the parity complexes ∆, G , and Q.
Remark 7.3 Theorem 22 relies on the fact that each µ(x) is tight and therefore a
segment in the required place. This is readily proved when (R1), (R2) and (AS) are
used, but we would like to use the excision of extremals more generally if possible.
So we ask, is the tightness condition strictly necessary? Or, is there another way
to ensure that µ(x) is a segment in that proof? We do not yet know.
Remark 7.4 There seems to be a fundamental relationship between parity com-
plexes and `directed graphs of multiple dimension'. Note that this notion of higher-
dimensional graph would not be the same as an n-graph since each component of an
n-graph has a single source and single target rather than a source set and a target
set. Some of the axioms for parity complexes are just those of this `graph' structure
and others restrict us to graphs of a certain kind. Axioms (R1), (R2) and (AS)
place further restrictions. Since we are mainly interested in examples that satisfy
all of these conditions, we do not need to worry too much about this narrowing of
our focus. More generally though, it would be good to know which of these condi-
tions are associated with the graph structure of parity complexes, and which of the
conditions allow for the (free) ω-category construction. This could be the focus of
some future research.
  This concludes our exposition of 5. We will not discuss Section 6 of [9] and our
exposition of the original text ends here.
Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
                                                            Parity complexes        ·     47

8. SOME LESSONS IN CODED MATHEMATICS
8.1 Duals
We were often forced to prove dual results where x+ and x− were interchanged, or
                                          S
where the direction of a movement M −     → P was reversed. In these cases we were
forced to explicitly restate and reprove the result, even though the underlying logic
had not changed whatsoever. It would have been better if, from the beginning, we
had encoded plus and minus as duals to each other, then the theorems would dualise
automatically. One way to do this is to dene faceset : bool → C → Ensemble C
and then set minus := faceset false and plus := faceset true. From this starting
point it should be easy to combine dual results into one.

8.2 Notation
Coq has a Notation facility which allows the user to introduce custom notation for
specic expressions. We used this to make set operations easier to read and write.
For example, an expression such as Union A B is displayed as A ∪ B, and similarly
for intersection, inclusion, etc. This made our code much easier to read.

8.3 Tactics
Coq has a tactic language which allows for partial automation of proofs. The
language allows the user to describe simple proof strategies that can be automat-
ically applied when little innovative thinking is required. A particular built-in
tactic called intuition will automatically deal with simple proofs that require
only knowledge of rst-order logic. We used the tactic language to describe a
proof tactic called basic that automatically applied further logical steps such as
(x ∈ A ∩ B) → (x ∈ A ∧ x ∈ B). In many cases this vastly simplied proofs by
applying repeat (basic; intuition) to automatically prove some trivial facts.
   More expert use of this system would surely result in more elegant and readable
proofs.

8.4 Axiom of extensionality for sets
We chose to remove the axiom of extensionality because we wanted to deal with
sets in a completely constructive fashion. This was a choice of style. In many ways,
retaining the axiom would not have weakened our encoding and we would not have
needed to implement setoid rewrite for ensembles.

8.5 Compiling the excision of extremals algorithm
Our choice to implement sets using ensembles has made it impossible to directly
compile an executable version of the excision of extremals. This is unfortunate:
we have proved that such an algorithm can run but we can't actually compile or
run it without further coding. The mathematical signicance of our work is not
undermined, but better planning would have yielded executable code as a pleasant
side-eect.

9. CONCLUSION
We have formalised Ross Street's Parity Complexes up to the excision of extremals
algorithm in 4. In particular, 1 and 2 together with Theorem 22 are proved as
                                         Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
48     ·     Mitchell Buckley

indicated in the original text. Section 3 is also formalised with the same essential
arguments as [9], but with many additional dual theorems, and a technical but
meaningful change to the logical ow of Lemma 17 and Proposition 18.
  We have indicated where the material is most eective at capturing the di-
cult combinatorics, and where future work might make improvements. We have
explicitly outlined the logical dependence of the central results.

References
 [1] Iain R. Aitchison. The geometry of oriented cubes. Macquarie University
     Research Report No: 86-0082, 1986.
 [2] Fahd Ali Al-Agl and Richard Steiner. Nerves of multiple categories. Proc.
     London Math. Soc. (3), 66(1):92128, 1993.
 [3] Michael Johnson. Pasting diagrams in n-categories with applications to co-
     herence theorems and categories of paths. PhD thesis, University of Sydney,
     1988.
 [4] Michael Johnson. The combinatorics of n-categorical pasting. J. Pure Appl.
     Algebra, 62(3):211225, 1989.
 [5] The Coq development team. The Coq proof assistant reference manual (v8.4),
     2014.
 [6] Richard Steiner. The algebra of directed complexes. Appl. Categ. Structures,
     1(3):247284, 1993.
 [7] Richard Steiner. Omega-categories and chain complexes. Homology Homotopy
     Appl., 6(1):175200, 2004.
 [8] Ross Street. The algebra of oriented simplexes. Journal of Pure and Applied
     Algebra, 49(3):283335, 1987.
 [9] Ross Street. Parity complexes. Cahiers de Topologie et Géométrie Diérentielle
     Catégoriques, 32(4):315343, 1991.
[10] Ross Street. Parity complexes: Corrigenda. Cahiers de Topologie et Géométrie
     Diérentielle Catégoriques, 35(4):359361, 1994.
[11] Ross Street. Higher categories, strings, cubes and simplex equations. Appl.
     Categ. Structures, 3(1):2977, 1995.
[12] Dominic Verity. Complicial sets characterising the simplicial nerves of strict
     ω -categories. Mem. Amer. Math. Soc., 193(905):xvi+184, 2008.




Journal of Formalized Reasoning Vol. 8, No. 1, 2015.
