Presheaf lectures

Category theory recap

We treated categories, functors, natural transformations, and maybe also monads and monoids.

Bartosz Milewski has a blog on category theory that people are enthousiastic about. The relevant sections would be:

part one
- 1 & 3 Categories
- 7 & 8 Functors
- 10 Natural transformations
- 4 Kleisli categories (related to monads)
part three
- 4-6 Monads
- 8 Functor algebras
- 9 Monad algebras (aka Eilenberg-Moore algebras)

Another place where you can learn about monads, is in the Haskell tutorial Learn you a Haskell for great good, chapter A fistful of monads.

Presheaf lecture 1 (Nov 4, 2022)

What is an algebraic/type theory, and what is a model?

Main idea: we can specify a unisorted or multisorted algebraic theory or programming language by

specifying the syntax as an (indexed) container
specifying an equational theory.

The framework of algebraic theories then tells us automatically what it means to give a model of that theory/language.

In the lecture I used slides 6 and 7 from my recent TyDe-presentation, for which there is also a video.

Relevant resources:

Gentle introduction to some prior concepts (namely containers, indexed containers, and (indexed) container functors):

Altenkirch, Ghani, Hancock, McBride, Morris, 2009, Indexed Containers

https://www.cambridge.org/core/services/aop-cambridge-core/content/view/FB9C7DC88A65E7529D39554379D9765F/S095679681500009Xa.pdf/indexed-containers.pdf
A text about monads and universal algebra from a mathematical viewpoint, by Anthony Voutas:

"The basic theory of monads and their connection to universal algebra"

https://voutasaur.us/monad-algebra.pdf

What's nice is that he takes his time to explain everything and does not require much prior knowledge. Section 1 is a formula-free introduction, sections 2 and 3 are certainly worth the while. Sections 4 and 5 are interesting but not especially relevant.
Milewski, 3.8-9
I tried to explain the relevance to type theory in chapter 3 (section 3.1 up to and including 3.1.3) of my PhD thesis.
I also synthesized the most important ideas (including some more advanced ones) here, though with few examples: https://anuyts.github.io/files/keml-diagrams.pdf

(In both instances, my contribution is only to describe what exists.)

STLC as a multisorted algebraic theory (MAT)

See def. 8.1 of my KEML-note, although it's a bit brief.

Types can be regarded as single-variable contexts, so terms can be regarded as substitutions.

A model is then a category whose objects are syntactic contexts (but with an unimportant trick we can model syntactic contexts by different, semantic contexts) and whose morphisms are semantic substitutions.

To model the empty context (and possibly a unit type), we need a terminal object. To model context extension (and possibly pair types) we need cartesian products. So the category needs to be cartesian, which means that it has a terminal object and binary cartesian products.

To model function types, lambda-abstraction and application with beta- and eta-rules, the model needs to be cartesian closed.

In short, models of the STLC are exactly cartesian closed categories (CCCs).

Set model of the simply-typed lambda-calculus (STLC)

I don't really have a good resource here.

Presheaf lecture 2 (Nov 25, 2022)

Guarded type theory

Some resources about the type system itself are:

Nakano's original paper,
A paper by Atkey and McBride more focused on using guarded type theory,
"The clocks are ticking, no more delays!" is the one closest to what is implemented in agda --guarded. An important difference between this paper on the one hand, and both what I discussed in the lecture and what is implemented in Agda on the other hand, is that the paper has multiple clockes, whereas Agda and I assume there is always exactly one clock (time dimension) available. In that case clocks cannot be introduced, discarded, or quantified. The rule with the diamond from the paper does not apply, and "later" and "next" are not annotated by a clock, since there is only a single one anyway.

Single-clock guarded type theory can be modelled in the topos of trees, i.e. the category of presheaves over ω.

I explained the model of the guarded STLC in Psh(ω), which I don't have a good reference for but I will come back to it in the dependent case.

Parametricity

Motivation
- The book "Types and Programming Languages" (a.k.a. TAPL) by Benjamin C. Pierce, chapters 23 and 24 and prerequisites (see the dependency graph in the book's front matter). This book is also the lecture material of the Formal Systems course.
- An accessible paper about parametricity: Wadler, 1989, Theorems for Free
Reflexive graphs are presheaves:

See e.g. my PhD, example 2.3.8.

Presheaf lecture 3 (Dec 2, 2022)

Parametricity of System F(ω); Reynolds' relational model for System F and how you need reflexive graphs if you want to generalize to Fω.
- I've made use of the following presentation:
  
  https://anuyts.github.io/files/reldtt-lyon.pdf
  
  (slides 1-8 and 11-13)
- I think what I've said is quite comparable to the discussion in ch. 9 of my PhD thesis (up to and including section 9.1.2).
  
  https://anuyts.github.io/files/phd.pdf
- The corresponding papers in the literature are:
  - Reynolds' original paper: https://people.mpi-sws.org/~dreyer/tor/papers/reynolds.pdf
  - Atkey's paper for Fω: https://bentnib.org/fomega-parametricity.html
Parametricity is only interesting when we look at languages with type variables (so not the STLC, but System F(ω) or dependent types). I've noted that these are not multisorted algebraic theories (MATs) but generalized algebraic theories (GATs, the dependent generalization). I haven't defined what a GAT is, but just like for MATs, if we specify a GAT then that automatically tells us what a model of that GAT looks like. For System F(ω) and dependent types, the "infrastructural" part of such a model is a category with families (CwF). I would suggest section 3.2.1-2 of my phd thesis (and all of chapter 3 for the curious), or the sources cited there.
I've started sketching how presheaf categories constitute a CwF, and I think I was in the process of explaining what a type is in a presheaf model when the lecture ended. This would correspond to sections 4.1.1-2 of my PhD thesis (or the sources cited there). Examples 4.1.1-3 are exactly about sets, reflexive graphs, and step-indexed sets, so they are exactly the examples from the lecture.

Presheaf lecture 4 (Dec 16, 2022)

Presheaf categories are Categories with families (CwFs)
- What is a type in a presheaf category (via slices & local democracy)
- What is a term in a presheaf category (via sections of slices)
- Boring type formers
- Pair and Σ-types
Relevant resources: See below.