How big can function spaces get without extensionality?

Question

In what follows we work in the usual formulation of Martin-Löf Type Theory including Axiom K [1]. Boldface numbers $\mathbf{n}$ denote the usual finite type with $n$ elements.

Motivation

Postulating function extensionality in Martin-Löf Type Theory (or deriving it from additional postulates such as univalence and interval types) allows one to compare the "sizes" of many function spaces: for example, it's easy to show that $\mathbf{1} \rightarrow \mathbf{0}$ has no inhabitants, while $\mathbf{1} \rightarrow \mathbf{1}$ constitutes a singleton set. The finite realm [2] looks fairly mundane, in that the function space $\mathbf{n} \rightarrow \mathbf{m}$ has size $m^n$.

The situation gets more complicated in the absence of function extensionality. One can still prove that $\mathbf{1} \rightarrow \mathbf{0}$ is empty, but what can one say about the size of function spaces $A \rightarrow B$ where $B$ is inhabited or at least non-empty? Can some such spaces get very large? Can all such spaces get very large?

Question

Consider axioms of the form $$\mathrm{big}_C : \Pi A,B:\mathcal{U}. B \rightarrow C \hookrightarrow (A \rightarrow B) $$ where $C:\mathcal{U}$ is some fixed small type and $X \hookrightarrow Y$ stands for the type of all injective maps $f: X \rightarrow Y$.

a.) For which values of $C$ does the axiom $\mathrm{big}_C$ remain consistent with Martin-Löf Type Theory?

b.) In MLTT + LEM, one cannot consistently take $C$ as $(\mathbf{1} \rightarrow \mathbf{1}) \rightarrow \mathbf{2}$, since then evaluating at $A = B = \mathbf{1}$ contradicts Cantor's theorem [3]. This doesn't seem to constrain the sizes of function spaces all that much, though, since $(\mathbf{1} \rightarrow \mathbf{1}) \rightarrow \mathbf{2}$ is itself a function space. If we assume LEM, can we take $C$ to be $\mathbb{N}$ or failing that at least $\mathbf{n+2}$ for some $n$?

edit: Thanks to the two answers so far, the answer to part b is positive , even with $C$ as $\mathbb{N}$.

[1] No bracket types or propositional truncations. I doubt it will come up, but if the distinction turns out to matter, assume I'm working with propositions as types.

[2] The ever-present caveat in constructive mathematics: for good/strong notions of finite.

[3] The injection version, not the (constructively valid) surjective one. I prove this in Agda here. NB by injective I mean $\Pi x. \Pi y. f(x)=f(y) \rightarrow x=y$, not split/mono, not even split/mono up to extensionality.

Answer 1

$\newcommand{Pot}{\mathsf{Pot}} \newcommand{Act}{\mathsf{Act}} \newcommand{Id}{\mathsf{Id}} \newcommand{refl}{\mathsf{refl}}$

I'm happy to defer to someone more knowledgeable on the topic. However, I've done some preliminary fooling around based on Streicher's Investigations Into Intensional Type Theory, and it seems like the answer to your question 'a' is, "function spaces can get quite large."

Streicher works with realizability, but I think you can also build something similar with a setoid-like construction within an existing type theory, which might be a little more comprehensible to someone practiced with working in (something like) MLTT. That's what I toyed around with, anyhow.

The key idea is that you form a sort of 'modified setoid' model of type theory, where these are given by:

• A type $\Pot$ of "potential' values
• If you want, add an equivalence 'relation' on $\Pot$, and have it interact appropriately with the below, so that you're building an intensional model in an 'extensional' setting. I'm not sure this really matters because we're trying to end up with something intensional anyway, but Streicher was working in a set theory which would be extensional.
• A 'predicate' $\Act(p)$ where $p \in \Pot$, specifying which "potential" values are "actual" values
• Some criterion forcing $\Pot$ to be large; in my toying around I required there to be an injective map $ℕ \hookrightarrow \Pot$. I think you could also require every type to contain many strictly potential values (i.e. not actual), which might help with certain arguments.

The point of all this is that the rules of type theory apply mostly to behavior on actual values, and the (strictly) potential values give ways of refuting various sorts of extensionality. For some examples:

• The empty type $⊥$ can be modeled as $\Pot := ℕ$ with an always false $\Act$
• The singleton type $⊤$ can be modeled as $\Pot := ℕ$ with $\Act$ holding just for $0$
• $ℕ$ can be modeled as $\Pot := ℕ$ and $\Act$ always true
• $A → B$ (and $Π$ similarly) is modeled with ...
  • $\Pot_{A → B} := \Pot_A → \Pot_B$
  • $\Act_{A → B}(f) := ∀x. \Act(x) → \Act(f(x))$
  • $ι_{A → B}(n) := λx. ι_B(n)$
• $\Id_A(x,y)$ can be modeled with ...
  • $\Pot := Σ_{n:ℕ} I(n)$ where $I(n) := (n = 0 → x = y)$
  • $\Act(n, p) := n = 0$

Terms always denote actual values, so for instance function extensionality can fail in the following way:

• Consider the following two functions $⊤ → ⊤$:
  • $f(n) = n$
  • $g(n) = \begin{cases}0 & n = 0 \\ n+1 & \text{otherwise} \end{cases}$
• Both are actual because they map $0$ to $0$
• There is an actual value of type $\mathsf{pw} : Π_{x:⊤}\Id_⊤(f(x), g(x))$:
  • $\mathsf{pw}(0) := (0, \mathsf{const}(\refl))$
  • $\mathsf{pw}(n+1) := (n+1, \mathsf{snz})$ (where $\mathsf{snz}$ is a proof that $n+1 = 0 → T$)
• An actual value of $\Id_{⊤→⊤}(f,g)$ must be $(0, e)$ where $e : f = g$ in our base type theory. But $f$ and $g$ are not even extensionally equal there, because they disagree on 'potential' values.

So for your $\mathsf{big}$ we need to find an actual value to model it. I don't think there's anything too tricky about the universe here, so let's just consider something like $\mathsf{big}_{ℕ,⊤,⊤}$: $\newcommand{b}{\mathsf{b}} \newcommand{ib}{\mathsf{ib}}$

• define $\b : ℕ → ⊤ → ⊤$ via $\b(n, u) = \begin{cases}0 & u = 0 \\ n & \text{otherwise}\end{cases}$
• $b$ is actual because the unit value $0$ is always mapped to $0$
• define $\ib : Π_{m,n:ℕ} \b(m) = \b(n) → m = n$ by reasoning as follows ...
  • for $\ib(m,n,0,e)$, we know $b(m) = b(n)$ from $e$, which implies $e' : m = n$ by applying both sides to any nonzero value, so we can yield $(0,\mathsf{const}(e'))$; this is the only actual case, and our result is actual
  • $\ib(m,n,n+1,e) := (n+1, \mathsf{snz})$, but we are in a strictly potential case

I believe a similar argument also gives an injection $ℕ \hookrightarrow (⊥ → ⊤)$. So, these are like worst case scenarios as far as 'size' goes. $ℕ$ is embedding into function types between 'trivial' types.

However, unless I'm just missing how, I don't think this is enough to give $\mathsf{big}_{ℕ,A,B}$ for all $A$ and inhabited $B$. But, I also don't think it's too hard to fix up. The problem is thus:

• When we try to implement $\mathsf{big}$, we will by hypothesis have an actual value of $B$ from inhabitedness
• But, to produce an actual injective $ℕ → A → B$, we need to recognize some potential values of $A$ so that we can embed the $ℕ$ in those positions (otherwise we have no choice but to return our only actual value of $B$). For $⊤$ we did this by looking at whether the unit value was $0$ or not (and for $⊥$ there are no actual values)
• But, for the definition of $A → B$ above, actual values are undecidable in general

So, I think what is necessary is not just an injection $ℕ \hookrightarrow \Pot$, but also a value $p : \Pot$ that is 1) not actual and 2) decidably apart from the rest of $\Pot$. Then I think it should be possible to embed $ℕ$ in $A → B$ via sticking it in the $p$ position. The types above actually already satisfy this except for ℕ and functions/$Π$, which we can fix by using something like:

• $\Pot_{A → B} = ⊤ + (\Pot_A → \Pot_B)$
• $\Act_{A → B}(ι_0(\mathsf{tt})) = ⊥$
• $\Act_{A → B}(ι_1(f)) = ∀x. \Act_A(x) → \Act_B(f(x))$

Although you could also consider adding more extra values. (Note: if your base theory has excluded middle, then the above fixup should be unnecessary, because you already have an oracle for equality and actuality. I think all you need to do is to require that every type has a strictly potential value. Then you can have a model where $Π$ types satisfy $η$ like Peter says, but which the above does not.)

But also, I don't think there's anything particularly special about $ℕ$ for embedding above. We just used $ℕ$ as the carriers for 'small' types and classified most of the values as "potential." We could do the same thing with a 'bigger' base type than $ℕ$.

However, the problem I would foresee with this is that most 'bigger' base types than $ℕ$ are function types, but the 'modified' function types are much bigger (by that measure) than the ones in the base theory. So, if you required every 'modified setoid' to have an injection from $ℕ → 2$ in the base theory, then e.g. both $ℕ$ and $2$ in the derived theory would already have $ℕ → 2$ potential values, so you are then considering something like whether $(ℕ → 2) → (ℕ → 2)$ can embed into $ℕ → 2$. Perhaps if you instead included a new base type $\nabla (2^ℕ)$ represented by something close to the base $ℕ → 2$, you could have a similar result about that, though I don't know exactly how it'd behave.

Finally, if by excluded middle you mean the naive $Π_{A:\mathcal{U}}A + ¬ A$ sort, I think this just gets inherited. Here's how it works out for the above definition of functions with extra elements

• $A + B$ can just be represented by the sum of the representations, with actuality inherited
• for $\mathsf{LEM}_A$ we need an actual value of $A + ¬ A$.
  • The potential elements are $\Pot_A + ⊤ + (\Pot_A → ℕ)$ ...
  • But the middle $⊤$ is never actual, and the right values are only actual when every $\Pot_A$ is not actual
• So, use the underlying excluded middle to decide $Σ_{x : \Pot_A} \Act_A(x)$
  • In the left case, you have obtained an actual $\Pot_A$ for the left modified case
  • In the right case, you have a proof that there are no actual $\Pot_A$ values, so every function $\Pot_A → ℕ$ is an actual $A → ⊥$ value

I think this might even work for a more sophisticated excluded middle, because the actual values of a modified proposition would form an underlying proposition. But I haven't worked it out in detail.

Answer 2

Expanding on my comment: The methods from Richard Garner’s 2008 paper On the strength of dependent products in the type theory of Martin-Löf (arXiv:0803.4466) show that your axiom $\newcommand{\big}{\mathrm{big}}\big_C$ is consistent with LEM, for any fixed type $C$, and more generally for any defined type whose definition doesn’t itself involve function types. Garner shows essentially that in any model of type theory (including the syntax itself), you can reinterpret the dependent function types $\Pi$ as any construction $\Pi'$ such that the original $\Pi_{x \colon A} B\newcommand{\of}{\colon}$ is a judgemental retract of $\Pi'_{x \of A} B$, while leaving the rest of the language unchanged.

(The details of the reinterpretation are reasonably routine: the new $\lambda$-abstraction uses the inclusion $\Pi_{x \of A}B \hookrightarrow \Pi'_{x \of A} B$, while the new function-application uses the retraction; $\beta$-reduction then holds thanks to the retract property.)

In particular, taking $\Pi'_{x \of A}B$ to be $(\Pi_{x \of A} B) \times (1 + C)$, your axiom $\big_C$ will hold under the resulting interpretation. (It’s clear that we have $\Pi_{A,B:U}\ B \to C \hookrightarrow (A \to' B)$; it’s not too hard then to check that this is logically equivalent to $\Pi'_{A,B:U}\ B \to' C \hookrightarrow' (A \to' B)$, where $(-)'$ means reinterpreting all the $\Pi$-types involved in each definition.)

Finally, the validity of LEM is unchanged; this is fairly direct to check. Generally, for any propositions-as-types statement not involving equality of functions, its reinterpretation will be logically equivalent to its original interpretation.

So starting either from the syntax of some consistent type theory including LEM and the core rules for $\Pi$, $\times$, and $+$, or more generally from any model of such a theory, and taking any type $C$ in that model, we can run Garner’s reinterpretation to show that $\big_C$ is consistent with whatever parts of that type theory are preserved by the reinterpretation — which will include at least all parts not involving function types, plus all PAT-statements not involving function equality, and so including at least LEM.

One elephant in the room here is the $\eta$-rule for functions, that $(\lambda x. f x) = f$, either judgementally or at least propositionally. The $\eta$-rule (even propositional) typically gets broken by this reinterpretation. PER-style models as described in Dan Doel’s answer are more likely to retain the $\eta$-rule in some form.