On this website, I organize my thoughts on a variety of topics at a granular level. Sometimes these thoughts are self-contained, and at times I may organize them into larger notebooks or lecture notes. My nascent ideas about the design of tools for mathematical thought are here. I welcome collaboration on any of the topics represented in my forest. To navigate my forest, press Ctrl-K.
I am accumulating an understanding of constructive domain theory — that is, the domain theory that can be carried out in an elementary topos with a natural numbers object. These notes are based on the work of Tom de Jong and Martín Escardó; these notes, however, assume the propositional resizing principle whereas de Jong and Escardó explore a predicative version domain theory based on large and locally small domains.
In this section, we gather some useful definitions and results concerning creation of (co)limits. The reason for stating these things explicitly is that the usual definitions of created (co)limits are deeply irrational in a variety of incompatible ways, so it is important to fix definitions that can work from the start. It would be good to reformulate this in terms of displayed categories of algebras.
Let
We aim to understand sufficient conditions for a forgetful functor to create colimits. As we will show below, it is sufficient for these colimits to be preserved the the monad.
Let
By assumption,
We must show that the map
To show that
We must check that the the following multiplication square commutes:
By assumption, we know that
We compute algebraically, using the algebra property of
Hence we may define a
Let
Let
In particular, we must factor any cocone
We must check that
To see that
through the cocone
First we must check that the following diagram commutes:
This holds immediately from the homomorphism property of
Second, we must check that the following diagram commutes:
This follows from the factorization
Let
Let
A dcpo is called pointed when it has a bottom element
A dcpo
Suppose that
Conversely, suppose that
A pointed dcpo carries a (unique)
The algebra structure is unique if it exists because
We define the structure map
The unit law for the algebra is trivial. The multiplication law is verified as follows:
Let
To define the bottom element of
Let
It is clear that a homomorphism of algebras must preserve the bottom element. On the other hand, suppose that
Because both composites preserve the bottom element, it is enough to observe that they both take
The category of
Having a bottom element and being an algebra are both properties of dcpos, because these structures are uniquely determined. Therefore, we will argue that pointed dcpos with bottom-preserving morphisms form the same subcategory of
To finish, we recall that a morphism of dcpos preserves algebra structure if and only if it preserves the bottom element.
By virtue of the monadicity result, we will refer to pointed dcpos and
We will deduce the closure of
For any dcpo
We fix another lax square of the following form:
We must show that there exists a unique morphism
We will define
For uniqueness, suppose that we have two morphisms
Let
Let
Using the universal property of
First we define
Next we define
To arrange
Thus we have the desired lax square and a unique morphism
Our goal is to show that we may choose the universal map
Using the universal property of the co-comma squares for each
We must check that the outer triangle below commutes:
Rewriting using the strictness of lifted morphisms, this amounts to the established fact that
We must check that the outer triangle below commutes:
Rewriting with established equations, it suffices to observe that the outer diagram below commutes:
Finally, we must check that any two morphisms
Let
This follows from the following facts:
The Eilenberg–Moore category
This is the first part of Corollary 2 of Linton's Coequalizers in categories of algebras.
The coproduct of lift-algebras is computed as a reflexive coequalizer, whose existence we have already established. Given an index set
The Eilenberg–Moore category
These notes were prepared by Jonathan Sterling, based in part on discussions with Martín Escardó and Tom de Jong. Any errors belong to Jonathan Sterling.
An element
(This is adapted from Johnstone’s definition of positive elements of frames to the case of dcpos by Tom de Jong.)
The bottom element
Suppose that
Let
Fixing semidirected
Let
Let
Let
This follows from the closure of positive elements in an algebra under directed suprema.
Let
Let
The positive elements of a lifted dcpo
Let
Conversely, suppose that
Let
Therefore, we first suppose that any
Conversely, if
It follows from our characterization of positivity in terms of partial elements that an element
(See also Proposition 6.2.12 of Tom de Jong’s thesis.)
So far we have studied positivity as an order-theoretic property of domains; in this section, we explore a non-order-theoretic generalization of this condition that is applicable in the setting of axiomatic domain theory. This notion is inspired by the alternative characterization positivity in terms of partial elements.
Let
When
Under these circumstances, we refer to
Let
We shall write
Let
Let
Let
We first observe that the latter condition is equivalent to the following:
For anyu \in LA , ifa \sqsubseteq \bigsqcup _{p: u{ \downarrow }}u[p] thenu{ \downarrow }= \top .
This follows from the (constructive) characterization of the path order in dcpos. Therefore, our result follows from our earlier characterization of positive elements of a pointed dcpo in terms of partial elements.
In a lifted dcpo
We say that a pointed dcpo
Let
An element
Let
We must check that
In a pointed dcpo, any non-bottom element is non-negatively generated.
Hence, any element
The bottom element is clearly non-negatively generated, as it lies beneath any element. Now fix
When a pointed dcpo
(2) implies (1) by setting
Let
Let
Let
Let
Let
It suffices to recall that a lifted dcpo is positively generated.
We describe some light conditions under which a continuous dcpo is positively generated.
Let
We must show that for any
As
Let
We observe that every element of
Let
As positive generation implies non-negative generation for an element of a pointed dcpo, we may conclude that
I am not sure how useful the following construction is. On the other hand, maybe it has a universal property at the level of posets.
Let
Let
In classical mathematics, every
Let
The mapping defined above is continuous because we have assumed that
Let
We fix
For the deflation, we fix
Let
First, we recall that the embedding-projection pair
Because
A pointed dcpo
This follows from two existing lemmas:
This document records what I have learned about the design of “tools for mathematical thought” over the past couple years. One of my goals in writing this is to set out both the unique requirements of an information data model that is needed to record and facilitate mathematical thought, as well as the technical requirements for tools that can be used for mathematics.
A “tool for mathematical thought” could be many things, but it must be a tool for the development and interlinking of mathematical ideas in a way that facilitates authoring, publishing, teaching, learning, and the maintenance of evergreen notes.
A tool for mathematical thought could be a piece of software, or it could be an organizing principle for physical notes on paper. In these notes, we will primarily explore the design of computerized tools for mathematical thought.
The existing tools for mathematical thought can be divided into two main categories: interactive proof assistants and textual authoring and publishing tools (including LaTeX, as well as the Gerby software that runs the Stacks Project).
The phrase evergreen note is due to Andy Matuschak, who has written extensively about it in his public Zettelkasten. Evergreen notes are permanent notes that evolve and accumulate over time, cutting across different projects.
One of the design principles for evergreen notes described by Matuschak is atomicity (Evergreen notes should be atomic): a note should capture just one thing, and if possible, all of that thing. A related point is that it should be possible to understand a note by (1) reading it, and (2) traversing the notes that it links to and recursively understanding those notes.
Traditional mathematical notes do not achieve this kind of atomicity: understanding the meaning of a particular node (e.g. a theorem or definition) usually requires understanding everything that came (textually) before it. In the context of the hierarchical organization of evergreen mathematical notes, this would translate to needing to go upward in the hierarchy in order to understand the meaning of a leaf node. I regard this property of traditional mathematical notes as a defect: we should prefer explicit context over implicit context.
High-quality mathematical notes should make sense without context; hierarchical context is imposed in order to tell a story, but consumers of mathematical notes should not be forced into a particular narrative. Indeed, as many different hierarchical structures can be imposed, many different narratives can be explored.
My first exploration of hypertext mathematics was the lecture notes on relative category theory; in hindsight, these lecture notes are very much traditional lecture notes, not written with the atomicity principle in mind. As a result, it is often difficult to understand a given node without ascending upward in the hierarchy.
Atomicity in evergreen mathematical notes is enhanced by adhering to the following principles:
It can be a bit excessive to link every word: but the pertinent links could be added to a “related pages” section.
Matuschak describes a number of organizing principles for evergreen notes, which are quite compelling; one design principle (Prefer associative ontologies to hierarchical taxonomies) deserves additional discussion in the context of mathematical thought. In particular, the problem of circular reference must be grappled with immediately rather than incidentally: in ordinary knowledge management, circularity represents the completion of a train of thought, whereas in mathematical thinking it remains very important to distinguish assumptions from consequences.
Hence a purely associative organization of mathematical knowledge is not viable (although it often happens by accident), and so the hierarchical organization of mathematics must be taken seriously from the start. We find that Matuschak has in fact already grappled with the need for hierarchy in his note It’s hard to navigate to unlinked “neighbors” in associative note systems, where he discusses the difficulty of traversing the “neighbor”-relationship between notes that are related by another note’s context, but are not related on their own. Matuschak proposes to solve the problem by grafting hierarchy onto the associative ontology after the fact through “outline notes”:
“Outline notes” can create pseudo-hierarchies with order and structure by linking to many child notes. Then we need the UI to support navigating between neighbors “through” these outline notes.
The viewpoint of outline hierarchy as a structure imposed on the existing associative ontology is a convenient organizing principle for evergreen notes in the sense of Matuschak, but it is a necessary principle for the design of tools for mathematical thought.
Multiple hierarchical structures can be imposed on the same associative network of nodes; a hierarchical structure amounts to a “narrative” that contextualizes a given subgraph of the network. One example could be the construction of lecture notes; another example could be a homework sheet; a further example could be a book chapter or scientific article. Although these may draw from the same body of definitions, theorems, examples, and exercises, these objects are contextualized within a different narrative, often toward fundamentally different ends.
As a result, any interface for navigating the neighbor-relation in hierarchically organized notes would need to take account of the multiplicity of parent nodes. Most hypertext tools assume that the position of a node in the hierarchy is unique, and therefore have a single “next/previous” navigation interface; we must investigate the design of interfaces that surface all parent/neighbor relations.
It is easy to make the mistake of prematurely imposing a complex hierarchical structure on a network of notes, which leads to excessive refactoring. Hierarchy should be used sparingly, and its strength is for the large-scale organization of ideas. The best structure to impose on a network of many small related ideas is a relatively flat one. I believe that this is one of the mistakes made in the writing of the foundations of relative category theory, whose hierarchical nesting was too complex and quite beholden to my experience with pre-hypertext media.
There are many ways to model hierarchy, but there are two salient orthogonal distinctions in the different designs.
Both HTML and LaTeX support a form of hierarchical organization with “absolute” heading levels, i.e. levels that count upward from a single root. In HTML, there is <h1>
, <h2>
, <h3>
..., and in LaTeX there is \part
, \chapter
, \section
, \subsection
,\subsubsection
, ..., \paragraph
depending on the document class. This is in contrast to a relative model of hierarchy, in which there is a single command to introduce a section heading at the “current” level, and there are other commands to introduce hierarchical nesting.
The absolute sectioning model is completely inadequate for the hierarchical organization of ideas, for the simple reason that it is the context of a node that determines what its level in the hierarchy is, not the node itself. When this is mixed up, it makes re-contextualization an extremely painful and time-consuming process: you must recursively increment or decrement all section levels that occur underneath a given node, as anyone who has used LaTeX for any significant writing project can attest.
In traditional texts, re-contextualization occurs when you want to move a section from one place in the hierarchy to another; in the more fluid media I am pursuing, there may be many orthogonal hierarchical structures imposed on the network, so re-contextualization ceases to be a refactoring task and is elevated as a basic unit of mathematical activity. In either case, we are drawn to prefer relative hierarchy over absolute hierarchy. See existing implementations of this idea.
This is similar to the relationship between De Bruijn levels (global levels) and De Bruijn indices (local levels) in type theory: conventional section headings are like De Bruijn indices in that they count from the root node, whereas what we would want are section headings that count from the present node.
Many document markup languages, including LaTeX and HTML, use sectioning commands that evince an implicit hierarchical structure: for instance, consider the following HTML code:
<h1>Foo</h1>
<h2>Bar</h2>
<h3>Baz</h3>
<h3>Qux</h4>
<h1>Boo</h1>
The above corresponds to the tree [Foo > [Bar > [Baz, Qux]], Boo]
. On the other hand, it is also possible to consider a model in which the hierarchy is made explicit through the syntactical tree structure of the markup language. This style is also supported (but not forced) in HTML:
<section>
<h1>Foo</h1>
<section>
<h2>Bar</h2>
<section>
<h3>Baz</h3>
</section>
<section>
<h3>Qux</h3>
</section>
</section>
</section>
<section>
<h1>Boo</h1>
</section>
We greatly prefer the combination of (relative, explicit) hierarchy.
There are a few LaTeX packages that implement relative hierarchy for sectioning as an alternative to the backward model of absolute hierarchy.
\levelup{<title>}
and \leveldown{<title>}
.\subimport
command that is to be used instead of \input
or \include
.There are some attempts to impose a (relative, explicit) hierarchical model in HTML by using <section>
and only the <h1>
heading command. In the HTML5 spec, this behavior was initially endorsed as part of the “outline” algorithm, but almost no vendors of browsers nor assistive technology have correctly implemented this behavior so it is dead on arrival.
A forest of evergreen notes (or a forest for short) is loosely defined to be a collection of evergreen notes in which multiple hierarchical structures are allowed to emerge and evolve over time. Concretely, one note may contextualize several other notes via transclusion within its textual structure; in the context of a forest, we refer to an individual note as a tree.
Of course, a tree can be viewed as a forest that has a root node.
The extent of a tree within a forest is the smallest set of trees closed under the following rules:
A forest of evergreen notes may in general contain the work of many authors: for example, the tree on constructive domain theory comprises mathematical contributions of not only the present author, but also Martín Escardó and Tom de Jong. However, the correct attribution of authorship to a given tree is more subtle than one might at first think.
To understand this subtlety, we first consider that each individual tree may contain both textual content and transcluded subtrees. Thinking inductively, a simple model of tree authorship would be to take the union of the authors of the immediate textual content and the authors of all trees within its extent. This model is incorrect, however, as authorship is usually taken to imply responsibility and endorsement, as can be seen by way of example from the ACM Policy on Authorship, Peer Review, Readership, and Conference Publication:
They agree to be held accountable for any issues relating to the correctness or integrity of the work with the understanding that depending on the circumstances not all authors are necessarily held “equally” accountable. In the case of publications-related misconduct, it may be the case that penalties may vary for co-authors listed on a single publication.
In particular, although one person may be aware of and responsible for the content of a given tree, it would be unreasonable to require them to be responsible for any subsequent (and potentially erroneous!) re-contextualization of that tree in the forest. For this reason, authors must be distinguished from contributors in forests of evergreen notes.
An author of a tree within a forest is someone who satisfies the following conditions:
A contributor to a tree within a forest is someone who is an author of at least one tree lying within its extent.
Many non-LaTeX hypertext tools boast some compatibility with mathematical typesetting: for instance, in any HTML-based tool it is possible to use MathML or, for better cross-browser support and easier authoring, import
Mathematical writing tends to involve a variety of notations which (1) can be difficult to typeset by hand, and (2) will likely change over time. The difficulty of hand-typesetting is somewhat less important than the propensity of notation to change over time: when we change notations within a given mathematical work, we must update every occurrence of the notation: but when the representation of the notation is unstructured, it is not in fact possible for a tool (e.g. find-and-replace) to detect every instance that needs to be updated. Therefore, it is mandatory that the representation of mathematical notations be structured.
LaTeX allows authors to structure their notations very simply using macros, which can be introduced using \newcommand
or \NewDocumentCommand
. It is trivial to update all occurences of a notation by simply changing the definition of the corresponding macro.
Unfortunately, most tools that purport to support the inclusion of mathematical expressions do not have adequate support for macros. Both
In LaTeX, macros are organized into packages that are then globally imported into a single document. Because a LaTeX document comprises just one project and thus any transclusions (via \input
or \include
) are of components local to that one project, this model is adequate — although experienced users of LaTeX are nonetheless all too aware of the difficulties of namespacing macro commands when interacting with multiple packages or document classes.
The requirements for a tool that aims to bring together multiple projects over a very long period of time are somewhat different: many distinct packages of notation will be used across the body of work, and it is not possible to fix a single global notation package.
Indeed, it is not reasonable to expect that all notes within a person’s mathematical life shall share the same notations, and in many cases, it would moreover be necessary for the names of the macros associated to these notations to clash. This can happen because two projects are orthogonal, or it can happen as the author’s tastes change over time — and it is not reasonable for such a tool to force enormous and weighty refactorings (touching thousands or tens of thousands of notes) every time the author’s taste changes. The need for arduous refactorings of this kind is one of the main ways that large mathematical projects tend to collapse under their own weight.
It follows that any tool for thought whose support for mathematical notations involves a globally-defined macro package is inadequate for mathematical uses. On the other hand, it is also not reasonable to require the author to define all their macros in each note: notes tend to be small, and there will always be large clusters of notes that share the same notations — and for which the small refactoring tasks involved when notations change are a positive feature rather than a negative one, as one of the goals of a cluster is to accumulate cohesion.
Therefore, the precise requirement for macro library support is as follows:
Finally, careful attention must be paid to the interaction between the above requirements and the transclusion of mathematical notes: a transcluded note must be rendered with respect to its own macro library, and not that of the parent note.
A basic requirement of tools for mathematical thought is to support the rendering of mathematical diagrams. What kinds of diagrams are needed depends, of course, on the problem domain: for my own work, the main diagram-forms needed are commutative diagrams and string diagrams.
Although diagramming may seem to non-mathematicians to be somewhat orthogonal to notational macro support, in reality any solution to the diagramming problem must be tightly and natively integrated with the rendering of mathematical expressions — simply because most diagrams involve mathematical expressions, and these invariably involve notational macros. The reason PGF/TikZ has been so successful is that it respects this tight coupling.
The situation for hypertext mathematical tools is somewhat less advanced than that of LaTeX and PFG/TikZ, but there are several options which we discuss below.
amscd
package. Unfortunately, this support is completely inadequate for usage by mathematicians today:
Like amscd
commands for rudimentary square-shaped commutative diagrams. Unlike the amscd
, the supported diagrams are rendered correctly without jagged lines; this means that for the vanishingly small population of mathematicians whose needs are limited to square-shaped diagrams, MathJax’s builtin support is viable.
On the other hand, there is a more advanced option available for users of MathJax: the XyJax-v3 plugin, which adds support for the full gamut of xypic
diagrams to MathJax. Notably, this plugin is used by the Stacks Project. The only downside of the xypic
support is that it interacts poorly with accessibility features (but no worse than any other solution to rendering non-trivial commutative diagrams), and diagrams created using xypic
look considerably less professional than those created using tikz
or quiver.
Both
The quiver application is an excellent graphical interface for interactively constructing commutative diagrams, with very high-quality rendering.
One positive aspect of quiver is that it is possible to load it with your own macro library, so that diagrams involving custom notations render correctly in the graphical interface. The downside of the approach here is that the macro library must be located on a publicly accessible URL that can be pasted into the quiver interface.
Quiver also offers excellent support for embedding the resulting diagrams in existing LaTeX documents: after creating your diagram, you can request a LaTeX snippet that includes a URL which allows you to resume editing your diagram. For example:
\[
\begin{tikzcd}
A & B
\arrow[from=1-1, to=1-2]
\end{tikzcd}
\]
Unfortunately, the support for embedding quiver diagrams in HTML documents is currently inadequate for professional use. The HTML embed code provided simply produces an <iframe>
with a very large watermark, and it is not possible to style the interior of the embedded frame (e.g. to change the background color, or decrease the margins):
<!-- https://q.uiver.app/?q=WzAsMixbMCwwLCJBIl0sWzEsMCwiQiJdLFswLDFdXQ== -->
<iframe class="quiver-embed" src="https://q.uiver.app/?q=WzAsMixbMCwwLCJBIl0sWzEsMCwiQiJdLFswLDFdXQ==&embed" width="304" height="176" style="border-radius: 8px; border: none;"></iframe>
Therefore, we must conclude that although quiver is an excellent tool for authors of traditional LaTeX documents, it is not currently a candidate for inclusion in tools for hypertext mathematical authoring.
Because of the currently inadequate support of quiver for embedding diagrams in hypertext settings, we cannot consider it any further. There is a final option that turns out to be the most used in practice: generating SVG images statically from embedded LaTeX code.
Because of the general inadequacy of the other available tools, most authors of hypertext mathematics with diagramming needs tend to rely on the static generation of images from LaTeX code using a local LaTeX toolchain. It is not difficult to instrument pandoc with a Lua filter to render tikz code to SVG images.
There are also a variety of other tools that do something similar, which tend to be employed in static site generation:
The basic architecture of such a tool is to scan for LaTeX blocks, and then identify them by a hash of their contents. This hash is used as a filename for .tex
files, which are compiled to .dvi
and thence to .svg
using the dvisvgm
tool; the resulting file is then embedded in HTML using an <img>
tag. Alternatively, is also possible to transclude the resulting <svg>
element directly, but then one must be careful to rename all identifiers in the <svg>
element uniquely, as it is possible for two different <svg>
elements on a single page to interfere one each other.
Both antex and forester support passing a macro library to be used when rendering. Both jekyll-sheafy and forester set their macro libraries on a page-local basis through Markdown “front matter”.
A serious downside of generating images from LaTeX code is the negative impact on accessibility tools. This seems only slightly mitigated by the transclusion of the <svg>
element as opposed to using <img>
. Ultimately accessibility for mathematical diagrams remains an unsolved problem, and it does not seem that the existing discussion on accessibility of hypertext mathematics has much to say about this problem.
Finally, we comment on more principled approaches using web standards such as SVG and MathML that we hope will take form in the future.
SVG is an extremely powerful low-level language for vector images and diagrams with a variety of applications. Unfortunately, it is not reasonable to compose such diagrams directly in SVG as an author: in contrast to programmatic tools like PGF/TikZ, all positions in SVG are fixed, and there is no possibility to impose important abstractions (e.g. the concept of a line that is “glued” to a pair of nodes). On the other hand, there are many advantages to SVG, including the possibility to intermix SVG with other formats such as MathML.
Because of the low level of abstraction, SVG images that appear in practice today are nearly always produced by a tool or compiler from an input that is defined at a much higher level of abstraction.
Despite some preliminary support for structured representation of high-level mathematical idioms via Content MathML, MathML is not intended to be an authoring language: it is a target language for other tools. Moreover, the content dictionaries (collections of basic elements) of Content MathML are chosen to pertain to the needs of grade-school and secondary-school mathematics and not at all to the needs of professional mathematics:
The base set of content elements is chosen to be adequate for simple coding of most of the formulas used from kindergarten to the end of high school in the United States, and probably beyond through the first two years of college, that is up to A-Level or Baccalaureate level in Europe.
Nonetheless, it seems that the goal was for the content dictionaries of Content MathML to be extended by the individual “communities of practice” to meet their specific needs:
Hence, it is not in general possible for a user agent to automatically determine the proper interpretation for
definitionURL
values without further information about the context and community of practice in which the MathML instance occurs.
However, in contexts where highly precise semantics are required (e.g. communication between computer algebra systems, within formal systems such as theorem provers, etc.) it is the responsibility of the relevant community of practice to verify, extend or replace definitions provided by OpenMath CDs as appropriate.
It seems that there is a possibility to use XSLT to define your own semantic notational macros, and this certainly bears further investigation. Due to the mutually reinforcing combination of historically poor vendor support and near-absolute isolation from actual communities of practice, i.e. working mathematicians, sophisticated direct use of MathML has never caught on. On the other hand, there is a great deal of MathML on the web today in the form of MathJax and
It seems that the future of MathML is brighter than it was in the past, as we are finally seeing a vital project to improve vendor support led by Igalia. Currently, even browsers that support the MathML standard do so with completely inadequate and unprofessional rendering quality, which means that tools like MathJax and
The W3C MathML Core Working Draft points out that MathML can be embedded into <svg>
elements using the <foreignObject>
element. This is a great strength of the modularity of the model, and I believe that in the future, we will be able to use this as a way to render accessible mathematical diagrams in hypertext.
What is missing? Essentially the current issue preventing widespread use of this method is the fact that neither SVG nor MathML is an authoring language: they are both currently too low-level to be seriously used by authors.
For exactly so long as diagrams must be drawn using LaTeX-based tools rather than something MathML-compatible, it would be non-negotiable for the support of notational macros to itself be based in LaTeX syntax (e.g. as in both
This is an investigation of Guillaume Munch-Maccagnoni’s theory of duploids, working in the setting of univalent foundations. Most of what we do could be done in non-univalent foundations; the purpose of univalence is to sharpen our perspective on the relationship between structure and property in duploid theory.
A category has hom sets, and is always assumed to be univalent / Rezk-complete; we use the term precategory to refer to a structure that has hom sets and a type of objects with no univalence condition.
The most basic construct of duploid theory is a deductive system, a variant on the concept of a precategory that relaxes the associativity axiom to reflect the evaluation order of execution in effectful programming languages and proof theories. In this section, we define deductive systems and develop their basic properties.
A deductive system
Given a deductive system
Let
An object
The following are equivalent for a deductive system
Supposing that every map is linear, we must check that each
Clearly every object is positive if and only if every map is linear; likewise, every object is negative if and only if every map is thunkable.
Finally, when every map is both linear and thunkable, the cut law is associative — but this is exactly the condition that the deductive system give rise to a precategory.
Inverses to morphisms in a deductive system need not be unique due to the general failure of associativity; therefore, we must be careful when speaking of “invertible maps” or “isomorphisms”. It happens that both linear and thunkable inverses are unique.
Let
Let
Let
Let
Let
A deductive system
A deductive system
A deductive system is called univalent when it is both positively univalent and negatively univalent.
Let
Let
All four maps
Let
Let
All four maps
An object
A deductive system
A preduploid
Equivalently, we can define a duploid to be a univalent preduploid such that every object is merely equipped with both an upshift and a downshift.
To see that the main definition implies our alternative definition, let
Conversely, assume that every object is merely equipped with both an upshift and a downshift. That a positive object
We assume knowledge of basic categorical concepts such as categories, functors, and natural transformations. The purpose of this lecture is to develop the notion of a category over another category.
We will draw on the work of Ahrens and Lumsdaine, Bénabou, Borceux, Jacobs, and Streicher.
A meta-category
In the definition of meta-categories, we have not imposed any restrictions on what kinds of things the objects and morphisms are; our definition is pre-mathematical, so we do not assume beforehand that there is a such thing as a collection of “all” meta-categories.
We may define analogous notions of meta-functor, etc. But we do not
assume that the notion of “all meta-functors
Assumption. We assume a meta-category
A category
Consequently there exists a meta-category
Assumption. At times we may assume that there exists a category
Let
When we have too many subscripts, we will write
Let
Above we have used the “pullback corner” to indicate
Let
Assuming the axiom of choice, any cartesian fibration may be equipped with a (non-canonical) cleaving. In the current version of these notes, we freely use this principle, but in the future we would like to follow Ahrens and Lumsdaine in distinguishing between weak and strong fibrations, in which the latter come equipped with cleavings.
A displayed category
We will also refer to cartesian fibrations as simply fibrations or fibered categories.
There are other variations of fibration. For instance,
Let
Prove that the fundamental self-indexing
In light of our discussion of the fundamental self-indexing, the following result for displayed categories generalizes the ordinary “pullback lemma.”
Let
Suppose first that
Because
Conversely, suppose that
Because
Some authors including Grothendieck give an equivalent definition of cartesian fibration that factors through a nonequivalent definition of cartesian morphisms. Such authors refer to our notion of cartesian morphism as “hypercartesian” (see Streicher).
Let
Cartesian morphisms are clearly hypocartesian (setting
Let
Any cartesian map is clearly hypocartesian. To see that a hypocartesian map
As the cartesian lift
Grothendieck defines a fibration in terms of (what we refer to as) hypocartesian morphisms rather than (what we refer to as) cartesian morphisms, and therefore imposes the additional constraint that the hypocartesian morphisms be closed under composition. Below, we verify that these two definitions of cartesian fibration coincide.
Let
Suppose first that
Conversely, suppose that
Let
The composite
Hypocartesian and cartesian morphisms can be thought of as two distinct ways to generalize the concept of a pullback, depending on what one considers the essential properties of pullbacks. Hypocartesian morphisms more directly generalize the “little picture” universal property of pullbacks as limiting cones, whereas cartesian morphisms generalize the “big picture” dynamics of the pullback pasting lemma. As we have seen, these two notions coincide in any cartesian fibration; the instance of this result for the fundamental self-indexing verifies that pullbacks can be equivalently presented in terms of cartesian morphisms.
Let
From this notion, we can see that the variation of displayed categories over their base categories itself has a “displayed categorical” structure; up to size issues, we could speak of the displayed bicategory of displayed categories.
Note. The correct notion of morphism between cartesian fibrations is given by displayed functors that preserve cartesian maps. We will call these fibered functors.
Let
We adapt Bénabou’s construction as reported by Streicher. Our first construction works for an uncloven fibration, but it has the downside that it requires us to treat the collection of cartesian lifts as a set that can be quotiented, whereas our second construction avoids this by virtue of a cleaving. Up to equivalence, the two constructions coincide for a cloven fibration, which shows that our second construction is independent of the chosen cleaving.
Let
Given
such that
Let
Going forward, we will not be sensitive to the difference between the two constructions of opposite fibrations.
There is a simple characterization of cartesian maps in
A morphism
Suppose that
We must define the unique intervening map
The desired intervening map
We leave the converse to the reader.
The foregoing characterization of cartesian maps in
The displayed category
Fixing
The construction of fibered opposite categories does appear quite involved, but it can be seen to be inevitable from the perspective of the fiber categories
A displayed morphism
Any ordinary category
The displayed category
This story for relative category theory reflects the way that ordinary categories are “based on”
The family fibration can be cloven, constructively. In particular, let
Suppose that
We visualize the change of base scenario as follows:
In a category
It often happens that a useful class of figure shapes can be arranged into a set-indexed family
Let
Let
Let
Note that any displayed category
The construction of the total category of a displayed category is called the Grothendieck construction.
Prove that the total category
In many cases, one starts with a functor
Suppose that
We have a functor
Explicitly construct the functorial action of
Verify that
In classical category theory, cartesian fibrations are defined by
Grothendieck to be certain functors
There is an alternative definition of cartesian fibration due to Street that avoids
equality of objects; here we require for each
By unrolling definitions, it is not difficult to see that the displayed
category
It also makes sense to speak of categories displayed over other displayed
categories; one way to formalize this notion is as follows. Let
Now let
Using the displayed category induced by a functor, we may define the pushforward of a displayed category along a functor. In particular, let
There are a number of (equivalent) variations on the definition of a locally small fibration. We attempt to provide some intuition for these definitions.
An ordinary category
Consider an index set
If
We will reformulate the local smallness property of the family fibration in a way that uses only the language that makes sense for an arbitrary cartesian fibration, though for now we stick with
First we consider the restriction of
Explicitly the family
There is a canonical map
That each
To convince ourselves of this, we note that the family
Based on our explorations above, we are now prepared to write down (and
understand) the proper definition of local smallness for an arbitrary cartesian fibration
For any
In the above,
Given
A cartesian fibration
In ordinary category theory, a category
An ordinary category is called globally small when it has a set of objects.
Up to equivalence of categories, we may detect global smallness of a category
Let
Warning. Our terminology differs from that of Jacobs; what we refer to as a generic object here is Jacobs’ weak generic object. We prefer the unqualified terminology, as generic objects in the stronger sense are very rare.
An ordinary category
To see that this is the case, suppose that
Conversely assume that
A cartesian fibration
Let
Given an ordinary category
The intuition of separating families is that to compare two morphisms
In the category of sets, to compare two morphisms it is enough to check
that they agree on global points. This means that the unary family
We will now generalize the notion of separating family to the case of a cartesian fibration.
Let
Let
A class of sets
A better behaved notion of definability for sets than the formal one is
given model-theoretically, i.e. relative to a model
A class of sets
A class of sets
Bénabou then generalizes these definitions to an arbitrary fibration,
in such a way that the general fibered notion of definable class is
equivalent in the fundamental self-indexing
To motivate Bénabou’s general notion of definability, we will first develop an alternative perspective on definability for classes of sets in terms of families of sets.
Let
Conversely to the closure of a class of sets under change of base, we may take a class of families of sets
A class of families of sets
A stable class of families of sets is definable when any family of sets can be restricted to a “biggest” subfamily that lies in the class.
Let
Suppose that
Conversely suppose that
We will now construe set-theoretic definability as the instantiation at the fundamental self-indexing
Let
Let
The purpose of this section is to develop the relationship between internal
categories (categories defined in the internal language of a category
A cartesian fibration is called small when it is both locally small and globally small.
We have already seen in our discussion of locally small and globally small categories that smallness in the fibered sense appropriately generalizes the ordinary notion of smallness for categories over
The notion of a (meta-)category is an essentially algebraic theory. As such it is possible to compute models of this theory in any category that has finite limits.
Let
For the details of these laws, we refer to any standard source.
Let
Given
The externalization is a cartesian fibration.
Given an object
The externalization is globally small
We may choose a generic object for
The externalization is locally small.
Fix
We define
We need to define a displayed evaluation map
Putting all this together, we assert that the terminal object of
Fixing another such candidate hom span
First we note that the evaluation map
The morphism
That
The full subfibration associated to a displayed object
Let
We will think of the fiber category
Because
The externalization
We will define a fibred equivalence
Fix
We must define
By composition with the “evaluation map” for our hom object, we have a map
Next we define
Let
By the characterization of the externalization we know that the externalization of
Cocartesian fibrations are a dual notion to cartesian fibrations, in which the variance of indexing is reversed.
Let
We use a “pushout corner” to indicate
A displayed category
Cocartesian fibrations are also known as opfibrations.
Let
Warning. Do not confuse this construction with the opposite fibered category, which produces a displayed category over
Let
Let
Prove that a displayed category
Recall that the fundamental self-indexing
Prove that the fundamental self-indexing
Dually to the fundamental self-indexing, every category
Let
Prove that
Prove that the total category of
Prove that
A cartesian fibration
Recall that for every
A cartesian fibration
Suppose that
Likewise, because
Conversely, suppose that
Because vertical maps are isomorphisms and
Working in univalent foundations, let
Let
When it causes no ambiguity, we will write
We will write
Let
Now let
Given a pair of reflection algebras
We shall write
Given a path of reflection algebras
Given a type
Let
We will write
Given a displayed reflection algebra
The projection function
If
Letting
Our first step is describe a classifying reflection algebra for fully incoherent cones over the identity functor on
Let
Given an element
This definition is equivalent to one given by Awodey, Frey, and Speight.
As suggested by the name, the data of an incoherent naturality structure over a family
Let
In particular, we define
To define the displayed algebra structure
Given an element
This definition is similar to that of Awodey, Frey, and Speight, except that we do not impose any coherence law for identities.
By the contractibility of singletons and our characterization of paths between homomorphisms, the definition of semicoherence structures is equivalent to following more direct formulation that avoids the additional cell
Our reason for choosing the more complex definition involving
Letting
Above we have used the definition of the structure map on the total reflection algebra as well as that of the displayed structure map on
The generic element
That the higher identification
We will use the semicoherence structure associated to any element of
From the semicoherence structure
Canceling
Therefore, the underlying function
The underlying function
In particular, the construction of Shulman gives us a type
We may equip
That the above is well-defined can be deduced as follows, using the fact that the splitting of
We have to check that the homotopy of functions
Note that
Therefore, to construct
Above we have used the fact that the coherence datum
Our main theorem then follows from wild categorical considerations, as we show below.
Let
Our splitting of the generic element of the generic cone
If
Our construction of the initial reflection algebra for each
This is a chapter-by-chapter overview of the dissertation of Jonathan Sterling.
For more than four decades, dependent type theory has been positioned as the “common language” that can finally unify mathematics and computer programming: while it has never been controversial that a computer program is a form of mathematical construction, the running hypothesis of the type theoretic community has been the converse to this claim, namely that mathematical constructions should be viewed as programs that can in principle be executed by a physical machine — roughly, sets = types and elements = programs. Thus the struggle to realize this type theoretic hypothesis has been a two-way process, punctuated by moments at which the mathematical meaning of a programming construct is elucidated, or at which the computational content of a mathematical construct is uncovered.
In the current millennium, a new identification has been taking shape in which types =
Thus one of the main projects for the first decade of homotopy type theory was to substantiate the relationship between HoTT and mathematics on the one hand, and between HoTT and computer programming on the other hand. The question of whether homotopy type theoretic language can be interpreted in sheaves on arbitrary infinite-dimensional spaces (
For any closed term
The assertions
The canonicity conjecture ensures that terms written in cubical type theory can be thought of as computer programs, and was verified independently by Huber and Angiuli for different variants of cubical type theory. The decidability conjecture is no less important, as it is a necessary ingredient to implement a typechecker or a compiler for a programming language based on cubical type theory.
This dissertation positively resolves the decidability conjecture for cubical type theory, the last remaining open question in its syntactic metatheory. Standard techniques proved inadequate for tackling this problem, so the bulk of this dissertation focuses on developing a new mathematical technique called synthetic Tait computability that generalizes and abstracts the method of Tait computability or logical predicates; in the past two years, synthetic Tait computability has played a central role in solving several problems in both type theory and core programming languages, suggesting that this dissertation presents a lasting and transformative contribution to the state of the art.
We give a chapter-by-chapter overview of First Steps in Synthetic Tait Computability. The novel contributions are contained in Chapters 4, 5, 7, and 8; the remaining Chapters 0-3 and 6 are primarily expository.
This chapter situates the motivations and applications of type theory in mathematics and computer science, and poses these against the semantic and syntactic properties of type theory that are needed to substantiate these applications. On the semantic side, type theory needs a number of properties including function extensionality, function comprehension, propositional univalence, effective quotients, etc.; on the syntactic side, type theory needs to be at least consistent, and many applications require both canonicity and decidability. Combining these syntactic and semantic properties into a single system has been a challenge, and cubical type theory was designed with the intention of satisfying them all. Prior to this dissertation, only the decidability conjecture remained open; thus with the present contribution, we regard the Cubical Hypothesis confirmed.
To state and prove theorems like canonicity and decidability for a type theory, we must have a mathematical definition of the syntax of type theory. Conventionally, the syntax of type theory has been studied in several layers: one starts with a definition of “raw” syntax as trees labeled by the names of the generating operations, quotients these trees under permutation of bound variables, and then layers on top of this an additional inductively defined formalism expressing the well-formedness of types, well-formedness of terms, definitional equality of types, and definitional equality of terms. After this, one verifies that definitional equivalence classes of well-formed types and terms can be used as the raw materials to construct a universal model of the type theory that has a universal property: any other model of type theory can be equipped with a unique structure-preserving homomorphism from the universal model. The described universal property determines the universal model up to unique isomorphism, if such a model exists.
We refer to the painstaking process described above as the subjective metatheory, building on the Hegel–Lawvere distinction between objective and subjective approaches to logic. The objective metatheory, in contrast, involves stating and proving results about type theories and programming languages relying only on the universal property of the universal model and not on any specifics of its presentation; the advantage of the objective metatheory is that it is simpler, more direct, more modular, and more composable.
Chapter 1 argues that the subjective metatheory in the sense described is redundant: the decidability conjecture can be stated with respect to any representative of the universal model and does not depend in any way on the raw syntax of type theory, and moreover, for all the type theories considered in this dissertation the existence of at least one representative of the universal model is guaranteed for somewhat trivial reasons that have nothing to do with the specifics of type theory. In this chapter, we develop a logical framework for specifying type theories modularly and working with their universal models in an objective fashion.
Much of this dissertation is stated and proved by exploiting the language of (Grothendieck) topoi, a concept that leads a dual life as a kind of generalized logic and as a kind of generalized topology. The viewpoint of topos theory qua generalized topology plays an important role in this dissertation, and yet it nonetheless remains unfamiliar to most computer scientists and logicians. For this reason, Chapter 2 is provided as sufficient exposition to understand the use of topoi in the remainder of the dissertation, focusing on the recollement or gluing of a topos from a pair of complementary open and closed subtopoi, a classical construction that provides the geometrical basis for synthetic Tait computability.
Universes started their life in the Grothendieck school of algebraic geometry as a technical device to circumvent the annoyance that there cannot be a “set of all sets”; a universe is a set of enough sets, and whilst a universe cannot contain itself, it may nonetheless lie within an even bigger universe. Several important developments in the theory of universes from the 1970s onward by Bénabou, Martin-Löf, Dybjer, Hofmann, Streicher, Awodey, and others have collided to deliver the present-day understanding of the centrality of universes in semantics: a model of type theory is just a special kind of universe in a special kind of category. This chapter provides expository background on the theory of universes, including a novel account of open and closed subuniverses to reflect the recollement theory of topoi from Chapter 2. These open and closed subuniverses will play a critical role in the development of synthetic Tait computability in subsequent chapters.
It is simple enough to verify negative properties of a formal system, e.g. the non-derivability of a given assertion
In the subsequent development of the computability method for applications in computer science, indexed variants of the logical predicates have proved to be fundamental and a number of variations on indexed logical predicates have appeared including the Kripke logical predicates of Jung and Tiuryn and the much more sophisticated Grothendieck logical predicates of Fiore and Simpson as well as Altenkirch, Dybjer, Hofmann, and Scott. This chapter points out that all of these forms of indexing arise in the same way from what is referred to as a figure shape, a continuous map into the classifying space of “Henkin models” of a given theory. Then the (Kripke, Grothendieck, etc.) logical predicates model is presented much more simply as the Artin gluing of this morphism’s inverse image.
An explicit proof of canonicity for the simply typed
The first demonstration of the power and modularity of synthetic Tait computability is a new a proof of the canonicity property for Martin-Löf type theory. Unlike traditional proofs of canonicity via non-synthetic Tait computability, the synthetic version is completely modular and broken up into general-purpose lemmas that are stated at a high level of abstraction and can be reused in proofs of different properties for different type theories. (Indeed, some of the constructions isolated in this chapter are used off the shelf in Chapter 7 to prove normalization for cubical type theory.) The modularization of syntactic metatheory is one of the main contributions of this dissertation.
This chapter develops a more sophisticated application of synthetic Tait computability, the proof of normalization and decidability of Martin-Löf’s type theory with a cumulative hierarchy of universes. The synthetic argument contained in this chapter builds on the work of Fiore on categorical normalization by gluing for simply typed λ-calculus, and that of Coquand on a presheaf-theoretic version of normalization by evaluation for dependent types. Analogous to the external argument of Fiore, we construe the syntax of normal and neutral forms as the initial algebra for an internal inductive definition in the language of synthetic Tait computability. The influence of Coquand is visible in the definition of the Tait saturation yoga for dependent types in the synthetic setting, an important closure condition for logical predicates that comprised one of the main innovations of Tait in the context of simply typed combinators. Although this chapter is intended only as “dry run” for the main result (to be exposed in Chapter 7), the normalization argument presented here has intrinsic value: it is the simplest and most direct proof of normalization and decidability for Martin-Löf type theory with
This expository chapter introduces cubical type theory as an extension to Martin-Löf’s type theory by an interval
This chapter reports the main result of the dissertation, normalization for cubical type theory and its corollaries: injectivity of type constructors, and decidability of equality & typing. These results were first obtained by Sterling and Angiuli for the fragment of cubical type theory without universes; the present chapter extends the results of op. cit. to support a cumulative hierarchy of universes.
The central innovation of this chapter is to generalize the notion of neutral form to accommodate the computational behavior of terms that have free variables of type
When
In other words, the path neutral application
Now that neutrals are equipped with frontiers of instability, a more refined notion of normal form is needed: when
where
Just as the embedding of neutrals into normals is “stabilized” by a com patible normal form defined on the neutral’s frontier of instability, so too must the Tait saturation yoga be adjusted. Conventionally one requires the computability predicate for a type
The twin innovations of frontiers of instability and stabilization then suffice to adapt the synthetic normalization argument of Chapter 5 to a proof of normalization (and thus decidability) for cubical type theory.
This dissertation has focused almost solely on the development and applications of synthetic Tait computability in the context of pure type theory, but the author originally invented synthetic Tait computability to solve problems in core programming languages, as part of Sterling and Harper’s re-analysis of the phase distinction in ML-style module systems between static (compiletime) and dynamic (runtime) code. The purpose of this chapter is to identify several applications of synthetic Tait computability to core programming languages, and set an agenda for future work — some of which has been executed and published following the completion of this dissertation
A brief overview is given of the applications of synthetic Tait computability to program modules, material that is published in the Journal of the ACM.
The modal language of synthetic Tait computability promises a new and more abstract account of refinement types and program extraction via a phase distinction between computation and specification. Refinement types are often thought of as a kind of subtype, but there is a fundamental difference: when
Finally, an application of synthetic Tait computability to security and information flow control is identified: a security class is a phase distinction between low and high security. The preliminary results presented in this section have been substantially improved upon by Sterling and Harper, adding support for general recursion and termination-insensitive noninterference by combining synthetic Tait computability with synthetic domain theory.
One of the design principles for evergreen notes described by Matuschak is atomicity (Evergreen notes should be atomic): a note should capture just one thing, and if possible, all of that thing. A related point is that it should be possible to understand a note by (1) reading it, and (2) traversing the notes that it links to and recursively understanding those notes.
Traditional mathematical notes do not achieve this kind of atomicity: understanding the meaning of a particular node (e.g. a theorem or definition) usually requires understanding everything that came (textually) before it. In the context of the hierarchical organization of evergreen mathematical notes, this would translate to needing to go upward in the hierarchy in order to understand the meaning of a leaf node. I regard this property of traditional mathematical notes as a defect: we should prefer explicit context over implicit context.
High-quality mathematical notes should make sense without context; hierarchical context is imposed in order to tell a story, but consumers of mathematical notes should not be forced into a particular narrative. Indeed, as many different hierarchical structures can be imposed, many different narratives can be explored.
My first exploration of hypertext mathematics was the lecture notes on relative category theory; in hindsight, these lecture notes are very much traditional lecture notes, not written with the atomicity principle in mind. As a result, it is often difficult to understand a given node without ascending upward in the hierarchy.
This document records what I have learned about the design of “tools for mathematical thought” over the past couple years. One of my goals in writing this is to set out both the unique requirements of an information data model that is needed to record and facilitate mathematical thought, as well as the technical requirements for tools that can be used for mathematics.
A “tool for mathematical thought” could be many things, but it must be a tool for the development and interlinking of mathematical ideas in a way that facilitates authoring, publishing, teaching, learning, and the maintenance of evergreen notes.
A tool for mathematical thought could be a piece of software, or it could be an organizing principle for physical notes on paper. In these notes, we will primarily explore the design of computerized tools for mathematical thought.
The existing tools for mathematical thought can be divided into two main categories: interactive proof assistants and textual authoring and publishing tools (including LaTeX, as well as the Gerby software that runs the Stacks Project).
The phrase evergreen note is due to Andy Matuschak, who has written extensively about it in his public Zettelkasten. Evergreen notes are permanent notes that evolve and accumulate over time, cutting across different projects.
One of the design principles for evergreen notes described by Matuschak is atomicity (Evergreen notes should be atomic): a note should capture just one thing, and if possible, all of that thing. A related point is that it should be possible to understand a note by (1) reading it, and (2) traversing the notes that it links to and recursively understanding those notes.
Traditional mathematical notes do not achieve this kind of atomicity: understanding the meaning of a particular node (e.g. a theorem or definition) usually requires understanding everything that came (textually) before it. In the context of the hierarchical organization of evergreen mathematical notes, this would translate to needing to go upward in the hierarchy in order to understand the meaning of a leaf node. I regard this property of traditional mathematical notes as a defect: we should prefer explicit context over implicit context.
High-quality mathematical notes should make sense without context; hierarchical context is imposed in order to tell a story, but consumers of mathematical notes should not be forced into a particular narrative. Indeed, as many different hierarchical structures can be imposed, many different narratives can be explored.
My first exploration of hypertext mathematics was the lecture notes on relative category theory; in hindsight, these lecture notes are very much traditional lecture notes, not written with the atomicity principle in mind. As a result, it is often difficult to understand a given node without ascending upward in the hierarchy.
Atomicity in evergreen mathematical notes is enhanced by adhering to the following principles:
It can be a bit excessive to link every word: but the pertinent links could be added to a “related pages” section.
Matuschak describes a number of organizing principles for evergreen notes, which are quite compelling; one design principle (Prefer associative ontologies to hierarchical taxonomies) deserves additional discussion in the context of mathematical thought. In particular, the problem of circular reference must be grappled with immediately rather than incidentally: in ordinary knowledge management, circularity represents the completion of a train of thought, whereas in mathematical thinking it remains very important to distinguish assumptions from consequences.
Hence a purely associative organization of mathematical knowledge is not viable (although it often happens by accident), and so the hierarchical organization of mathematics must be taken seriously from the start. We find that Matuschak has in fact already grappled with the need for hierarchy in his note It’s hard to navigate to unlinked “neighbors” in associative note systems, where he discusses the difficulty of traversing the “neighbor”-relationship between notes that are related by another note’s context, but are not related on their own. Matuschak proposes to solve the problem by grafting hierarchy onto the associative ontology after the fact through “outline notes”:
“Outline notes” can create pseudo-hierarchies with order and structure by linking to many child notes. Then we need the UI to support navigating between neighbors “through” these outline notes.
The viewpoint of outline hierarchy as a structure imposed on the existing associative ontology is a convenient organizing principle for evergreen notes in the sense of Matuschak, but it is a necessary principle for the design of tools for mathematical thought.
Multiple hierarchical structures can be imposed on the same associative network of nodes; a hierarchical structure amounts to a “narrative” that contextualizes a given subgraph of the network. One example could be the construction of lecture notes; another example could be a homework sheet; a further example could be a book chapter or scientific article. Although these may draw from the same body of definitions, theorems, examples, and exercises, these objects are contextualized within a different narrative, often toward fundamentally different ends.
As a result, any interface for navigating the neighbor-relation in hierarchically organized notes would need to take account of the multiplicity of parent nodes. Most hypertext tools assume that the position of a node in the hierarchy is unique, and therefore have a single “next/previous” navigation interface; we must investigate the design of interfaces that surface all parent/neighbor relations.
It is easy to make the mistake of prematurely imposing a complex hierarchical structure on a network of notes, which leads to excessive refactoring. Hierarchy should be used sparingly, and its strength is for the large-scale organization of ideas. The best structure to impose on a network of many small related ideas is a relatively flat one. I believe that this is one of the mistakes made in the writing of the foundations of relative category theory, whose hierarchical nesting was too complex and quite beholden to my experience with pre-hypertext media.
There are many ways to model hierarchy, but there are two salient orthogonal distinctions in the different designs.
Both HTML and LaTeX support a form of hierarchical organization with “absolute” heading levels, i.e. levels that count upward from a single root. In HTML, there is <h1>
, <h2>
, <h3>
..., and in LaTeX there is \part
, \chapter
, \section
, \subsection
,\subsubsection
, ..., \paragraph
depending on the document class. This is in contrast to a relative model of hierarchy, in which there is a single command to introduce a section heading at the “current” level, and there are other commands to introduce hierarchical nesting.
The absolute sectioning model is completely inadequate for the hierarchical organization of ideas, for the simple reason that it is the context of a node that determines what its level in the hierarchy is, not the node itself. When this is mixed up, it makes re-contextualization an extremely painful and time-consuming process: you must recursively increment or decrement all section levels that occur underneath a given node, as anyone who has used LaTeX for any significant writing project can attest.
In traditional texts, re-contextualization occurs when you want to move a section from one place in the hierarchy to another; in the more fluid media I am pursuing, there may be many orthogonal hierarchical structures imposed on the network, so re-contextualization ceases to be a refactoring task and is elevated as a basic unit of mathematical activity. In either case, we are drawn to prefer relative hierarchy over absolute hierarchy. See existing implementations of this idea.
This is similar to the relationship between De Bruijn levels (global levels) and De Bruijn indices (local levels) in type theory: conventional section headings are like De Bruijn indices in that they count from the root node, whereas what we would want are section headings that count from the present node.
Many document markup languages, including LaTeX and HTML, use sectioning commands that evince an implicit hierarchical structure: for instance, consider the following HTML code:
<h1>Foo</h1>
<h2>Bar</h2>
<h3>Baz</h3>
<h3>Qux</h4>
<h1>Boo</h1>
The above corresponds to the tree [Foo > [Bar > [Baz, Qux]], Boo]
. On the other hand, it is also possible to consider a model in which the hierarchy is made explicit through the syntactical tree structure of the markup language. This style is also supported (but not forced) in HTML:
<section>
<h1>Foo</h1>
<section>
<h2>Bar</h2>
<section>
<h3>Baz</h3>
</section>
<section>
<h3>Qux</h3>
</section>
</section>
</section>
<section>
<h1>Boo</h1>
</section>
We greatly prefer the combination of (relative, explicit) hierarchy.
There are a few LaTeX packages that implement relative hierarchy for sectioning as an alternative to the backward model of absolute hierarchy.
\levelup{<title>}
and \leveldown{<title>}
.\subimport
command that is to be used instead of \input
or \include
.There are some attempts to impose a (relative, explicit) hierarchical model in HTML by using <section>
and only the <h1>
heading command. In the HTML5 spec, this behavior was initially endorsed as part of the “outline” algorithm, but almost no vendors of browsers nor assistive technology have correctly implemented this behavior so it is dead on arrival.
A forest of evergreen notes (or a forest for short) is loosely defined to be a collection of evergreen notes in which multiple hierarchical structures are allowed to emerge and evolve over time. Concretely, one note may contextualize several other notes via transclusion within its textual structure; in the context of a forest, we refer to an individual note as a tree.
Of course, a tree can be viewed as a forest that has a root node.
The extent of a tree within a forest is the smallest set of trees closed under the following rules:
A forest of evergreen notes may in general contain the work of many authors: for example, the tree on constructive domain theory comprises mathematical contributions of not only the present author, but also Martín Escardó and Tom de Jong. However, the correct attribution of authorship to a given tree is more subtle than one might at first think.
To understand this subtlety, we first consider that each individual tree may contain both textual content and transcluded subtrees. Thinking inductively, a simple model of tree authorship would be to take the union of the authors of the immediate textual content and the authors of all trees within its extent. This model is incorrect, however, as authorship is usually taken to imply responsibility and endorsement, as can be seen by way of example from the ACM Policy on Authorship, Peer Review, Readership, and Conference Publication:
They agree to be held accountable for any issues relating to the correctness or integrity of the work with the understanding that depending on the circumstances not all authors are necessarily held “equally” accountable. In the case of publications-related misconduct, it may be the case that penalties may vary for co-authors listed on a single publication.
In particular, although one person may be aware of and responsible for the content of a given tree, it would be unreasonable to require them to be responsible for any subsequent (and potentially erroneous!) re-contextualization of that tree in the forest. For this reason, authors must be distinguished from contributors in forests of evergreen notes.
An author of a tree within a forest is someone who satisfies the following conditions:
A contributor to a tree within a forest is someone who is an author of at least one tree lying within its extent.
Many non-LaTeX hypertext tools boast some compatibility with mathematical typesetting: for instance, in any HTML-based tool it is possible to use MathML or, for better cross-browser support and easier authoring, import
Mathematical writing tends to involve a variety of notations which (1) can be difficult to typeset by hand, and (2) will likely change over time. The difficulty of hand-typesetting is somewhat less important than the propensity of notation to change over time: when we change notations within a given mathematical work, we must update every occurrence of the notation: but when the representation of the notation is unstructured, it is not in fact possible for a tool (e.g. find-and-replace) to detect every instance that needs to be updated. Therefore, it is mandatory that the representation of mathematical notations be structured.
LaTeX allows authors to structure their notations very simply using macros, which can be introduced using \newcommand
or \NewDocumentCommand
. It is trivial to update all occurences of a notation by simply changing the definition of the corresponding macro.
Unfortunately, most tools that purport to support the inclusion of mathematical expressions do not have adequate support for macros. Both
In LaTeX, macros are organized into packages that are then globally imported into a single document. Because a LaTeX document comprises just one project and thus any transclusions (via \input
or \include
) are of components local to that one project, this model is adequate — although experienced users of LaTeX are nonetheless all too aware of the difficulties of namespacing macro commands when interacting with multiple packages or document classes.
The requirements for a tool that aims to bring together multiple projects over a very long period of time are somewhat different: many distinct packages of notation will be used across the body of work, and it is not possible to fix a single global notation package.
Indeed, it is not reasonable to expect that all notes within a person’s mathematical life shall share the same notations, and in many cases, it would moreover be necessary for the names of the macros associated to these notations to clash. This can happen because two projects are orthogonal, or it can happen as the author’s tastes change over time — and it is not reasonable for such a tool to force enormous and weighty refactorings (touching thousands or tens of thousands of notes) every time the author’s taste changes. The need for arduous refactorings of this kind is one of the main ways that large mathematical projects tend to collapse under their own weight.
It follows that any tool for thought whose support for mathematical notations involves a globally-defined macro package is inadequate for mathematical uses. On the other hand, it is also not reasonable to require the author to define all their macros in each note: notes tend to be small, and there will always be large clusters of notes that share the same notations — and for which the small refactoring tasks involved when notations change are a positive feature rather than a negative one, as one of the goals of a cluster is to accumulate cohesion.
Therefore, the precise requirement for macro library support is as follows:
Finally, careful attention must be paid to the interaction between the above requirements and the transclusion of mathematical notes: a transcluded note must be rendered with respect to its own macro library, and not that of the parent note.
A basic requirement of tools for mathematical thought is to support the rendering of mathematical diagrams. What kinds of diagrams are needed depends, of course, on the problem domain: for my own work, the main diagram-forms needed are commutative diagrams and string diagrams.
Although diagramming may seem to non-mathematicians to be somewhat orthogonal to notational macro support, in reality any solution to the diagramming problem must be tightly and natively integrated with the rendering of mathematical expressions — simply because most diagrams involve mathematical expressions, and these invariably involve notational macros. The reason PGF/TikZ has been so successful is that it respects this tight coupling.
The situation for hypertext mathematical tools is somewhat less advanced than that of LaTeX and PFG/TikZ, but there are several options which we discuss below.
amscd
package. Unfortunately, this support is completely inadequate for usage by mathematicians today:
Like amscd
commands for rudimentary square-shaped commutative diagrams. Unlike the amscd
, the supported diagrams are rendered correctly without jagged lines; this means that for the vanishingly small population of mathematicians whose needs are limited to square-shaped diagrams, MathJax’s builtin support is viable.
On the other hand, there is a more advanced option available for users of MathJax: the XyJax-v3 plugin, which adds support for the full gamut of xypic
diagrams to MathJax. Notably, this plugin is used by the Stacks Project. The only downside of the xypic
support is that it interacts poorly with accessibility features (but no worse than any other solution to rendering non-trivial commutative diagrams), and diagrams created using xypic
look considerably less professional than those created using tikz
or quiver.
Both
The quiver application is an excellent graphical interface for interactively constructing commutative diagrams, with very high-quality rendering.
One positive aspect of quiver is that it is possible to load it with your own macro library, so that diagrams involving custom notations render correctly in the graphical interface. The downside of the approach here is that the macro library must be located on a publicly accessible URL that can be pasted into the quiver interface.
Quiver also offers excellent support for embedding the resulting diagrams in existing LaTeX documents: after creating your diagram, you can request a LaTeX snippet that includes a URL which allows you to resume editing your diagram. For example:
\[
\begin{tikzcd}
A & B
\arrow[from=1-1, to=1-2]
\end{tikzcd}
\]
Unfortunately, the support for embedding quiver diagrams in HTML documents is currently inadequate for professional use. The HTML embed code provided simply produces an <iframe>
with a very large watermark, and it is not possible to style the interior of the embedded frame (e.g. to change the background color, or decrease the margins):
<!-- https://q.uiver.app/?q=WzAsMixbMCwwLCJBIl0sWzEsMCwiQiJdLFswLDFdXQ== -->
<iframe class="quiver-embed" src="https://q.uiver.app/?q=WzAsMixbMCwwLCJBIl0sWzEsMCwiQiJdLFswLDFdXQ==&embed" width="304" height="176" style="border-radius: 8px; border: none;"></iframe>
Therefore, we must conclude that although quiver is an excellent tool for authors of traditional LaTeX documents, it is not currently a candidate for inclusion in tools for hypertext mathematical authoring.
Because of the currently inadequate support of quiver for embedding diagrams in hypertext settings, we cannot consider it any further. There is a final option that turns out to be the most used in practice: generating SVG images statically from embedded LaTeX code.
Because of the general inadequacy of the other available tools, most authors of hypertext mathematics with diagramming needs tend to rely on the static generation of images from LaTeX code using a local LaTeX toolchain. It is not difficult to instrument pandoc with a Lua filter to render tikz code to SVG images.
There are also a variety of other tools that do something similar, which tend to be employed in static site generation:
The basic architecture of such a tool is to scan for LaTeX blocks, and then identify them by a hash of their contents. This hash is used as a filename for .tex
files, which are compiled to .dvi
and thence to .svg
using the dvisvgm
tool; the resulting file is then embedded in HTML using an <img>
tag. Alternatively, is also possible to transclude the resulting <svg>
element directly, but then one must be careful to rename all identifiers in the <svg>
element uniquely, as it is possible for two different <svg>
elements on a single page to interfere one each other.
Both antex and forester support passing a macro library to be used when rendering. Both jekyll-sheafy and forester set their macro libraries on a page-local basis through Markdown “front matter”.
A serious downside of generating images from LaTeX code is the negative impact on accessibility tools. This seems only slightly mitigated by the transclusion of the <svg>
element as opposed to using <img>
. Ultimately accessibility for mathematical diagrams remains an unsolved problem, and it does not seem that the existing discussion on accessibility of hypertext mathematics has much to say about this problem.
Finally, we comment on more principled approaches using web standards such as SVG and MathML that we hope will take form in the future.
SVG is an extremely powerful low-level language for vector images and diagrams with a variety of applications. Unfortunately, it is not reasonable to compose such diagrams directly in SVG as an author: in contrast to programmatic tools like PGF/TikZ, all positions in SVG are fixed, and there is no possibility to impose important abstractions (e.g. the concept of a line that is “glued” to a pair of nodes). On the other hand, there are many advantages to SVG, including the possibility to intermix SVG with other formats such as MathML.
Because of the low level of abstraction, SVG images that appear in practice today are nearly always produced by a tool or compiler from an input that is defined at a much higher level of abstraction.
Despite some preliminary support for structured representation of high-level mathematical idioms via Content MathML, MathML is not intended to be an authoring language: it is a target language for other tools. Moreover, the content dictionaries (collections of basic elements) of Content MathML are chosen to pertain to the needs of grade-school and secondary-school mathematics and not at all to the needs of professional mathematics:
The base set of content elements is chosen to be adequate for simple coding of most of the formulas used from kindergarten to the end of high school in the United States, and probably beyond through the first two years of college, that is up to A-Level or Baccalaureate level in Europe.
Nonetheless, it seems that the goal was for the content dictionaries of Content MathML to be extended by the individual “communities of practice” to meet their specific needs:
Hence, it is not in general possible for a user agent to automatically determine the proper interpretation for
definitionURL
values without further information about the context and community of practice in which the MathML instance occurs.
However, in contexts where highly precise semantics are required (e.g. communication between computer algebra systems, within formal systems such as theorem provers, etc.) it is the responsibility of the relevant community of practice to verify, extend or replace definitions provided by OpenMath CDs as appropriate.
It seems that there is a possibility to use XSLT to define your own semantic notational macros, and this certainly bears further investigation. Due to the mutually reinforcing combination of historically poor vendor support and near-absolute isolation from actual communities of practice, i.e. working mathematicians, sophisticated direct use of MathML has never caught on. On the other hand, there is a great deal of MathML on the web today in the form of MathJax and
It seems that the future of MathML is brighter than it was in the past, as we are finally seeing a vital project to improve vendor support led by Igalia. Currently, even browsers that support the MathML standard do so with completely inadequate and unprofessional rendering quality, which means that tools like MathJax and
The W3C MathML Core Working Draft points out that MathML can be embedded into <svg>
elements using the <foreignObject>
element. This is a great strength of the modularity of the model, and I believe that in the future, we will be able to use this as a way to render accessible mathematical diagrams in hypertext.
What is missing? Essentially the current issue preventing widespread use of this method is the fact that neither SVG nor MathML is an authoring language: they are both currently too low-level to be seriously used by authors.
For exactly so long as diagrams must be drawn using LaTeX-based tools rather than something MathML-compatible, it would be non-negotiable for the support of notational macros to itself be based in LaTeX syntax (e.g. as in both
A “tool for mathematical thought” could be many things, but it must be a tool for the development and interlinking of mathematical ideas in a way that facilitates authoring, publishing, teaching, learning, and the maintenance of evergreen notes.
A tool for mathematical thought could be a piece of software, or it could be an organizing principle for physical notes on paper. In these notes, we will primarily explore the design of computerized tools for mathematical thought.
This is an investigation of Guillaume Munch-Maccagnoni’s theory of duploids, working in the setting of univalent foundations. Most of what we do could be done in non-univalent foundations; the purpose of univalence is to sharpen our perspective on the relationship between structure and property in duploid theory.
A category has hom sets, and is always assumed to be univalent / Rezk-complete; we use the term precategory to refer to a structure that has hom sets and a type of objects with no univalence condition.
The most basic construct of duploid theory is a deductive system, a variant on the concept of a precategory that relaxes the associativity axiom to reflect the evaluation order of execution in effectful programming languages and proof theories. In this section, we define deductive systems and develop their basic properties.
A deductive system
Given a deductive system
Let
An object
The following are equivalent for a deductive system
Supposing that every map is linear, we must check that each
Clearly every object is positive if and only if every map is linear; likewise, every object is negative if and only if every map is thunkable.
Finally, when every map is both linear and thunkable, the cut law is associative — but this is exactly the condition that the deductive system give rise to a precategory.
Inverses to morphisms in a deductive system need not be unique due to the general failure of associativity; therefore, we must be careful when speaking of “invertible maps” or “isomorphisms”. It happens that both linear and thunkable inverses are unique.
Let
Let
Let
Let
Let
A deductive system
A deductive system
A deductive system is called univalent when it is both positively univalent and negatively univalent.
Let
Let
All four maps
Let
Let
All four maps
An object
A deductive system
A preduploid
Equivalently, we can define a duploid to be a univalent preduploid such that every object is merely equipped with both an upshift and a downshift.
To see that the main definition implies our alternative definition, let
Conversely, assume that every object is merely equipped with both an upshift and a downshift. That a positive object
We assume knowledge of basic categorical concepts such as categories, functors, and natural transformations. The purpose of this lecture is to develop the notion of a category over another category.
We will draw on the work of Ahrens and Lumsdaine, Bénabou, Borceux, Jacobs, and Streicher.
A meta-category
In the definition of meta-categories, we have not imposed any restrictions on what kinds of things the objects and morphisms are; our definition is pre-mathematical, so we do not assume beforehand that there is a such thing as a collection of “all” meta-categories.
We may define analogous notions of meta-functor, etc. But we do not
assume that the notion of “all meta-functors
Assumption. We assume a meta-category
A category
Consequently there exists a meta-category
Assumption. At times we may assume that there exists a category
Let
When we have too many subscripts, we will write
Let
Above we have used the “pullback corner” to indicate
Let
Assuming the axiom of choice, any cartesian fibration may be equipped with a (non-canonical) cleaving. In the current version of these notes, we freely use this principle, but in the future we would like to follow Ahrens and Lumsdaine in distinguishing between weak and strong fibrations, in which the latter come equipped with cleavings.
A displayed category
We will also refer to cartesian fibrations as simply fibrations or fibered categories.
There are other variations of fibration. For instance,
Let
Prove that the fundamental self-indexing
In light of our discussion of the fundamental self-indexing, the following result for displayed categories generalizes the ordinary “pullback lemma.”
Let
Suppose first that
Because
Conversely, suppose that
Because
Some authors including Grothendieck give an equivalent definition of cartesian fibration that factors through a nonequivalent definition of cartesian morphisms. Such authors refer to our notion of cartesian morphism as “hypercartesian” (see Streicher).
Let
Cartesian morphisms are clearly hypocartesian (setting
Let
Any cartesian map is clearly hypocartesian. To see that a hypocartesian map
As the cartesian lift
Grothendieck defines a fibration in terms of (what we refer to as) hypocartesian morphisms rather than (what we refer to as) cartesian morphisms, and therefore imposes the additional constraint that the hypocartesian morphisms be closed under composition. Below, we verify that these two definitions of cartesian fibration coincide.
Let
Suppose first that
Conversely, suppose that
Let
The composite
Hypocartesian and cartesian morphisms can be thought of as two distinct ways to generalize the concept of a pullback, depending on what one considers the essential properties of pullbacks. Hypocartesian morphisms more directly generalize the “little picture” universal property of pullbacks as limiting cones, whereas cartesian morphisms generalize the “big picture” dynamics of the pullback pasting lemma. As we have seen, these two notions coincide in any cartesian fibration; the instance of this result for the fundamental self-indexing verifies that pullbacks can be equivalently presented in terms of cartesian morphisms.
Let
From this notion, we can see that the variation of displayed categories over their base categories itself has a “displayed categorical” structure; up to size issues, we could speak of the displayed bicategory of displayed categories.
Note. The correct notion of morphism between cartesian fibrations is given by displayed functors that preserve cartesian maps. We will call these fibered functors.
Let
We adapt Bénabou’s construction as reported by Streicher. Our first construction works for an uncloven fibration, but it has the downside that it requires us to treat the collection of cartesian lifts as a set that can be quotiented, whereas our second construction avoids this by virtue of a cleaving. Up to equivalence, the two constructions coincide for a cloven fibration, which shows that our second construction is independent of the chosen cleaving.
Let
Given
such that
Let
Going forward, we will not be sensitive to the difference between the two constructions of opposite fibrations.
There is a simple characterization of cartesian maps in
A morphism
Suppose that
We must define the unique intervening map
The desired intervening map
We leave the converse to the reader.
The foregoing characterization of cartesian maps in
The displayed category
Fixing
The construction of fibered opposite categories does appear quite involved, but it can be seen to be inevitable from the perspective of the fiber categories
A displayed morphism
Any ordinary category
The displayed category
This story for relative category theory reflects the way that ordinary categories are “based on”
The family fibration can be cloven, constructively. In particular, let
Suppose that
We visualize the change of base scenario as follows:
In a category
It often happens that a useful class of figure shapes can be arranged into a set-indexed family
Let
Let
Let
Note that any displayed category
The construction of the total category of a displayed category is called the Grothendieck construction.
Prove that the total category
In many cases, one starts with a functor
Suppose that
We have a functor
Explicitly construct the functorial action of
Verify that
In classical category theory, cartesian fibrations are defined by
Grothendieck to be certain functors
There is an alternative definition of cartesian fibration due to Street that avoids
equality of objects; here we require for each
By unrolling definitions, it is not difficult to see that the displayed
category
It also makes sense to speak of categories displayed over other displayed
categories; one way to formalize this notion is as follows. Let
Now let
Using the displayed category induced by a functor, we may define the pushforward of a displayed category along a functor. In particular, let
There are a number of (equivalent) variations on the definition of a locally small fibration. We attempt to provide some intuition for these definitions.
An ordinary category
Consider an index set
If
We will reformulate the local smallness property of the family fibration in a way that uses only the language that makes sense for an arbitrary cartesian fibration, though for now we stick with
First we consider the restriction of
Explicitly the family
There is a canonical map
That each
To convince ourselves of this, we note that the family
Based on our explorations above, we are now prepared to write down (and
understand) the proper definition of local smallness for an arbitrary cartesian fibration
For any
In the above,
Given
A cartesian fibration
In ordinary category theory, a category
An ordinary category is called globally small when it has a set of objects.
Up to equivalence of categories, we may detect global smallness of a category
Let
Warning. Our terminology differs from that of Jacobs; what we refer to as a generic object here is Jacobs’ weak generic object. We prefer the unqualified terminology, as generic objects in the stronger sense are very rare.
An ordinary category
To see that this is the case, suppose that
Conversely assume that
A cartesian fibration
Let
Given an ordinary category
The intuition of separating families is that to compare two morphisms
In the category of sets, to compare two morphisms it is enough to check
that they agree on global points. This means that the unary family
We will now generalize the notion of separating family to the case of a cartesian fibration.
Let
Let
A class of sets
A better behaved notion of definability for sets than the formal one is
given model-theoretically, i.e. relative to a model
A class of sets
A class of sets
Bénabou then generalizes these definitions to an arbitrary fibration,
in such a way that the general fibered notion of definable class is
equivalent in the fundamental self-indexing
To motivate Bénabou’s general notion of definability, we will first develop an alternative perspective on definability for classes of sets in terms of families of sets.
Let
Conversely to the closure of a class of sets under change of base, we may take a class of families of sets
A class of families of sets
A stable class of families of sets is definable when any family of sets can be restricted to a “biggest” subfamily that lies in the class.
Let
Suppose that
Conversely suppose that
We will now construe set-theoretic definability as the instantiation at the fundamental self-indexing
Let
Let
The purpose of this section is to develop the relationship between internal
categories (categories defined in the internal language of a category
A cartesian fibration is called small when it is both locally small and globally small.
We have already seen in our discussion of locally small and globally small categories that smallness in the fibered sense appropriately generalizes the ordinary notion of smallness for categories over
The notion of a (meta-)category is an essentially algebraic theory. As such it is possible to compute models of this theory in any category that has finite limits.
Let
For the details of these laws, we refer to any standard source.
Let
Given
The externalization is a cartesian fibration.
Given an object
The externalization is globally small
We may choose a generic object for
The externalization is locally small.
Fix
We define
We need to define a displayed evaluation map
Putting all this together, we assert that the terminal object of
Fixing another such candidate hom span
First we note that the evaluation map
The morphism
That
The full subfibration associated to a displayed object
Let
We will think of the fiber category
Because
The externalization
We will define a fibred equivalence
Fix
We must define
By composition with the “evaluation map” for our hom object, we have a map
Next we define
Let
By the characterization of the externalization we know that the externalization of
Cocartesian fibrations are a dual notion to cartesian fibrations, in which the variance of indexing is reversed.
Let
We use a “pushout corner” to indicate
A displayed category
Cocartesian fibrations are also known as opfibrations.
Let
Warning. Do not confuse this construction with the opposite fibered category, which produces a displayed category over
Let
Let
Prove that a displayed category
Recall that the fundamental self-indexing
Prove that the fundamental self-indexing
Dually to the fundamental self-indexing, every category
Let
Prove that
Prove that the total category of
Prove that
A cartesian fibration
Recall that for every
A cartesian fibration
Suppose that
Likewise, because
Conversely, suppose that
Because vertical maps are isomorphisms and
This tree defines the basic notational macros used across .
We study idempotents in intensional Martin-Löf type theory, and in particular the question of when and whether they split. We show that in the presence of propositional truncation and Voevodsky’s univalence axiom, there exist idempotents that do not split; thus in plain MLTT not all idempotents can be proven to split. On the other hand, assuming only function extensionality, an idempotent can be split if and only if its witness of idempotency satisfies one extra coherence condition. Both proofs are inspired by parallel results of Lurie in higher category theory, showing that ideas from higher category theory and homotopy theory can have applications even in ordinary MLTT.
Finally, we show that although the witness of idempotency can be recovered from a splitting, the one extra coherence condition cannot in general; and we construct “the type of fully coherent idempotents”, by splitting an idempotent on the type of partially coherent ones. Our results have been formally verified in the proof assistant Coq.
We develop domain theory in constructive and predicative univalent foundations (also known as homotopy type theory). That we work predicatively means that we do not assume Voevodsky’s propositional resizing axioms. Our work is constructive in the sense that we do not rely on excluded middle or the axiom of (countable) choice. Domain theory studies so-called directed complete posets (dcpos) and Scott continuous maps between them and has applications in programming language semantics, higher-type computability and topology. A common approach to deal with size issues in a predicative foundation is to work with information systems, abstract bases or formal topologies rather than dcpos, and approximable relations rather than Scott continuous functions. In our type-theoretic approach, we instead accept that dcpos may be large and work with type universes to account for this. A priori one might expect that complex constructions of dcpos result in a need for ever-increasing universes and are predicatively impossible. We show that such constructions can be carried out in a predicative setting. We illustrate the development with applications in the semantics of programming languages: the soundness and computational adequacy of the Scott model of PCF and Scott’s
These are notes about the theory of Fibred Categories as I have learned it from Jean Bénabou. I also have used results from the Thesis of Jean-Luc Moens from 1982 in those sections where I discuss the fibered view of geometric morphisms. Thus, almost all of the contents is not due to me but most of it cannot be found in the literature since Bénabou has given many talks on it but most of his work on fibered categories is unpublished. But I am solely responsible for the mistakes and for misrepresentations of his views. And certainly these notes do not cover all the work he has done on fibered categories. I just try to explain the most important notions he has come up with in a way trying to be as close as possible to his intentions and intuitions. I started these notes in 1999 when I gave a course on some of the material at a workshop in Munich. They have developed quite a lot over the years and I have tried to include most of the things I want to remember.
We present calf, a cost-aware logical framework for studying quantitative aspects of functional programs. Taking inspiration from recent work that reconstructs traditional aspects of programming languages in terms of a modal account of phase distinctions, we argue that the cost structure of programs motivates a phase distinction between intension and extension. Armed with this technology, we contribute a synthetic account of cost structure as a computational effect in which cost-aware programs enjoy an internal noninterference property: input/output behavior cannot depend on cost. As a full-spectrum dependent type theory, calf presents a unified language for programming and specification of both cost and behavior that can be integrated smoothly with existing mathematical libraries available in type theoretic proof assistants.
We evaluate calf as a general framework for cost analysis by implementing two fundamental techniques for algorithm analysis: the method of recurrence relations and physicist’s method for amortized analysis. We deploy these techniques on a variety of case studies: we prove a tight, closed bound for Euclid’s algorithm, verify the amortized complexity of batched queues, and derive tight, closed bounds for the sequential and parallel complexity of merge sort, all fully mechanized in the Agda proof assistant. Lastly we substantiate the soundness of quantitative reasoning in calf by means of a model construction.
We propose a new sheaf semantics for secure information flow over a space of abstract behaviors, based on synthetic domain theory: security classes are open/closed partitions, types are sheaves, and redaction of sensitive information corresponds to restricting a sheaf to a closed subspace. Our security-aware computational model satisfies termination-insensitive noninterference automatically, and therefore constitutes an intrinsic alternative to state of the art extrinsic/relational models of noninterference. Our semantics is the latest application of Sterling and Harper’s recent re-interpretation of phase distinctions and noninterference in programming languages in terms of Artin gluing and topos-theoretic open/closed modalities. Prior applications include parametricity for ML modules, the proof of normalization for cubical type theory by Sterling and Angiuli, and the cost-aware logical framework of Niu et al. In this paper we employ the phase distinction perspective twice: first to reconstruct the syntax and semantics of secure information flow as a lattice of phase distinctions between “higher” and “lower” security, and second to verify the computational adequacy of our sheaf semantics with respect to a version of Abadi et al.’s dependency core calculus to which we have added a construct for declassifying termination channels.
The theory of program modules is of interest to language designers not only for its practical importance to programming, but also because it lies at the nexus of three fundamental concerns in language design: the phase distinction, computational effects, and type abstraction. We contribute a fresh “synthetic” take on program modules that treats modules as the fundamental constructs, in which the usual suspects of prior module calculi (kinds, constructors, dynamic programs) are rendered as derived notions in terms of a modal type-theoretic account of the phase distinction. We simplify the account of type abstraction (embodied in the generativity of module functors) through a lax modality that encapsulates computational effects, placing projectibility of module expressions on a type-theoretic basis.
Our main result is a (significant) proof-relevant and phase-sensitive generalization of the Reynolds abstraction theorem for a calculus of program modules, based on a new kind of logical relation called a parametricity structure. Parametricity structures generalize the proof-irrelevant relations of classical parametricity to proof-relevant families, where there may be non-trivial evidence witnessing the relatedness of two programs—simplifying the metatheory of strong sums over the collection of types, for although there can be no “relation classifying relations,” one easily accommodates a “family classifying small families.”
Using the insight that logical relations/parametricity is itself a form of phase distinction between the syntactic and the semantic, we contribute a new synthetic approach to phase separated parametricity based on the slogan logical relations as types, by iterating our modal account of the phase distinction. We axiomatize a dependent type theory of parametricity structures using two pairs of complementary modalities (syntactic, semantic) and (static, dynamic), substantiated using the topos theoretic Artin gluing construction. Then, to construct a simulation between two implementations of an abstract type, one simply programs a third implementation whose type component carries the representation invariant.
The implementation and semantics of dependent type theories can be studied in a syntax-independent way: the objective metatheory of dependent type theories exploits the universal properties of their syntactic categories to endow them with computational content, mathematical meaning, and practical implementation (normalization, type checking, elaboration). The semantic methods of the objective metatheory inform the design and implementation of correct-by-construction elaboration algorithms, promising a principled interface between real proof assistants and ideal mathematics.
In this dissertation, I add synthetic Tait computability to the arsenal of the objective metatheorist. Synthetic Tait computability is a mathematical machine to reduce difficult problems of type theory and programming languages to trivial theorems of topos theory. First employed by Sterling and Harper to reconstruct the theory of program modules and their phase separated parametricity, synthetic Tait computability is deployed here to resolve the last major open question in the syntactic metatheory of cubical type theory: normalization of open terms.
We prove normalization for (univalent, Cartesian) cubical type theory, closing the last major open problem in the syntactic metatheory of cubical type theory. Our normalization result is reduction-free, in the sense of yielding a bijection between equivalence classes of terms in context and a tractable language of
We present a cubical type theory based on the Cartesian cube category (faces, degeneracies, symmetries, diagonals, but no connections or reversal) with univalent universes, each containing
In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our programming language is dependently-typed, however, we would like to appeal to such invariance results within the language itself, in order to obtain correctness theorems for complex implementations by transferring them from simpler, related implementations. Recent work in proof assistants has shown that Voevodsky’s univalence principle allows transferring theorems between isomorphic types, but many instances of representation independence in programming involve non-isomorphic representations.
In this paper, we develop techniques for establishing internal relational representation independence results in dependent type theory, by using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them. The correspondence becomes an isomorphism between the quotiented types, thereby allowing us to obtain an equality of implementations by univalence. We illustrate our techniques by considering applications to matrices, queues, and finite multisets. Our results are all formalized in Cubical Agda, a recent extension of Agda which supports univalence and higher inductive types in a computationally well-behaved way.
Dependent type theories are a family of logical systems that serve as expressive functional programming languages and as the basis of many proof assistants. In the past decade, type theories have also attracted the attention of mathematicians due to surprising connections with homotopy theory the study of these connections, known as homotopy type theory, has in turn suggested novel extensions to type theory, including higher inductive types and Voevodskys univalence axiom. However, in their original axiomatic presentation, these extensions lack computational content, making them unusable as programming constructs and unergonomic in proof assistants.
We prove the conjecture that any Grothendieck (
We introduce and develop the notion of displayed categories. A displayed category over a category
We present a dependent type theory organized around a Cartesian notion of cubes (with faces, degeneracies, and diagonals), supporting both fibrant and non-fibrant types. The fibrant fragment validates Voevodsky’s univalence axiom and includes a circle type, while the non-fibrant fragment includes exact (strict) equality types satisfying equality reflection. Our type theory is defined by a semantics in cubical partial equivalence relations, and is the first two-level type theory to satisfy the canonicity property: all closed terms of boolean type evaluate to either true or false.
Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant η-equalities and consequently do not admit dependent eliminators. To recover η and dependent elimination, we present a method to construct refinements of these impredicative encodings, using ideas from homotopy type theory. We then extend our method to construct impredicative encodings of some higher inductive types, such as 1-truncation and the unit circle S1.
Cubical type theory is an extension of Martin-Löf type theory recently proposed by Cohen, Coquand, Mörtberg, and the author which allows for direct manipulation of n-dimensional cubes and where Voevodsky’s Univalence Axiom is provable. In this paper we prove canonicity for cubical type theory: any natural number in a context build from only name variables is judgmentally equal to a numeral. To achieve this we formulate a typed and deterministic operational semantics and employ a computability argument adapted to a presheaf-like setting.
The Stacks project is an ever growing open source textbook and reference work on algebraic stacks and the algebraic geometry needed to define them. Here are some quick facts:
For a longer discussion, please read the blog post What is the stacks project?.
In the last 60 years, the use of the notion of category has led to a remarkable unification and simplification of mathematics. Conceptual Mathematics, Second Edition, introduces the concept of ‘category’ for the learning, development, and use of mathematics, to both beginning students and general readers, and to practicing mathematical scientists. The treatment does not presuppose knowledge of specific fields, but rather develops, from basic definitions, such elementary categories as discrete dynamical systems and directed graphs; the fundamental ideas are then illuminated by examples in these categories.
Quillen introduced model categories as an abstract framework for homotopy theory which would apply to a wide range of mathematical settings. By all accounts this program has been a success and — as, e.g., the work of Voevodsky on the homotopy theory of schemes or the work of Joyal and Lurie on quasicategories seem to indicate—it will likely continue to facilitate mathematical advances. In this paper we present a novel connection between model categories and mathematical logic, inspired by the groupoid model of (intensional) Martin–Löf type theory due to Hofmann and Streicher. In particular, we show that a form of Martin–Löf type theory can be soundly modelled in any model category. This result indicates moreover that any model category has an associated “internal language” which is itself a form of Martin-Löf type theory. This suggests applications both to type theory and to homotopy theory. Because Martin–Löf type theory is, in one form or another, the theoretical basis for many of the computer proof assistants currently in use, such as Coq and Agda, this promise of applications is of a practical, as well as theoretical, nature.
Dcpos can be presented by preorders of generators and inequational relations expressed as covers. Algebraic operations on the generators (possibly with their results being ideals of generators) can be extended to the dcpo presented, provided the covers are “stable” for the operations. The resulting dcpo algebra has a natural universal characterization and satisfies all the inequational laws satisfied by the generating algebra. Applications include known “coverage theorems” from locale theory.
This paper studies normalisation by evaluation for typed lambda calculus from a categorical and algebraic viewpoint. The first part of the paper analyses the lambda definability result of Jung and Tiuryn via Kripke logical relations and shows how it can be adapted to unify definability and normalisation, yielding an extensional normalisation result. In the second part of the paper the analysis is refined further by considering intensional Kripke relations (in the form of glueing) and shown to provide a function for normalising terms, casting normalisation by evaluation in the context of categorical glueing. The technical development includes an algebraic treatment of the syntax and semantics of the typed lambda calculus that allows the definition of the normalisation function to be given within a simply typed meta-theory.
Solves the decision problem for the simply typed lambda calculus with a strong binary sum, or, equivalently, the word problem for free Cartesian closed categories with binary co-products. Our method is based on the semantic technique known as “normalization by evaluation”, and involves inverting the interpretation of the syntax in a suitable sheaf model and, from this, extracting an appropriate unique normal form. There is no rewriting theory involved and the proof is completely constructive, allowing program extraction from the proof.
This book is an attempt to give a systematic presentation of both logic and type theory from a categorical perspective, using the unifying concept of fibred category. Its intended audience consists of logicians, type theorists, category theorists and (theoretical) computer scientists.
We introduce a notion of Grothendieck logical relation and use it to characterise the definability of morphisms in stable bicartesian closed categories by terms of the simply-typed lambda calculus with finite products and finite sums. Our techniques are based on concepts from topos theory, however our exposition is elementary.
A functor category semantics for higher-order abstract syntax is proposed with the following aims: relating higher-order and first order syntax, justifying induction principles, suggesting new logical principles to reason about higher-order syntax
We give a new characterization of lambda definability in Henkin models using logical relations defined over ordered sets with varying arity. The advantage of this over earlier approaches by Plotkin and Statman is its simplicity and universality. Yet, decidability of lambda definability for hereditarily finite Henkin models remains an open problem. But if the variable set allowed in terms is also restricted to be finite then our techniques lead to a decision procedure.
In earlier work, we used a typed function calculus, XML, with dependent types to analyze several aspects of the Standard ML type system. In this paper, we introduce a refinement of XML with a clear compile-time/run-time phase distinction, and a direct compile-time type checking algorithm. The calculus uses a finer separation of types into universes than XML and enforces the phase distinction using a nonstandard equational theory for module and signature expressions. While unusual from a type-theoretic point of view, the nonstandard equational theory arises naturally from the well-known Grothendieck construction on an indexed category.
The type-theoretic explanation of modules proposed to date (for programming languages like ML) is unsatisfactory, in that it fails to reflect the distinction between compile-time, when type-expressions are evaluated, and run-time, when value-expressions are evaluated. This paper proposes a new explanation based on “programming languages as indexed categories” and illustrates, as an application, how ML should be extended to support higher order modules. The paper also outlines a methodology for a modular approach to programming languages, where programming languages (of a certain kind) are identified with objects in a 2-category and features are viewed as 2-categorical notions.
En hommage à Alexandre Grothendieck.
This chapter discusses that relating constructive mathematics to computer programming seems to be beneficial. Among the benefits to be derived by constructive mathematics from its association with computer programming, one is that you see immediately why you cannot rely upon the law of excluded middle: its uninhibited use would lead to programs that one did not know how to execute. By choosing to program in a formal language for constructive mathematics, like the theory of types, one gets access to the conceptual apparatus of pure mathematics, neglecting those parts that depend critically on the law of excluded middle, whereas even the best high level programming languages so far designed are wholly inadequate as mathematical languages. The virtue of a machine code is that a program written in it can be directly read and executed by the machine. The distinction between low and high level programming languages is of course relative to the available hardware. It may well be possible to turn what is now regarded as a high level programming language into machine code by the invention of new hardware.
Unpublished manuscript.
If you have a LaTeX document which
you will run into the problem that
Gerby addresses these problems by providing an online tag-based view, instead of just having a big PDF. Gerby is tailored towards making large online textbooks and reference works more accessible.
In case you were wondering, a gerbe is a kind of stack (in the mathematical sense), and the software was originally meant for the Stacks project.
A Handbook of Categorical Algebra is designed to give, in three volumes, a detailed account of what should be known by everybody working in, or using, category theory. As such it will be a unique reference. The volumes are written in sequence, with the first being essentially self-contained, and are accessible to graduate students with a good background in mathematics. Volume 1, which is devoted to general concepts, can be used for advanced undergraduate courses on category theory. After introducing the terminology and proving the fundamental results concerning limits, adjoint functors and Kan extensions, the categories of fractions are studied in detail; special consideration is paid to the case of localizations. The remainder of the first volume studies various ‘refinements’ of the fundamental concepts of category and functor.
Homotopy type theory is a new branch of mathematics that combines aspects of several different fields in a surprising way. It is based on a recently discovered connection between homotopy theory and type theory. It touches on topics as seemingly distant as the homotopy groups of spheres, the algorithms for type checking, and the definition of weak
We characterise the polarised evaluation order through a categorical structure where the hypothesis that composition is associative is relaxed. Duploid is the name of the structure, as a reference to Jean-Louis Loday’s duplicial algebras. The main result is a reflection
Le texte présente les fondements d’une théorie du groupe fondamental en Géométrie Algébrique, dans le point de vue “kroneckerien” permettant de traiter sur le même pied le cas d’une variété algébrique au sens habituel, et celui d’un anneau des entiers d’un corps de nombres, par exemple.
The text presents the foundations of a theory of the fundamental group in Algebraic Geometry from the Kronecker point of view, allowing one to treat on an equal footing the case of an algebraic variety in the usual sense, and that of the ring of integers in a number field, for instance.