nLab homotopy.io

Contents

Context

Higher category theory

higher category theory

Basic concepts

Basic theorems

Applications

Models

Morphisms

Functors

Universal constructions

Extra properties and structure

1-categorical presentations

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Contents

Introduction

Overview

Screenshot of homotopy.io

This page describes homotopy.io, a web-based proof assistant for finitely-presented globular n-categories, for arbitrary nn. It is available at the following address:

It is based on the theory of associative n-categories (ANCs), which provides a strictly associative and unital model of composition. This reduces proof bureaucracy, with all the remaining weak structure in homotopies of composites, which have a direct geometrical interpretation. The proof assistant allows the user to define generators for a higher category, compose them, apply homotopies, and visualize the resulting composites as string diagrams in 2 dimensions or surface diagrams in 3 dimensions. Interaction with the proof assistant is entirely by direct manipulation using the mouse.

It can be considered a successor to the existing proof assistant Globular, which allows the construction of formal proofs in a strictly associative and unital model of 4-categories.

Homotopy construction in homotopy.io is enabled by two basic mechanisms: contraction, which makes the geometry locally more singular; and expansion, which makes the geometry locally more generic. These local moves ‘drag’ neighbouring parts of the composite, and allow the construction of nontrivial homotopies. It is an open question whether these contraction and expansion moves are capable of generating all possible homotopies in every dimension.

The image at the top-right shows a 3d surface diagram of one side of the pentagon equation (live workspace).

Contributors

The proof assistant is based on the theory of associative n-categories, which has been worked on by Christoph Dorn, Christopher Douglas, David Reutter and Jamie Vicary. The proof assistant has been implemented by Lukas Heidemann, Nick Hu and Jamie Vicary.

Overview of functionality

Using homotopy.io involves building a signature listing the types available to work with, composing them to form diagrams, and then deforming these diagrams with homotopies. The fundamental idea is that an nn-diagram corresponds to an nn-morphism in the free associative nn-category over the signature.

Signatures. In dimension 0, generating cells can be constructed by clicking the “+” symbol next to the heading “0-cells”. In dimension n+1n+1, a cell is defined by two pieces of data: its source nn-diagram, and its target nn-diagram. We add such a cell by building an nn-diagram SS, clicking ‘Source’ to choose it as the source of the new generator, then building a nn-diagram TT, and clicking ‘Target’ to choose it as the target of the new generator. The new cell will then appear in the signature. A pair of nn-diagrams S,TS,T can serve as the source and target of a new generator just when they satisfy the globularity condition, saying that their sources are the same, and their targets are the same.

Diagrams. An nn-diagram is a composite of kk-cells from the signature, for knk \leq n. To build a diagram, we first click on the thumbnail of a cell in the signature, which will display it in the central window. We can compose it with other cells by clicking near the boundary. These compositions are always whiskerings, with a kk-cell generator attached to an nn-diagram along a common min(k,n)\text{min}(k,n)-dimensional boundary. Non-whiskered composites can be obtained by first building whiskered composites, and then rewriting the interior of the diagram using homotopies. We can rewrite parts of an nn-diagram by clicking in the diagram interior, which will apply an n+1n+1-cell, or clicking and dragging, which will apply a homotopy.

Homotopies. Once a diagram has been constructed, we can modify it by applying a homotopy, which we trigger by clicking and dragging on the diagram. If this is performed on the boundary of the diagram, it will attach the homotopy to the boundary; if this is performed in the interior of the diagram, it will rewrite it.

Renderer (experimental). Diagrams can be rendered in both 2d and 3d. At the moment, only the 2d renderer is interactive, allowing diagrams to be manipulated directly using the mouse; the 3d renderer is for display only, and is currently quite buggy, only working reliably for small diagrams with a connected geometry. It is hoped that homotopy.io will soon allow rendering and smooth animation of arbitrary 3d composites.

Projection. Diagrams can be high-dimensional, and hence hard to display on a computer screen. Projection causes lower dimensions of the diagram to be ignored; for example, given a 5-dimensional diagram with projection set to 3, you will see a single (53=2)(5-3=2)-dimensional diagram, in which the vertices represent 5-cells, the wires represent 4-cells, and the regions represent 3-cells. Note that projection loses information in general.

Slice. For an nn-diagram with n>2n \gt 2, projection will always lose some information about the diagram. Slicing allows an (n+1)(n+1)-dimensional diagram to be viewed as a movie of nn-dimensional diagrams, in a way which preserves all information about the diagram. For example, for a 9-dimensional diagram with projection set to 3, there are still 6 remaining dimensions to display. With the renderer set to 2d, this leaves 4 dimensions to be handled with slice controls, which allows us to investigate the 6d displayed geometry as a movie of movies of movies of movies of 2d diagrams.

Undo and redo. Use the browser back and forward buttons to undo and redo your interactions with the proof assistant.

Server. The proof assistant has a backend that lets you log in and save proofs to the server. You can also make proofs shareable, and obtain a short URL suitable for sharing with others, or embedding in a research paper. In the future you will also be able to publish proofs, obtaining a permanent date-stamped URL.

Homotopies

A composite diagram can be deformed by clicking and dragging in its interior. If the indicated deformation would be geometrically invalid, an error message is displayed in the lower-right corner, and the diagram does not change. Otherwise, a new diagram is displayed, which is homotopic to the original diagram.

Conjecturally, homotopies can be used to construct arbitrary progressive deformations of the nn-diagram as a subcomplex of n\mathbb{R}^n. Informally, homotopies can move parts of the diagram around, but they can’t change the local neighbourhoods of the generating cells inhabiting the diagram.

Of course, the proof assistant manipulates finite combinatorial structures, and we use the word ‘homotopic’ with reference to their presumed geometrical realization. We do not make this precise here, nor has it yet been made precise in the literature; for this reason, our use of the term ‘homotopy’ is not yet well connected to the standard notion.

Every homotopy is either a contraction, which make the geometry locally more singular, or an expansion, which make it locally more generic. If we view our original diagram DD as a zigzag (see Combinatorial foundation, a contraction is encoded as a zigzag map DDD \to D', and an expansion as a zigzag map DDD' \to D, for some other diagram DD'.

Base cases

A homotopy is triggered by choosing an nn-diagram for n2n \geq 2, choosing some vertex that it contains, and dragging that vertex vertically; that is, either up or down.

If the chosen vertex is in generic position, meaning that it is the unique vertex at its height, a contraction will be triggered; otherwise, an expansion will be triggered. In the base case, a contraction decreases the height of a diagram by 1, and an expansion increases it by 1. Expansions always succeed, but contractions will only succeed if the diagram is actually locally contractible, in the sense of homotopy theory. Mathematically, contractions are performed by taking the colimit of part of the zigzag diagram (see the Combinatorial Foundation section.)

To illustrate this, we suppose we have the following diagram, where for convenience we label the vertices with numbers (live workspace):

Vertices 1 and 4 are in generic position, so dragging them will trigger contractions, while dragging vertices 2 and 3, which are in singular position, would trigger expansions. We illustrate the resulting diagrams as follows:

ExpansionExpansionContractionContraction
2 up or 3 down 2 down or 3 up 1 down 4 up

Dragging vertex 1 up, or vertex 4 down, has no effect, as vertices cannot be dragged off the top or bottom edge of a diagram.

The contractions illustrated above are unique. However, in some cases, contractions are non-unique, as illustrated here (live workspace):

Starting with the central diagram, we produce the leftmost diagram by dragging the upper vertex south-east or the lower vertex north-west, and produce the rightmost diagram by dragging the upper vertex south-west or the lower vertex north-east.

Contraction is not always possible. The following images illustrate non-contractible scenarios:

(live workspace) (live workspace)

In both of these cases, attempting to perform the contraction will give an error message. In the first case, the contraction fails because there is no canonical ordering on the rear wires; this is analogous to the nonunique contraction case given above, but here, because of the projection, we cannot give extra data to break the symmetry. In the second case, the contraction is successful at the level of the untyped diagram, but it is rejected by the type checker, since it merges two distinct generating cells, changing their neighbourhoods in a way which is not allowed by the type system.

If there are no slice controls displayed, then the homotopy is being performed at codimension 0 (that is, at the top level), and the diagram will be rewritten according to the homotopy. If every slice control shows S or T, then we are viewing a boundary of the main diagram, and the homotopy we are building will be attached to that boundary. Otherwise, we are in the interior of the diagram, working in some positive codimension, and the homotopy must now be propagated to lower codimension, using the recursive scheme detailed in the next section.

Recursive cases

When we apply a homotopy to an interior slice of the main diagram, it is propagated up to the top level. A homotopy can be either a contraction or an expansion, and we can be in a regular or singular subslice; this gives 4 cases, which we consider separately.

Combinatorial foundation

The combinatorial data stored by the proof assistant can be understood in terms of zigzags.

Definition

In a category CC, a zigzag is a finite diagram of the following sort:

A zigzag

We write Z r={r 0,,r n}Z_r = \{ r_0, \ldots, r_n \} for the set of regular slices, and Z s={s 0,,s n1}Z_s = \{ s_0, \ldots, s_{n-1} \} for the set of singular slices.

Definition

Given zigzags Z,ZZ,Z' in a category CC, a zigzag map f:ZZf:Z \to Z' comprises a monotone function f s:Z sZ sf_\text{s} : Z_\text{s} \to Z'_\text{s}, and for each iZ si \in Z_\text{s} a morphism f i:s is f s(i)f_i : s_i \to s' _{f_\text{s}(i)}, such that the diagram built as follows is commutative:

  • Take the disjoint union of ZZ and ZZ' as diagrams in CC.
  • Add the arrows f if_i between singular objects.
  • In between these arrows, add equalities between regular objects.

The idea is illustrated in the following picture:

A zigzag

Definition

Given a category CC, its zigzag category Z CZ_C has zigzags as objects, and zigzag maps as morphisms.

Definition

An untyped nn-diagram is an object of the category obtained by starting with the terminal category 11, and applying the zigzag category construction nn times.

For a signature Σ\Sigma, we write |Σ||\Sigma| for its set of generating types, which is equipped with a dimension function dim:|Σ|\text{dim}:|\Sigma| \to \mathbb{N}. We write 𝒫 Σ\mathcal{P}_\Sigma for the poset with objects given by elements of |Σ||\Sigma|, and a nonidentity morphism xyx \to y just when dim(x)<dim(y)\text{dim}(x) \lt \text{dim}(y).

Definition

A |Σ||\Sigma|-typed nn-diagram is an object of the category obtained by starting with the category 𝒫 Σ\mathcal{P}_\Sigma, and applying the zigzag category construction nn times.

Type checking and normalization

Given a |Σ||\Sigma|-typed nn-diagram DD, we can then ask if it is well-typed with respect to Σ\Sigma. This involves identifying the neighbourhoods of every point, and checking that they agree with the standard type neighbourhoods defined in Σ\Sigma. This procedure is explained in Christoph Dorn’s PhD thesis referenced below.

proof assistants:

based on plain type theory/set theory:

based on dependent type theory/homotopy type theory:

based on cubical type theory:

based on modal type theory:

based on simplicial type theory:

For monoidal category theory:

For higher category theory:

projects for formalization of mathematics with proof assistants:

Other proof assistants

Historical projects that died out:

References

Background on associative n-categories:

In relation to homotopy.io:

category: software

Last revised on December 20, 2023 at 23:18:38. See the history of this page for a list of all contributions to it.