Directed HoTT based on profunctors?

[Oscar Cunningham]

I've been looking at some of the papers working on Directed HoTT (the idea being that types are (∞,∞)-categories rather than mere ∞-groupoids) and to me it seems like there are two main obstacles:

 (1) Many natural constructions are not functors. In particular the equality type itself. If C is a mere category and we have an isomorphism i:(a=b) and a morphism f:b -> c we can't compose i and f to get an element of type (a=c). Indeed a and c need not be isomorphic. So we can't view (a=b) as a dependent type over C. This problem doesn't arise in undirected HoTT because constructions which aren't functorial still respect equivalence. The existing treatments of Directed HoTT face this issue by introducing a constructor that for each type C gives you a type C^core corresponding to its underlying groupoid. To me this seems not in the spirit of Directed HoTT; it's just retreating back to the safety of undirected HoTT as soon as things get tough.

 (2) If C is a type in undirected HoTT we get a nice correspondence between spaces B -> C over C and functors C -> U. In particular given a dependent type we can form its Σ-type to get a type over C and given a type over C we can look at its fibers to get a dependent type, and these processes are inverses. This appears not to work in Directed HoTT. If we let U be the category of categories then given a functor C -> U we can use the Grothendieck construction to get a category over C, but not every category over C arises in this way - only the fibrations.

I believe there may be a way to fix both these problems by using profunctors instead of functors.

This would be based on the fact that categories B -> C over a given category C are in correspondence with normal lax functors C -> Prof, where Prof is the 2-category of categories and profunctors. (See here: https://mathoverflow.net/a/245743/4613)

So my idea would be to make a Directed HoTT in which the type B -> C is still viewed as the (normal lax) functors from B to C, but dependent types are thought of as being lax functors C -> U where we're now thinking of the morphisms in U as being profunctors rather than functors. (In other words the Directed Univalence Axiom would say Hom_U(B,C) ≈ Prof(B,C).)

This immediately fixes obstacle (2) be design, and in fact it also fixes obstacle (1). A morphism f:b -> c does induce a profunctor (a=b) -> (a=c), so we can now think of (a=b) as a dependent type.

Could this idea be useful? Is anyone working on ideas like this?

(It seems that lax functors defined on higher categories fail to respect the principle of equivalence (https://golem.ph.utexas.edu/category/2009/12/the_problem_with_lax_functors.html), but that they are well defined between *double* categories. So perhaps what we would really want is for types to be ∞-tuple catgories, and for each direction of morphism in U to be the appropriate kind of profunctor. This would fit well with the fact that a classic example of a double category is that of profunctors and functors.)

[Colin Zwanziger]

Hi Oscar,

You may be interested in:

•  "A Double-Categorical Perspective on Type Universes" by Morehouse, Kavvos, and Licata
• "On the Directed Univalence Axiom" by Cavallo, Riehl, and Sattler
  

As a quick 2 cents: I think this is an interesting line of inquiry, but I don't think it should be pursued to the exclusion of approaches based on regular old functors C -> Cat. My worry is that normal, lax functors C -> Prof are more exotic and difficult to work with. There is a question of how much of type theory we can retain in this setting. For instance, in the approach based on functors C -> Cat, one can shoot for Sigma and Pi types being interpreted by left and right Kan extension. Do Kan extensions generalize to the normal, lax setting? I don't know.

Best,

Colin Zwanziger

--
You received this message because you are subscribed to the Google Groups "HoTT Cafe" group.
To unsubscribe from this group and stop receiving emails from it, send an email to hott-cafe+...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/hott-cafe/093c9958-6b69-4ee9-a7fc-3e14aaca117b%40googlegroups.com.

[Michael Shulman]

FWIW, Riehl-Shulman directed type theory
(https://arxiv.org/abs/1705.07442) solves these problems by relaxing
the requirement that all types be categories. All morphisms between
categories are functors, but non-fibrations (such as the identity
type) are classified by maps into a universe that is not itself a
category. As written this type theory only handles (oo,1)-categories,
but one should be able to write down a version for (oo,oo)-categories
based on Theta-spaces rather than simplicial spaces.

> To view this discussion on the web visit https://groups.google.com/d/msgid/hott-cafe/CAAhSxooR2NbWWx3dtAwGBXAj6tWk8Kh4HQd5Fp1QPWK0eV1ToA%40mail.gmail.com.

[Matt Oliveri]

I was also thinking that it might be nice for directed morphisms in a universe to be like profunctors. My line of reasoning was that an aspect of cubical type theory that's really really nice from an implementation perspective is that it has heterogeneous paths, which make the path spaces for for Pi and Sigma (for example) technically nice. In the style of judgments used, heterogeneous paths arise automatically, as elements of a type depending on the formal interval. The dependent type itself is a path in the universe, and thus an equivalence.

So in undirected HoTT, types provide a notion of path, and dependent (on the interval) types are equivalences, which provide a notion of heterogeneous path. If, in directed HoTT, types should be like (higher) categories and provide a notion of morphism, then by analogy, dependent types should provide a notion of heterogeneous morphism. That is, a dependent (on the interval) type should be a notion of heteromorphism. So, a profunctor? It seems, by this informal and rhetorical argument, that it might be good to think of directed lines in the universe as profunctors.

But that was pretty much the full extent of my thinking, and the Riehl-Shulman approach also uses a formal directed interval, if I understand correctly. So the technical niceness that motivated my line of thought should be available there, too.

(And really, I don't see why we shouldn't be able to define all this more-specialized higher-dimensional stuff in undirected HoTT. I like the idea that HoTT is the higher-dimensional analogue of set theory; and we do math in set theory, not "poset theory".)