We use type-theoretic techniques to present an algebraic theory of ∞-categories with strict units. Starting with a known type-theoretic presentation of fully weak ∞-categories, in which terms denote valid operations, we extend the theory with a non-trivial definitional equality. This forces some operations to coincide strictly in any model, yielding the strict unit behaviour.

The theory of associative n-categories has recently been proposed as a strictly associative and unital approach to higher category theory. As a foundation for a proof assistant, this is potentially attractive, since it has the potential to allow simple formal proofs of complex high-dimensional algebraic phenomena. However, the theory relies on an implicit term normalisation procedure to recognize correct composites, with no recursive method available for computing it.

A combinatorial theory of associative n-categories has recently been proposed, with strictly associative and unital composition in all dimensions, and the weak structure arising as a notion of `homotopy' with a natural geometrical interpretation. Such a theory has the potential to serve as an attractive foundation for a computer proof assistant for higher category theory, since it allows composites to be uniquely described, and relieves proofs from the bureaucracy of associators, unitors and their coherence. However, this basic theory lacks a high-level way to construct homotopies, which would be intractable to build directly in complex situations; it is not therefore immediately amenable to implementation. We tackle this problem by describing a `contraction' operation, which algorithmically constructs complex homotopies that reduce the lengths of composite terms. This contraction procedure allows building of nontrivial proofs by repeatedly contracting subterms, and also allows the contraction of those proofs themselves, yielding in some cases single-step witnesses for complex homotopies. We prove correctness of this procedure by showing that it lifts connected colimits from a base category to a category of zigzags, a procedure which is then iterated to yield a contraction mechanism in any dimension. We also present homotopy.io, an online proof assistant that implements the theory of associative n-categories, and use it to construct a range of examples that illustrate this new contraction mechanism.

We give a mathematical analysis of a new type of classical computer network architecture, intended as a model of a new technology that has recently been proposed in industry. Our approach is based on groubits, generalizations of classical bits based on groupoids. This network architecture allows the direct execution of a number of protocols that are usually associated with quantum networks, including teleportation, dense coding and secure key distribution.

To any complex Hadamard matrix we associate a quantum permutation group. The correspondence is not one-to-one, but the quantum group encapsulates a number of subtle properties of the matrix. We investigate various aspects of the construction: compatibility to product operations, characterization of matrices which give usual groups, explicit computations for small matrices.