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: Identity extension

Mike Shulman (Aug 27 2025 at 07:21):

Continuing on from the other topics about parametricity, I'd like to propose a framework for talking about identity extension that, I think, makes things more clear for me. In particular, it gives a precise and more general sense for a specific model to "be parametric".

Now the specific kind of model that can "be parametric" is not a model of system F alone, but rather of system F with a "logic over it". There are a lot of ways one might do this, such as the purely binary one in the Abadi-Cardelli-Curien paper, but I find it more familiar and natural to allow arbitrary predicates. I think I would formalize this as a pair of fibrations.

• At the bottom is a finite-product category of "kinds", with two base kinds $\ast$ (types) and $\omega$ (propositions), and in which all exponentials such as $\ast \to \ast\to \ast\to\omega$ exist (predicates).
• Fibered over this is a CCC of "types", with type variables of kind $\ast$, and $\forall$-quantifiers over $\ast$. Note that the propositions and predicates are irrelevant to this layer.
• Fibered over this is another CCC (perhaps posetal) of "predicates", with equality predicates satisfying their usual rules, variables of predicate kinds such as $\ast \to \ast \to \ast \to\omega$, and $\forall$-quantifiers over $\ast$ and over all types.

Maybe this isn't quite right, but I think something like it should be sensible. Of course there is a corresponding syntactic theory of such things.

Now given any such "logic-enriched model of system F" we can construct a new model of system F (without logic) whose types are those of our original model equipped with a relation (say binary). This is the usual logical relations construction. Since this relational model is a model of system F, there is a map to it from the initial model of system F, and therefore in particular any definable type-in-context is interpreted by a relation-in-context. We say our original logic-enriched model satisfies identity extension if this relational interpretation of every definable type-in-context is equality.

Mike Shulman (Aug 27 2025 at 07:27):

A framework like this would allow us to say (and presumably prove) things like "in any logic-enriched model satisfying identity extension, the interpretation of any definable transformation between definable functors is natural".

And on the other hand we could interpret particular "proofs" of identity extension as constructions of particular models where it holds, such as Neel's mutually recursive PERs-and-relations model, or Reynolds' original mutually recursive sets-and-relations model.

And finally, we could also make precise negative statements like "the initial model of system F, equipped with the logic of set-theoretic relations on closed terms, does not satisfy identity extension".