Depending on Category Variables

There has been a bunch of great work on directed type theory lately, where you talk about types with groupoid structure, as you do in homotopy type theory, but types with category structure.

Riehl-Shulman is the one paper I almost understand like 75% of, after staring at it for a long time. Also Nuyts's work also seeming very interesting although I definitely don't understand the details deeply there.

Despite both of those existing, I'm going to talk a little a bit about what I've been thinking about lately on the topic, even at the risk that it might be subsumed by something already in the literature — because if I understand precisely how, that would be progress for me understanding what's going on, anyway.

Why Is Directed Type Theory Hard, Anyway

As far as I can tell, the crux of why it isn't easy to come up with a theory of types-with-categorical structure is you don't get dependent type constructors for free from the structure of Cat; because no matter how much you wish it was, Cat just isn't locally cartesian closed. An easy counterexample is seeing that a particular pushout is not preserved by pullback. So since the pullback functor doesn't preserve all colimits, it doesn't have a right adjoint, so we don't have $\Pi$ types.

The pushout is taking two morphisms, thought of as going $A \to B$ and $B \to C$ and joining them in the middle; the structure of Cat forces their composite $A \to C$ to exist. But then if we take the pullback of this whole pushout diagram along the inclusion of $A \to C$ into the commutative triangle, we get a non-pushout diagram that shows how $A$ and $C$ are included in the morphism $A\to C$ — but there's nothing in the inputs to that pushout-attempt that explains why there should be an actual morphism between $A$ and $C$ as opposed to just two naked objects. The pullback erased exactly the collateral information (the other two morphisms) that induced its existence.

How Riehl-Shulman deal with this is by simply refraining from trying to make every type a category; there is some graph-like structure on every set arising from the axiomatization of the interval, but only some types admit composition — namely the 'Segal types' described in the paper — and further only some of those have a kind of univalence-like property that says that isomorphism means equality. ('Rezk types')

A Less Ambitious Direction

But what I've been thinking about lately isn't even trying to equip every type in a type theory with some almost categorical structure and then fishing out the ones that are genuinely categories. To be entirely honest, I'm still a little unclear what I am doing, but I'll describe it as best as I can given what I know.

What I do want to have is

a reasonable syntactically presentable proof theory with
well-behaved dependent types, and
some notion of hypotheses of a 'proposition' which is a category
whose consistency is guaranteed by some reasonable semantics

So I want to have some understanding of the meaning of sequents like \[\alpha : \C, \beta : \D \prov A(\alpha, \beta) : \rtype \] where $\C, \D$ are categories. But also I will eventually want to be able to imagine types depending on ordinary variables at ordinary types, so I'll have two zones, something like \[\alpha : \C, \beta : \D; x : A(\alpha, \beta) \prov B(\alpha, \beta, x) : \rtype \]

...Not really a theory of directed types in the same way

One thing that's a non-requirement — which I will just state hand-wavingly — is that terms $M$ in \[\alpha : \mathbf{2} \prov M : A \] (when $A$ doesn't depend on the variable $\alpha$) look anything like 'morphisms/paths/etc. in the type $A$'. This is a key difference from at least Riehl-Shulman, and I think most other attempts to have basically 'all the types' in the type theory have some directed structure. I think am going to inevitably find that $A$ depending on $\alpha$ has some extra structure, but it's going to be of a somewhat different flavor.

...Not just presheaf categories

Another non-goal is the notion that \[\alpha : \C \prov A(\alpha) : \rtype \] means that $A$ is merely a functor $\rset^\C$, with all structure on that type coming from the structure of the category $\rset^\C$. This seems like an extremely tempting, natural answer to the question "how would I design a syntax for variables of category type appearing in a context", because we know that $\rset^\C$ has a ton of useful structure; presheaf categories are locally cartesian closed, for one thing. The reason I want to do something other than that has to do with function types and substitution.

An elementary yoneda-lemma computation tells us what the exponential must look like in functor categories into $\rset$. If we have $F, G : \rset^\C$ and we want to know what $F \imp G : \rset^\C$ looks like, well, for any object $c \in \C$, we have \[(F \imp G)(c) = \hom(\C[c, \dash], F \imp G) = \hom(\C[c, \dash] \x F, G)\] This means if we had a function type \[\alpha : \C \prov A(\alpha) \imp B(\alpha) : \rtype \] and we wanted to have a syntactic notion of substitution of an object $c \in \C$ for the variable $\alpha$, it would be wrong to define \[ [c/\alpha](A(\alpha) \imp B(\alpha)) = (A(c) \imp B(c)) \] because the Kripke-esque "for all future worlds" inherent in the $\C[c, \dash] \x \cdots$ needs to be accounted for. Actually we would need to do something more like \[ [c/\alpha](A(\alpha) \imp B(\alpha)) = \forall d : \C . \forall g : c \to d . (A(d) \imp B(d)) \]

What To Do Instead?

It struck me that this pair of quantifiers felt a lot like what happened with the semantics of shift operators. Consequently, maybe I want to have a different underlying notion of function type that corresponds to "functions in the representation language", and take this quantification over objects of the category seriously as a propositional connective in the language being represented.

And, thankfully, there is a reasonable categorical notion by which to interpret universal (and existential) quantification over objects of a category: (co)ends! But the kind of thing you take a (co)end over is a functor taking two arguments, one at $\C$ and one at $\C^\op$. So I'm going to make a guess that the meaning of a context \[\Delta = \alpha_1 : \C_1, \ldots, \alpha_n : \C_n\] is actually \[\ll\Delta\rr = (\C_1 \x \C_1^\op) \x \cdots, (\C_n \x \C_n^\op)\] and the meaning of $\Delta \prov A : \rtype$ is a functor from $\ll\Delta\rr$ to $\rset$.

This means that I could imagine a type formation rule \[ {\Delta \prov A : \rtype \qquad \Delta \prov B: \rtype \over \Delta \prov A \to B : \rtype} \] because if $\ll A\rr : \ll\Delta\rr \to \rset$ and $\ll B\rr : \ll\Delta\rr \to \rset$, then we can define a functor by \[ \ll A \to B \rr(\bar c) = \ll A \rr(\tilde c) \to \ll B \rr(\bar c) \] \[ \ll A \to B \rr(\bar f) : (\ll A \rr(\tilde c) \to \ll B \rr(\bar c)) \to (\ll A \rr(\tilde d) \to \ll B \rr(\bar d))\] \[ \ll A \to B \rr (\bar f) = \lambda h . \ll B \rr(\bar f) \o h \o \ll A\rr(\bar f) \] where $\bar c = ((c_1, c'_1), \ldots, (c_n, c'_n))$ and $\tilde c = ((c_1', c_1), \ldots, (c'_n, c_n))$ and and $\bar f = ((f_1, f'_1), \ldots, (f_n, f'_n))$ for any $c_i \in \C_i, c'_i \in \C^\op_i$ and any $f_i : c_i \to d_i \in \C$ and $f'_i : d'_i \to c'_i \in \C$. (note the swapped arguments being fed to $A$!)

Also we could write down a type formation rule for the universal quantifier \[ { \Delta, \alpha : \C \prov A(\alpha) : \rtype \over \Delta \prov \forall \alpha : \C . A(\alpha) : \rtype} \] where the semantics of the rule can be realized with just currying.

I certainly don't know all of the details of how this works out, but I have a bunch of ideas that seem coherent so far. At least in the simply-typed case, the semantics of a term judgment \[ \Delta ; \Gamma \prov M : A \] is that $\ll M \rr$ should be an inhabitant of the end \[\int_{\bar c \in \ll\Delta\rr} \ll\Gamma\rr(\tilde c) \to \ll A \rr(\bar c)\] and you can write down existential quantifiers over category variables as well, and all their semantics works out and all the terms get interpreted at the right types because ends and coends satisfy all kinds of nice laws.

Of course, where things get tricky is dependent types! But I've seen some very promising things happen if you decorate term variables with just a little more information. Maybe by next week I'll have something worked out well enough to talk about...