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

Topic: Semantics of function extensionality

Valery Isaev (Aug 15 2021 at 22:02):

Are there any models of type theory in which function extensionality fails (well, except for the syntactic one)? In categorical semantics it is always true. Is there some version of the categorical semantics in which it does not hold?

Nathanael Arkor (Aug 15 2021 at 22:05):

In her thesis Polynomials and Models of Type Theory, Tamara von Glehn constructs a model of dependent type theory that does not satisfy function extensionality, using polynomial functors.

Sam Speight (Aug 15 2021 at 23:31):

And some models from game semantics.

Mitchell Riley (Aug 16 2021 at 00:00):

Nathanael Arkor said:

In her thesis Polynomials and Models of Type Theory, Tamara von Glehn constructs a model of dependent type theory that does not satisfy function extensionality, using polynomial functors.

Formalised by András Kovács here: https://github.com/AndrasKovacs/polynomial-model if you're into that kind of thing.

Mike Shulman (Aug 16 2021 at 00:49):

There's a somewhat trivial model that violates function extensionality in Garner's On the strength of dependent products in the type theory of Martin-Löf (section 4): replace the "real" exponential by two copies of itself.

Mike Shulman (Aug 16 2021 at 00:50):

Whether this rule "always" holds in categorical semantics depends on the definition of "categorical semantics" -- if by the latter you mean semantics where exponentials are interpreted by categorical exponentials, then of course funext always holds by definition, but you can also write down what a categorical semantics of type theory without funext would be, and then build models of it as have been mentioned.

Reid Barton (Aug 16 2021 at 11:31):

The next 700 syntactical models of type theory uses a similar method to obtain models of type theory satisfying $\neg \mathrm{funext}$ and various other forms of anti-extensionality.

Jon Sterling (Aug 31 2021 at 22:47):

Reid Barton said:

The next 700 syntactical models of type theory uses a similar method to obtain models of type theory satisfying $\neg \mathrm{funext}$ and various other forms of anti-extensionality.

I seem to recall that the "function" types in this paper are not actually exponentials (i.e. don't have an eta law). To me it is more interesting to try and violate function extensionality where functions types are actually exponentials.

Jon Sterling (Aug 31 2021 at 22:47):

(Hope I am not mixing up the papers I'm referring to!)

Mike Shulman (Sep 01 2021 at 00:49):

I think Garner's models fail the eta-rule too. I don't know of any models that satisfy eta but not funext, do you?

Jon Sterling (Sep 01 2021 at 01:21):

I think I might know one... I have to go and check if it does what I think.

Jon Sterling (Sep 01 2021 at 01:23):

I believe there is a realizability model due to Van Oosten (?), where you can generate a notion of homotopy using the codiscrete interval $\nabla{2}$ --- this models the identity type, but function extensionality fails. If I recall correctly, this would satisfy our constraints. But I hope I'm not mis-remembering.

Jon Sterling (Sep 01 2021 at 01:24):

I always felt that the other "counter-models" should be referred to as violating "non-function extensionality" rather than "function extensionality" (-:

Jon Sterling (Sep 01 2021 at 01:26):

Jonathan Sterling said:

I believe there is a realizability model due to Van Oosten (?), where you can generate a notion of homotopy using the codiscrete interval $\nabla{2}$ --- this models the identity type, but function extensionality fails. If I recall correctly, this would satisfy our constraints. But I hope I'm not mis-remembering.

There was some improvement to this by Dan Frumin (IIRC) that did model funext. Anyway, both were interesting to me for different reasons.

Kenji Maillard (Sep 01 2021 at 07:20):

A relatively simple model of $\texttt{MLTT} + \eta + \neg\texttt{funext}$ is the parametric exceptional model from this paper (section 4.2)

Bob Atkey (Sep 01 2021 at 09:53):

The polynomial functors/containers model from Tamara von Glehn's thesis has eta but not funext. I formalised it in Agda https://gist.github.com/bobatkey/0d1f04057939905d35699f1b1c323736 and @András Kovács made a tidier formalisation https://github.com/AndrasKovacs/polynomial-model

Bob Atkey (Sep 01 2021 at 09:55):

Oh, I see it linked to above. But the point is that it does support $\eta$ for $\Pi$-types.

Jon Sterling (Sep 01 2021 at 16:44):

Awesome, thanks everyone!

Mike Shulman (Sep 01 2021 at 17:05):

Someone should record this somewhere, maybe on the nlab.