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: category theory

Topic: CwF of presheaves

Tom Hirschowitz (Feb 13 2024 at 16:35):

With @Ambroise and my dad, we've constructed a category with families of presheaves, analogous to Lawvere's hyperdoctrine of presheaves: are we reinventing the wheel?

The base category is $𝐂𝐚𝐭$, and a type over a context $ℂ ∈ 𝐂𝐚𝐭$ is a functor $ℂ → 𝐒𝐞𝐭$.
Reindexing is by precomposition.

A term of type $A\colon ℂ → 𝐒𝐞𝐭$ is a global section, i.e., a natural transformation $1 → A$.
Reindexing is by whiskering.

If our calculations are correct, we've proved that the category of elements construction gives context extension, and that left extension gives dependent sums.

A bit more precisely, the category of elements $\{ A \}$ is the extended context, the projection $∂¹_A$ is… the projection, and the global section $∂²_A$ given by the comma category defining the category of elements is the “variable” term, as in the following diagram.

Screenshot_2024-02-13_17-29-37.png

(I can sketch dependent sums in a bit more detail if people are curious.)

Has anyone seen anything like this in the literature?

Vincent Moreau (Feb 13 2024 at 16:54):

Hi Tom, I have a very simple question. At the end of "Syntax and semantics" by Martin Hofmann, there is the presheaf cwf for a given category $K$. Its base category is $[K^{\mathrm{op}}, \mathbf{Set}]$ and a type on $P$ is a presheaf on its category of elements. Is this presheaf cwf somehow a sub cwf of yours, or more generally, is it related?

Josh Chen (Feb 13 2024 at 17:37):

This looks like the structural part of Hofmann and Streicher's groupoid interpretation of type theory, lifted to categories instead of groupoids and restricting types to the discrete fibrations.

Ivan Di Liberti (Feb 14 2024 at 02:27):

Tom Hirschowitz said:

Has anyone seen anything like this in the literature?

In the current version of my paper with Greta, this appears as 5.3.6 (which is a very short Rmk, but the whole section prepares for it). This arXiv version is a tiny bit outdated at this point, we hope to push the new version in the next month or so.

Mike Shulman (Feb 14 2024 at 03:26):

With Set-valued functors generalized to Cat-valued functors, this appears in the "Semantics" section of Licata and Harper's paper "2-dimensional directed type theory" and in Dan Licata's PhD Thesis, albeit without the language of CwFs.

Tom Hirschowitz (Feb 14 2024 at 07:40):

Great! Thank you all for the pointers. @Vincent Moreau Intriguing question... but I don't know the answer yet.

Tom Hirschowitz (Feb 14 2024 at 09:15):

@Ivan Di Liberti it looks like this is not quite the same as our construction. Am I right that in your case, the projection functor from terms to types has as image only identity discrete fibrations?

Ivan Di Liberti (Feb 14 2024 at 12:53):

I might have misunderstood what you do, it's easier for me to talk about what we do. Contexts are categories, types are presheaves, context-extension is the category of elements.

Ivan Di Liberti (Feb 14 2024 at 12:57):

A term will look like a "global element" of a presheaf, and the projection is just giving you back the presheaf.

Tom Hirschowitz (Feb 14 2024 at 15:51):

Ok, then it's indeed the same thing, and I'm reading you wrongly. I thought your functor $∑_{⊤}\colon 𝒦/1 → 𝐃𝐅𝐢𝐛$ mapped any object to the identity discrete (op?)fibration on it, which seemed to entail that terms were essentially the same as contexts. So how should I read the triangle above Defn 5.3.5? Or maybe that's not the triangle I should be looking at?

Ambroise (Feb 14 2024 at 17:28):

What is $\mathcal{K}/1$? is it isomorphic to $\mathcal{K}$ ?