What's it about?
See below for a desciption of the contents of the thesis, at four different levels of assumed background knowledge: 'Basic' (no assumed familiarity with type theory and category theory), 'Intermediate' (some familiarity), 'Advanced' (significant assumed familiarity), and 'Expert'.
Basic
Programming languages exist so we can instruct computers to make calculations. A good programming language is one that allows you to write all kinds of smart programs; but a great programming language is one that prevents you from writing stupid programs. One kind of foolishness that well-designed languages are able to prevent is ill-typedness, like trying to calculate "what's one plus purple?" That question doesn't make sense, because "purple" is not the right type of thing that we can add one to. A typed programming language keeps track of the different types of each piece of data; before ever running your code, it reads through it first and "typechecks" it: it annotates every piece of data with its type (e.g. we know the variable x is a number, the variable y is a string of characters) and will refuse to run it if it's "ill-typed" (e.g. if it contains x + y, which makes no sense because you can't add a number to a string of characters).
Modern typed programming languages have very elaborate type systems, because there are a lot more elaborate data structures that programmers might want to use (it's not just numbers and strings of characters). Type theory is the mathematical study of types: type theorists try to design really clever data types, think about how different types of data can be used, and build up mathematical tools to talk about types. This thesis is a work of type theory.
One of the exciting possibilities of type theory is interactive theorem proving. Interactive theorem proving is a new way of doing mathematics: traditionally, mathematicians have to write up their results (definitions, theorems, and proofs) in a natural language (e.g. English) for their colleagues to read and try to understand. Mathematicians, like all humans, can make mistakes; in order to check that a mathematician's work is correct, other expert mathematicians have to carefully read it and check all the details. This can be really hard and time-consuming: some mathematical proofs can be hundreds of pages long, and contain really dense and elaborate reasoning. Interactive theorem proving tries to solve this: instead of writing their proofs in English for a person to read, they instead write it in a specialized types programming language (a "proof assistant"), which has a rich enough type system to be able to express all the mathematical concepts they need. Then here's the key bit: the proof assistant language is such that, if the program/proof typechecks, that means it's correct. So there's no need for a human to laboriously check every last detail: the typechecker of the proof assistant already did! We call this process computer formalization; it's a lot more work to produce a computer-formalized proof (you have to spell out every tiny detail to satisfy the computer), but once you've done it, you can rest assured that your work is absolutely, 100% correct.
Type theorists are hard at work building better proof assistants, to try and make computer formalization easier. The purpose of this thesis is to propose a new type system, called (1,1)-directed type theory. This type system is only spelled out theoretically here, but could one day be turned into a proof assistant. Its purpose is to facilitate the formalization of results in a particular mathematical discipline called category theory. Category theory is a powerful and highly-general branch of mathematics, which is applied for all kinds of purposes. It has been formalized in several existing proof assistants, but only as a result of a ton of difficult work. The type system of (1,1)-directed type theory is specifically optimized for category theory; it manages to automate a lot of the difficult "bureaucracy" of formalizing category-theoretic results, so it doesn't require as much work.
This thesis introduces (1,1)-directed type theory, and provides a bunch of mathematical tools for reasoning about what (1,1)-directed TT can and cannot do. Remember: a great programming language is one where it's not possible to do silly things; there are some silly things we specifically don't want (1,1)-directed type theory to be capable of. Demonstrating that a programming language absolutely cannot do something is really difficult: how do you know that a really clever programmer couldn't figure out a way? In order to make those kinds of arguments, we need a sophisticated mathematical toolset known as a semantics. In addition to defining (1,1)-directed type theory and showing what it can do, this thesis also gives semantics for (1,1)-directed type theory and shows what it cannot do.
Intermediate
Many modern type theories are based on the dependent type theory of Martin-Löf. One of the characteristic features of Martin-Löf Type Theory (MLTT) are identity types: in MLTT, for any two terms s and t of the same type, we can form the type Id(s,t). This type encodes the proposition that s and t are equal: if s is equal to t, then this ought to be witnessed by some term p of type Id(s,t); if they are not equal, then the identity type Id(s,t) should be empty, there should be no terms of type Id(s,t). These identity types are crucial for interactive theorem proving, as proving equations between things is one of the main things mathematicians do.
One fundamental property of equality is symmetry: if x is equal to y, then of course y is equal to x. Identity types reflect this too: in MLTT, you can prove that terms of type Id(s,t) can be turned into terms of type Id(t,s). But what I'm interested in in this thesis is a kind of type theory known as directed type theory. In directed type theory, we want to modify the identity types of MLTT to not be symmetric. That is, directed type theory has so-called hom-types, written Hom(s,t), where it's completely possible for Hom(s,t) to be inhabited (i.e. there exists a term p:Hom(s,t)) but such that Hom(t,s) is uninhabited (there are no terms of type Hom(t,s)). Instead of representing equality, this can be interpreted as representing inequality: maybe s and t are numbers, and Hom(s,t) is the type of witnesses that s < t. Then certainly we don't want symmetry, because that would mean s < t implies t < s! Or maybe s and t represent possible states of some computer system, and Hom(s,t) is the type of processes that, when executed in state s, will result in state t. We definitely want to allow these processes to be irreversible, i.e. it's possible to go from s to t by some process, but there's no process taking you back to s from t. These are the kinds of phenomena that directed type theory is designed to model.
There's one big difficulty, though. In MLTT, the proof of symmetry (that Id(s,t) implies Id(t,s)) is done using a logical principle known as identity elimination, a.k.a. path induction, a.k.a. the J-rule. So if we want Hom-types to be "just like identity types, but asymmetric", we just toss out the J-rule, right? Well, that's "throwing the baby out with the bath water": the J-rule is also necessary to prove other things which we do want to keep. Most significantly, the J-rule is also used to prove the transitivity of identity types: if I have terms s, t, and u, and I have terms p : Id(s,t) (a proof that s equals t) and q : Id(t,u) (a proof that t equals u), then I can combine them to get a term of type Id(s,u). This "transitivity" property is one we want to keep around for Hom-types too: if s < t and t < u, then I should be able to conclude s < u; if there's a process taking me from state s to state t and another taking me from t to u, then I can just concatenate the two processes to go all the way from s to u. So our task here is to come up with a version of the J-rule for Hom-types which can prove transitivity, but cannot prove symmetry.
We do this by incorporating a modal typing discipline, which we call the polarity calculus. What we do is require every term to be decorated with a "polarity": either a plus or a minus. Then we make the restriction that the hom-type Hom(s,t) is only well-formed if s has negative polarity and t has positive polarity. Now, in this type system, a term s that doesn't contain any free variables can be freely translated between the polarities: if s has minus polarity, then there's a term -s with positive polarity, and vice-versa. But here's the key trick: variables are stuck with whatever polarity they have, and cannot be "negated" to the other polarity. So if x is an open variable (or a term containing open variables), then we're not allowed to form the term -x of opposite polarity. Why does this solve our problem about having transitivity but not symmetry? Well, the J-rule involves hom-types where one endpoint is a variable, i.e. Hom(s,x) where s is a closed term but x is an open variable. We aren't able to flip this around to form the type Hom(x,s): in order for Hom(s,x) to make sense, s must be negative polarity and x must be positive, but Hom(x,s) is the opposite. We're allowed to change the polarity of s (the term -s has positive polarity), but not so for x since it's a variable. So the proof of symmetry fails because we can't get the polarities to work out; indeed, we can do a more sophisticated argument to show that there's no way, no matter how clever we are, to use this modified J-rule to prove symmetry. Transitivity, on the other hand, doesn't require us to "flip things around", so the polarities work out fine. Thus we've succeeded at our central task: coming up with a genuinely directed type theory (at the cost of some added complexity, namely this polarity calculus).
Advanced
There's an intriguing thing one can do in Martin-Löf Type Theory: iterate identity types. That is, if we have p,q : Id(s,t), then we can form the type of identities between the identity terms p and q, Id(p,q). And given multiple elements of Id(p,q), we can ask about the type of identities between them, and so on. Every type comes equipped with an infinite tower of identities between identities between identities between.... Of course, type theorists soon wondered: what is an identity between identities? Can there actually be terms p,q : Id(s,t) where p and q are not themselves identical?
The answer was groundbreaking: the so-called Uniqueness of Identity Proofs (UIP) principle (which asserts that any such p and q must be identical, i.e. Id(p,q) inhabited) is consistent with the rules of MLTT, but independent of them. That is, you're free to either assume UIP (i.e. work in the type theory MLTT+UIP), or reject it. The latter suggestion is the starting-point of Homotopy Type Theory (HoTT), whose central axiom, univalence, logically contradicts UIP. HoTT is rich with so-called higher types, where the identity types are rich data structures, not mere propositions.
The proof of UIP's independence was done by Hofmann and Streicher, and introduced groupoid model of type theory for that purpose. One needs a model of type theory to show independence: to argue against any possible proof of UIP from the rules of MLTT, one needs to construct a model which validates all the rules of MLTT but refutes UIP. This is what was achieved with the groupoid model: it is a model of MLTT (specifically, it constitutes a category with families, a category with appropriate structure to interpret the operations of type theory), but, since the identity types are interpreted using the morphisms of a groupoid (which aren't, in general, unique), we can find counterexamples to UIP in this model.
We adapt this method for the independence proof that's critical to directed type theory: symmetry. That is, we want to design a system of directed type theory, and be sure that it's not possible to prove the Hom-types symmetric. But we can't just take the groupoid model: it's a model of undirected type theory. Instead, we modify it to the category model, which is like the groupoid model in every way, except it uses categories throughout instead of groupoids. We design our directed type theory to have semantics in the category model, and in particular we interpret the Hom-types using the morphisms of categories. The morphisms of categories are not, in general, invertible; hence we can come up with a counterexample to symmetry in the category model. Thus, the rules of our theory cannot prove symmetry. The (1,1)-directed type theory put forward in this thesis is, for this reason, designed specifically to be modelled by the category model.
But there's another reason we want to replace groupoids with categories. It was recognized early on that every type T in MLTT has the structure of a groupoid: the terms of T represent the objects of the groupoid, and, for s,t : T, the identity type Id(s,t) represents the set of morphisms from s to t. The reflexivity term refl : Id(s,s) is the identity morphism on s, and the transitivity and symmetry of identity types (both provable from the J-rule) correspond to the composition and inverse operations on morphisms possible in a groupoid. We call this a synthetic groupoid, because it's automatically a groupoid: no need to construct the objects and morphisms and composition and so on explicitly, every type we can write down in MLTT already comes equipped with this groupoid structure, as proved by the rules of MLTT. So now, consider: if we manage to make a directed type theory where symmetry is no longer provable, then this corresponds to dropping the invertibility of morphisms from the definition of groupoid. That is, every type in directed type theory has the structure of a synthetic category. In this thesis, I show how we can actually start to do synthetic category theory in the system of (1,1)-directed type theory.
Expert
In chapter 1 of this thesis, I develop a methodology for pursuing directed type theory based on generalized algebraic theories (GATs). GATs have the crucial property of always having an initial algebra. So, in particular, any extension of the GAT of categories with families will have an initial algebra, the syntax model of that particular type theory. The thesis therefore consists of a succession of type theories, capturing more and more of the category model's features. Also in chapter 1, I note the peculiarity of the groupoid model providing semantics for a synthetic groupoid theory (and the setoid model providing a semantics for synthetic setoid theory) and speculate about which GATs allow for this kind of "auto-synthesis"; the rest of the thesis consists of exploring the auto-synthetic potential of the GAT of categories.
In chapter 2, a modal typing discipline of positive and negative 'polarities' is proposed. Interpreted in the category model, this polarized type theory provides a type theory for Grothendieck fibrations and opfibrations. This polarity calculus makes it possible, in particular, to have (a "polarized" version of) dependent function types with semantics in the category model. However, in order to make these polarized Pi-types useful, we must restrict the context to be "neutral" in the appropriate sense; in the category model, the neutral contexts are precisely the groupoids. The salient features of these neutral contexts (specifically how they allow coercions between polarities) is abstractly axiomatized in the notion of a neutral-polarized CwF. Neutrality also permits us to characterize the "negative polarity" version of dependent sum types.
Chapter 3 features a developed of hom-types in this setting. The coercion operations of neutral contexts weaken the polarity calculus enough to have one term t appearing as both the (negative) domain and (positive) codomain of a hom-type, but maintains enough polarity restrictions on the J-rule to defeat the standard proof of symmetry. Indeed, we use the category model as a countermodel to show that no proof of symmetry can be given. This chapter also features a discussion of the directed analogue of various key type-theoretic concepts, including transport, the structure identity principle, and the universe of sets with its universe extensionality/univalence principle. However, the polarity calculus as stated here is too strict to allow for a "directed function extensionality": resolution of this issue is left to future work.
Chapter 4 showcases an informal style of directed type-theoretic reasoning (following the example of the HoTT Book), and applies it to perform synthetic category theory. Appropriate to our type-theoretic framework, we phrase the key universal mapping properties characteristic of category theory (e.g. in the definition of (co)products, pullbacks/pushouts, and adjoint functors) as principles of induction. This development encounters several of the limits of the present theory, suggesting avenues for future work.