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 & logic

Topic: Dependent function extensionality from nondependent?

Daniël Otten (Jul 15 2025 at 09:51):

In Martin-Löf type theory with uip or axiom K we know that the dependent version of function extensionality can be derived from the nondependent one. Is this also true without uip?

Related results show that strong versions of dependent function extensionality can be derived from weak dependent versions. See also section 4.9 of the HoTT book. However I am not aware of results relating the dependent and nondependent versions without other axioms.

Madeleine Birchfield (Jul 15 2025 at 11:09):

It is possible to define the dependent function type in terms of ordinary function types, identity types, and dependent sum types with the usual inference rules involving judgmental equality in the conversion rules:

$$\prod_{x:A} B(x) \equiv \sum_{f:A \to \sum_{x:A} B(x)} \lambda x.\pi_1(f(x)) =_{A \to A} \mathrm{id}_A$$

where $\pi_1:\left(\sum_{x:A} B(x)\right) \to A$ is the first projection function of the dependent sum type $\sum_{x:A} B(x)$ and $\mathrm{id}_A$ is the identity function on $A$. I'll leave it as an exercise to prove that the above type satisfies all 5 inference rules of the dependent function type.

From here, it should be a relatively simple direct proof of dependent function extensionality from non-dependent function extensionality of the types $A \to \sum_{x:A} B(x)$ and $A \to A$.

Madeleine Birchfield (Jul 15 2025 at 11:24):

I don't know if the same can be proven in weak type theory where the conversion rules use the identity type instead of judgmental equality.

Mike Shulman (Jul 15 2025 at 15:34):

I don't believe that type satisfies $\eta$-conversion.

Madeleine Birchfield (Jul 15 2025 at 23:45):

It satisfies propositional $\eta$-conversion though: Given a function $f:A \to \sum_{x:A} B(x)$ such that $p:\pi_1 \circ f = \mathrm{id}_A$ the eliminator is given by $x:A \vdash \pi_2(f(x)):B(x)$, and composing with the introduction yields a function $\lambda x.(x, \pi_2(f(x))):A \to \sum_{x:A} B(x)$, which is equal to $f \equiv \lambda x.(\pi_1(f(x)), \pi_2(f(x))$ by ap across $p:\pi_1 \circ f = \mathrm{id}_A$. The witness that $\lambda x.(x, \pi_2(f(x)))$ satisfies the identity in the dependent sum type is given by reflexivity across $\mathrm{id}_A$.

Mike Shulman (Jul 15 2025 at 23:48):

I think the eliminator has to transport across the propositional equality $\pi_1 \circ f = \mathrm{id}_A$ to have the right type.

Mike Shulman (Jul 15 2025 at 23:50):

For a function $f:A \to \sum_{x:A} B(x)$ you actually have $x:A \vdash \pi_2(f(x)) : B(\pi_1(f(x)))$.

Madeleine Birchfield (Jul 15 2025 at 23:59):

So something like $x:A \vdash \mathrm{tr}_p(\pi_2(f(x))):B(x)$?

Mike Shulman (Jul 16 2025 at 00:00):

or more precisely $\mathrm{tr}_{\mathrm{happly}(p,x)}$

Mike Shulman (Jul 16 2025 at 00:01):

But yes.

Madeleine Birchfield (Jul 16 2025 at 00:03):

Well then the question is still open for dependent function types which satisfy judgmental $\eta$-conversion, which is what I think @Daniël Otten was asking about since the types in MLTT usually satisfy judgmental $\eta$-conversion.

Daniël Otten (Jul 16 2025 at 00:06):

If the type theory already has Pi-types then I think you do still get an equivalence with this type so if we prove function extensionality for it it should transfer. At least, if we are not interested in having a definitional computation rule for function extensionality

Daniël Otten (Jul 16 2025 at 00:08):

I think we need to assume a definitional computation rule for the nondependent version of function extensionality to get definitional beta for this new definition of Pi-type

Mike Shulman (Jul 16 2025 at 00:09):

Daniël Otten said:

I think we need to assume a definitional computation rule for the nondependent version of function extensionality to get definitional beta for this new definition of Pi-type

I would have thought that would follow instead from definitional computation for Id-elimination, since abstractions in this new Pi-type have refl as their witness.

Daniël Otten (Jul 16 2025 at 00:18):

I think you have to define the new $\lambda x.b$ as $\langle\lambda x.\pi_1 \langle x,b\rangle, \mathsf{funext}(x.\mathsf{refl})\rangle$. And then we define the new application $f a$ as $\mathsf{tr}_{\mathsf{happly}(\pi_2 f) x} (\pi_1 f a)$. Then if we have the new $(\lambda x.b) a$ we need a computation rule for funext(x.refl) to compute to refl.

Mike Shulman (Jul 16 2025 at 00:25):

Why can't you define the new $\lambda x.b$ as $\langle \lambda x. \langle x,b \rangle, \mathsf{refl}\rangle$?

Mike Shulman (Jul 16 2025 at 00:26):

assuming your non-dependent function types have definitional $\eta$

Daniël Otten (Jul 16 2025 at 00:28):

Ah of course! I was trying to write it out for weak type theory and there you need funext of a more complicated term.

Daniël Otten (Jul 16 2025 at 00:32):

Do you even need $\eta$ in that case? I think you just get $\lambda x.x$ on both sides if you do a $\beta$ reduction for $\Sigma$ inside the lambda on the left

Daniël Otten (Jul 16 2025 at 00:49):

In that case I think we get a version of $\Pi$-types with definitional $\beta$ and propositional $\eta$ with a computation rule (saying that $\eta(\lambda x.b):\lambda x.(\lambda x.b) x=\lambda x.b$ computes to refl), which is also quite a natural notion as it corresponds to the positive formulation of $\Pi$-types.

Mike Shulman (Jul 16 2025 at 01:07):

And I guess that is sufficient to make it propositionally equivalent to any other $\Pi$-types, so that funext for one implies it for the other.

Daniël Otten (Jul 16 2025 at 01:15):

Yes so this should completely answer the question: even the most naive versions of funext already imply the strongest ones. With a bonus result that $\Pi$-types already follow from $\Sigma$-types, $\to$-types, and $=$-types if you only require propositional $\eta$ with a computation rule. Thank you both!

Evan Cavallo (Jul 16 2025 at 09:01):

Just as a historical note, I checked in the TypeTopology library and the version for Π-types with η is recorded there (https://martinescardo.github.io/TypeTopology/UF.FunExt-Properties.html#778) and attributed to Voevodsky (https://github.com/vladimirias/Foundations/blob/master/Generalities/uu0.v, starting on line 2946 I believe).