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: learning: questions

Topic: Locally closed cartesian categories

John Baez (Mar 17 2025 at 16:39):

On Mastodon, Juli O'Connor asked:

Why is it usually said that the internal language of a LCCC is extensional dependent type theory (that is, dependent type theory with a rewrite rule making typal equalities judgemental), and not that the internal language of a LCCC is a dependent type theory where all equality types are propositions?

Like, I get that in such a setting you can assume the rewrite rule and not create any contradictions. But with the rewrite rule you have don't have decidable type checking, and without the rule you do. I mean, you're basically just left with something like Lean, where you have to explicitly rewrite over any equalities.

I don't know. I feel like I shied away from the undecidability of it all, but after thinking about it some more, I don't see why that part is even mentioned much. It just seems distracting compared to the actual utility of knowing that this is the internal language of an LCCC.

Ryan Wisnesky (Mar 17 2025 at 17:31):

To my way of thinking, to have a type of propositions at all requires a subobject classifier in the categorical model, which LCCCs do not necessarily have; without that, you can instead perform "equality reflection" to turn equalities in the type theory into equalities in the model, which makes the models extensional.

Madeleine Birchfield (Mar 17 2025 at 17:52):

Ryan Wisnesky said:

To my way of thinking, to have a type of propositions at all requires a subobject classifier in the categorical model, which LCCCs do not necessarily have.

Juli O'Connor's question is not about having a type of propositions, it's about having axiom K/UIP (equalities are propositions) vs equality reflection.

Ryan Wisnesky (Mar 17 2025 at 19:21):

Indeed: if you don't have a type of propositions / subobject classifer in your LCCC, you must take equality reflection as a meta-theoretic axiom to interpret equality. If you do have a type of propositions, because say you are in a topos, then you don't need to use a meta-theoretic rule such as equality reflection, you can use an actual proposition (object level) such as K/UIP as an axiom (or not an axiom).

Ryan Wisnesky (Mar 17 2025 at 19:35):

To put it another way, in my opinion the reason LCCCs are a model of extensional dependent type theory (no type Prop), rather than intensional dependent type theory (with a type Prop), is that the latter requires the structure of a sub-object classifier to interpret the type of propositions (which isn't present in an arbitrary LCCC). Whereas the former can still interpret equalities, but not Prop itself, using equality reflection. But maybe I'm not understanding the question, or rusty with my type theory.

Madeleine Birchfield (Mar 17 2025 at 19:39):

Ryan Wisnesky said:

To put it another way, in my opinion the reason LCCCs are a model of extensional dependent type theory (no type Prop), rather than intensional dependent type theory (with a type Prop)

Intensional dependent type theories don't need to have universes or a type Prop either.

Ryan Wisnesky (Mar 17 2025 at 19:53):

Ok, sure, you don't necessarily need all Props in an intensional type theory but there should at least be an identity prop; to interpret the identity prop without a sub-object classifier (such as in an LCCC) you need a rule like equality reflection.

James Deikun (Mar 18 2025 at 02:14):

Axiom K doesn't mention a type of propositions; nor does UIP. UIP explicitly spells out that equality types are (-1)-truncated.

Mike Shulman (Mar 18 2025 at 16:23):

Correct; dependent type theory with identity types (defined by J) and UIP but no universes or subobject classifier is a perfectly good theory that can serve as an internal language for LCCCs.

Mike Shulman (Mar 18 2025 at 16:25):

As to Juli's original question, I would respond: why do you think that

it [is] usually said that the internal language of a LCCC is extensional dependent type theory

?

Madeleine Birchfield (Mar 18 2025 at 16:34):

Mike Shulman said:

Correct; dependent type theory with identity types (defined by J) and UIP but no universes or subobject classifier is a perfectly good theory that can serve as an internal language for LCCCs.

There's also this paper which proves the equivalence of extensional type theory and intensional type theory with UIP and function extensionality

https://www.sciencedirect.com/science/article/pii/S0304397524006686

Mike Shulman (Mar 18 2025 at 16:37):

Morita equivalence.

Madeleine Birchfield (Mar 18 2025 at 16:39):

Mike Shulman said:

As to Juli's original question, I would respond: why do you think that

it [is] usually said that the internal language of a LCCC is extensional dependent type theory

?

I wonder, how much of this confusion comes from the nLab previously using "extensional type theory" to refer to type theories with UIP? From the [[extensional type theory]] article:

Note: For a while, the nLab incorrectly used “extensional type theory” to refer to what we now call set-level type theory. If you encounter uses of this sort, please correct them.

Patrick Nicodemus (Mar 22 2025 at 13:58):

This is a bit of a tangent but I feel that category theory as a semantic model does not model dependent types as faithfully as we might want it to, basically because category theory does not provide a primitive and basic notion of "a family of objects parameterized by another object." For example, a basic construction in category theory is the Grothendieck construction which takes a pseudo-functor $\Psi : \mathbf{B}^{\rm op}\to \mathbf{Cat}$ and tells us how to construct a Grothendieck fibration $p : \mathbf{E}\to\mathbf{B}$ from it. If one tries to state and prove such a theorem in the internal language of an elementary topos, one has to give a notion of "a family of small categories indexed by the small category $\mathbf{B}$" which
either one cannot prove it or rather one ends up formulating it in such a way that it becomes a near-tautology.
To me, $\Psi : \mathbf{B}^{\rm op}\to \mathbf{Cat}$ is somehow a more faithful representation of the concept of "a family of categories indexed by a category" than a fibration.

Maybe the key point here is that in dependent type theory, $\Sigma$-types are a nontrivial language feature which allows one to prove theorems analogous to what the axiom of replacement allows you to prove in set theory. But in category theory we essentially model dependent types by their corresponding $\Sigma$-type. (I understand that this is not always literally true, because in the fibrational semantics there are additional conditions that need to be satisfied.)

So does anyone know of any interesting models for dependent type theory where the semantics of "indexing" is different than a morphism in a category?

Mike Shulman (Mar 22 2025 at 23:34):

Indeed, the way we actually interpret dependent type theory is usually by using one of the [[categorical models of dependent types]].

Josselin Poiret (Mar 24 2025 at 10:34):

Patrick Nicodemus said:

If one tries to state and prove such a theorem in the internal language of an elementary topos, one has to give a notion of "a family of small categories indexed by the small category $\mathbf{B}$" which

I don't think this is true: grothendieck fibrations are definitively distinct definitions from just pseudo functors into $\mathbf{Cat}$, even using "the internal language of an elementary topos" (which I think you just mean constructive logic)

Josselin Poiret (Mar 24 2025 at 10:35):

see any formalization of the two concepts in your favorite proof assistants (self-plug, you can see the definition of an opfibration in agda/cubical here)

Mike Shulman (Mar 24 2025 at 19:23):

It depends on what doctrine you take your "internal language of an elementary topos" in. If it's a dependent type theory like Agda, then yes you can define a notion of "pseudofunctor into Cat" that's distinct from a fibration, at least if you assume some universes (which an arbitrary elementary topos doesn't have) or are willing to operate a bit at the meta-level and talk about indexed families of types without a universe to internalize them. But the traditional internal language of an elementary topos is in the doctrine of higher-order logic, which doesn't have dependent types, so there is no real way to say "pseudofunctor into Cat".

Morgan Rogers (he/him) (Mar 25 2025 at 10:21):

I remember there being a comparison between internal presheaves in the Elephant and internal discrete opfibrations over an internal category, but searching my copy for "presheaf" turns up almost no results. I hadn't noticed until now that Johnstone seems to reserve this term for the localic case.

Patrick Nicodemus (Mar 25 2025 at 16:38):

Josselin Poiret said:

I don't think this is true: grothendieck fibrations are definitively distinct definitions from just pseudo functors into $\mathbf{Cat}$, even using "the internal language of an elementary topos" (which I think you just mean constructive logic)

I can clarify. First, what Mike said is closer to what I meant. Second, when I said "it becomes a near tautology", this was a misleading statement, what I meant was that they are semantically very similar, if you understand the semantics of a type familyB : A -> Type as being interpreted as a projection morphism pi : B -> A in an elementary topos, where the fibers are encodings of the type families, then the part of the Grothendieck construction which talks about the objects is semantically a truism. (If you assume a universe object in your topos, they have different semantics. This is a good semantics for a type theory where the universe itself is a type, it is incomplete semantics if you have a type theory where Type is a Kind and not a type, where Kind is a simpler and more restrictive sort than Type)

I think the correspondence between families of sets B : A -> Set and projections pi : B -> A is an interesting and nontrivial one. The ability to prove such an equivalence requires some logical strength in the underlying theory, in ZFC this is the replacement axiom. I am suggesting that it would be interesting/important to study models where it is clear how such a correspondence could fail, and the LCCC model cannot really illuminate this for us because the correspondence becomes trivial. (Similarly to how the strong extensionality properties of topos theory make it not a great fit for studying type theories which lack functional extensionality, propositional extensionality and so on.)

Patrick Nicodemus (Mar 25 2025 at 16:52):

Mike Shulman said:

Indeed, the way we actually interpret dependent type theory is usually by using one of the [[categorical models of dependent types]].

I am familiar with most of these models, but not all. I would have to think individually about them to see whether they satisfy my objection, because some of them are pretty close to just the fiber bundle model but with a level of indirection (e.g., for a fibration that models dependent type theory, there is often a "comprehension" functor that allows us to reflect types from the total category of the fibration into the base category of types, equipped with a projection morphism. If the base category is a category of types/objects modelling types, then this is just the fiber bundle model in different dress. If it is a category of contexts, this is is a bit better. But a "context" is not really a semantic notion so perhaps this is wandering from the point.)

Note that the first paragraph of the page you linked summarizes the various models in precisely the terms I am criticizing here.

Mike Shulman (Mar 25 2025 at 17:25):

The introduction to that nLab page is written assuming that you're starting from a plain category in which the only notion of "family of objects" is the "fibered" one $\pi:B\to A$, and your only concern is to deal with coherence problems. This is the practical approach, not the philosophical one, since that's the way these things usually arise in practice. But these models are also relevant to the philosophical question, because if you're in a situation where you do have an "indexed" notion $B:A\to \rm Set$, you can take the "comprehension operation" to be the Grothendieck construction that takes an indexed family to a fibered one. For instance, in a CwF model, you would take $\mathrm{Ty}(A)$ to be the set of functions $A \to \rm Set$, and for $B:A\to \rm Set$ the comprehension $A;B$ is the "total space" $\coprod_{a\in A} B(a)$ with its projection down to $A$.

Mike Shulman (Mar 25 2025 at 17:43):

Patrick Nicodemus said:

The ability to prove such an equivalence requires some logical strength in the underlying theory, in ZFC this is the replacement axiom

Whether or not that's true depends on what you mean by "a function $B:A\to \rm Set$". You need replacement if "a function $B:A\to \rm Set$" means a two-variable formula $\varphi(x,y)$ such that for all $x\in A$ there exists a unique set $y$ such that $\varphi(x,y)$. But this isn't usually what people mean by "a function $B:A\to \rm Set$", among other reasons because it's a metatheoretic object rather than a mathematical one. If you want "a function $B:A\to \rm Set$" to be an object of ZFC, then you have to define it to be something like a set $B$ of ordered pairs such that for all $x\in A$ there exists a unique set $y$ such that $(x,y)\in B$. And with this definition, you don't need replacement to prove the correspondence to projections $\pi : B'\to A$; you can just define $B' = \{ (x,z) \mid x\in A \land \exists y. ((x,y)\in B \land z\in y) \}$, which doesn't need replacement to prove it is a set.