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.
finegeometer (Sep 18 2024 at 02:51):Hi!
If I want to reason internally to a topos, I can work in the internal logic.
This looks like a fairly standard type theory, with axioms for funext, propositional extensionality, and quotients. I then add axioms specific to the topos I'm working with, such as the Kock-Lawvere axioms for smooth toposes, or the law of excluded middle for boolean toposes.
Now say my topos is a monoidal topos, such as presheaves on a monoidal category under Day convolution. Say I'll be working with the monoidal product and function type as extensively as regular products and functions. Then I'll want the monoidal product and function types to feel "built in" to the language, rather than axiomatized. How do I do this?
Presumably, what I want is some sort of linear dependent type theory. But which linear dependent type theory, exactly? I'd like a fairly detailed description, so a link to a paper would be preferable.
I'm happy to work informally, so I don't require that the type theory actually be implemented as a proof assistant. As long as the type theory is clearly defined, and preferably fairly simple, I'm happy.
Thanks!
Kevin Carlson (Sep 18 2024 at 04:52):Linear dependent type theory doesn't fully exist yet, though there's some considerable effort toward it (I'd just point you to the nLab, no specific knowledge of references.) That said, I think it's far from obvious that the linear type theory you get from sticking a monoidal structure onto a topos should be dependent just because the topos is dependent!
Mike Shulman (Sep 18 2024 at 07:01):I would say rather that there are a bunch of different linear dependent type theories, probably incomparable with each other, and it's not clear that any of them is uniformly better than the others.
Mike Shulman (Sep 18 2024 at 07:01):There may or may not be one in the literature that does exactly what you want; I'm not thinking of one off the top of my head.
Sam Staton (Sep 18 2024 at 07:04):Hi monoidal toposes with Day convolution, if that's what you have in mind, come up in models of "bunched type theory". An older reference is Peter O'Hearn's paper, and then Uli Schöpp and Ian Stark looked at dependently typed versions. More recently I am slightly out of the loop on the state of the art in dependent bunched type theory, I've seen @Mitchell Riley's thesis, but I don't yet know it well enough to say how much it connects to Day convolution or ordinary topos theory.
Mike Shulman (Sep 18 2024 at 07:15):Oh nice, I didn't realize there was a dependently typed version of the original bunched type theory (although I knew about Mitchell's work, which is bunched in a different way IIRC).
Mike Shulman (Sep 18 2024 at 07:15):Do you have a reference for the work of Schöpp and Stark?
Sam Staton (Sep 18 2024 at 07:36):Yes, I was thinking about Uli's thesis, Names and Binding in Type Theory.
Mitchell Riley (Sep 18 2024 at 08:50):If I remember right the Schöpp and Stark type theory builds in the assumption that the monoidal unit is terminal, because variables in any bunch are always usable. But it still might match your intended application.
Sam Staton (Sep 18 2024 at 16:16):Good point, you're right.
finegeometer (Sep 19 2024 at 01:02):Thank you! My intended application does, in fact, have the monoidal unit be the terminal object. So that should work.