Return to 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$?

[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.

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.

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 type. If we assume LEM, can we take $C$ to be $\mathbb{N}$ or failing that at least $\mathbf{n+2}$ for some $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.

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$?

[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.

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 type. If we assume LEM, can we take $C$ to be $\mathbb{N}$ or failing that at least $\mathbf{n+2}$ for some $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.

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 type. If we assume LEM, can we take $C$ to be $\mathbb{N}$ or failing that at least $\mathbf{n+2}$ for some $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.