4
$\begingroup$

Consider intensional Martin-Löf type theory with judgmental $\eta$ rule for dependent product types. Is there a model of it where function extensionality fails?

$\endgroup$
1
  • $\begingroup$ Here's a proof in Agda $\endgroup$ – ice1000 May 17 at 0:31
6
$\begingroup$

The simplest one that I know about is the $\text{Set}$-based polynomial model ("container" model). Here, every context is interpreted as a family of sets, i.e. a $Q : \text{Set}$ together with an $A : Q \to \text{Set}$. We can view this as a set of questions together with sets of possible answers for each question, or a request-response protocol with at most two messages sent. Certain game semantics generalize this to arbitrary number of interactions in a protocol.

A morphism between $(Q, A)$ and $(Q', A')$ is a function $f : Q \to Q'$ with $g : (q : Q) \to A'\,(f q) \to A\,q$. So this is not a usual morphism of families, because we map answers in the backwards direction. Again, this can be viewed with the game/protocol intuition, as a synchronous translation between two protocols. The translator gets $q : Q$ from the "domain" agent, computes $f\,q$ and feeds it to the "codomain" agent, then receives an answer in $A'\,(f\,q)$ and translates it back.

Roughly speaking, most of the polynomial model of MLTT works by taking a plain $\text{Set}$ model and the opposite of a simply-typed "fibered" $\text{Set}$ model, and gluing them together. We need to take opposites of type constructions because of the flipping of mapping directions in answers. So when modeling the answer components, products become coproducts, the unit type becomes the empty type, and so on.

Function types and $\Pi$ types are an exception to this scheme, where there is non-trivial interaction between the question and answer components of the model. See this for the simply typed case. See Pi.agda from this for a formalization of the dependent $\Pi$ case, or this for the same in a more general setting with heavier abstractions.

Regarding the failure of function extensionality: semantic $\Pi$ inhabitants can be viewed as bidirectional functions with forwards and backwards mapping components. However, the function application always projects out and applies the forwards component. Hence, if we have $(a : A) \to f\,a = g\,a$, this only expresses that $f$ and $g$ have the same forwards action, and does not say anything about the backwards actions. So $f = g$ generally does not follow.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy