Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: type theory & logic

Topic: Trying to interpret MLTT in Cat.

finegeometer (Aug 16 2023 at 15:54):

Inspired by the search for a directed version of homotopy type theory, I've been trying to interpret ordinary MLTT type theory in the 2-category of categories. It seems to almost work.

Here's what I have so far:

• To each context $\Gamma$, assign a 1-category $\llbracket\Gamma\rrbracket$.
• To each type $\Gamma \vdash X \textsf{ type}$, assign a pseudofunctor $\llbracket X\rrbracket : \llbracket\Gamma\rrbracket \to \mathbf{Cat}$.
• To each value $\Gamma \vdash x : X$, assign a lax natural transformation $\llbracket x\rrbracket : (\_ \mapsto \mathbf{1}) \Rightarrow_\mathrm{lax} \llbracket X\rrbracket$.
• For contexts, $\llbracket\cdot\rrbracket$ is the terminal category, and $\llbracket\Gamma, x : X\rrbracket = \int\llbracket X\rrbracket$; the result of applying the Grothendieck construction to $\llbracket X\rrbracket$.

This all seems to work. But I'm having trouble with pi-types. Letting $p$ be the canonical functor $\int \llbracket X\rrbracket \to \llbracket\Gamma\rrbracket$, I need a right 2-adjoint to $p^* : [\llbracket\Gamma\rrbracket, \mathbf{Cat}] \to [\int \llbracket X\rrbracket, \mathbf{Cat}]$, where those functor categories are categories of pseudofunctors and lax natural transformations. But I'm not sure this adjoint actually exists.

I think I've found references that say I'd be fine if I were working with pseudonatural transformations instead. But if I do that, I have problems with the variable rule instead.

This is where I'm stuck. I don't know if it's just that my inexperience with 2-categories has caught up to me, or if the whole idea is fundamentally flawed.

Mike Shulman (Aug 16 2023 at 16:22):

I could be wrong, but is what you need the fact that opfibrations are exponentiable morphisms in Cat?

Taichi Uemura (Aug 16 2023 at 22:25):

Exponentiability wouldn't be enough. One needs that exponentiation by an opfibtation preserved opfibrations, but I think that is false.

Mike Shulman (Aug 17 2023 at 02:35):

Yes, that's right. Exponentials by an opfibration preserve fibrations.

Mike Shulman (Aug 17 2023 at 02:49):

It's hard to get away without introducing both variances when you try to do directed type theory, which is part of what leads into the morass...

Matteo Capucci (he/him) (Aug 17 2023 at 08:06):

I'm very curious about your last remark @Mike Shulman... say one follows HoTT and then adds a type constructor

$$\dfrac{\Gamma \dashv A\, \text{type}}{\Gamma \dashv A^\circ\, \text{type}}$$

and then instead of the identity type we have a hom type with appropriately placed ops, with path induction basically coinciding with a version of Yoneda. Where does this break down?

Mike Shulman (Aug 17 2023 at 16:41):

What are the rules for elements of $A^\circ$?

Steve Awodey (Aug 19 2023 at 16:57):

Maybe it should be said, for those who don't know it, that the idea of interpreting (some version of) dependent type theory into (some variant of) Cat is not at all far-fetched, and various people have worked, and still are working, on it. The basic idea and some references are on this nLab page.