Injective types in univalent mathematics

TL;DR

This paper explores injective and algebraically injective types within univalent mathematics, establishing their characterizations and relationships to universe structures, with results depending on the presence or absence of propositional resizing axioms.

Contribution

It provides a comprehensive analysis of injective types in univalent foundations, linking them to propositional truncation, universe retracts, and partial-map classifiers, with new characterizations under different axiomatic assumptions.

Findings

Injectivity equals propositional truncation of algebraic injectivity under resizing.

Algebraically injective types are retracts of exponential powers of universes.

Results extend to algebraically injective sets and higher types, with universe embedding properties.

Abstract

We investigate the injective types and the algebraically injective types in univalent mathematics, both in the absence and in the presence of propositional resizing. Injectivity is defined by the surjectivity of the restriction map along any embedding, and algebraic injectivity is defined by a given section of the restriction map along any embedding. Under propositional resizing axioms, the main results are easy to state: (1) Injectivity is equivalent to the propositional truncation of algebraic injectivity. (2) The algebraically injective types are precisely the retracts of exponential powers of universes. (2a) The algebraically injective sets are precisely the retracts of powersets. (2b) The algebraically injective $(n+1)$-types are precisely the retracts of exponential powers of universes of $n$-types. (3) The algebraically injective types are also precisely the retracts of algebras of the partial-map classifier. From (2) it follows that any universe is embedded as a retract of any larger universe. In the absence of propositional resizing, we have similar results which have subtler statements that need to keep track of universe levels rather explicitly, and are applied to get the results that require resizing.

Equations

$${\color[rgb]{0,0,0.4}\Pi(X,Y:\mathcal{U})\,\Pi(j:X\hookrightarrow Y)\,\Pi(f:X\to D)\,\exists(g:Y\to D)\,g\mathrel{\circ}j=f,}$$

$${\color[rgb]{0,0,0.4}\Pi(X,Y:\mathcal{U})\,\Pi(j:X\hookrightarrow Y)\,\Pi(f:X\to D)\,\Sigma(f\mid j:Y\to D),f\mid j\mathrel{\circ}j=f,}$$

$$\Pi (X:\mathcal{U})\Sigma$$

$$\displaystyle\mathrel{\phantom{\times}}\text{{\color[rgb]{0,0,0.4}$\mathinner{{}\color[rgb]{0,0,0.4}\left\llbracket\normalcolor\,{\color[rgb]{0,0,0.4}X}\,\color[rgb]{0,0,0.4}\right\rrbracket}$} is a proposition}\times(X\to\mathinner{{}\color[rgb]{0,0,0.4}\left\llbracket\normalcolor\,{\color[rgb]{0,0,0.4}X}\,\color[rgb]{0,0,0.4}\right\rrbracket})$$

$$\displaystyle\times\mathinner{{}\color[rgb]{0,0.3,0.9}\left(\normalcolor\,\Pi(P:\mathcal{V}),\text{{\color[rgb]{0,0,0.4}$P$} is a proposition}\to(X\to P)\to\mathinner{{}\color[rgb]{0,0,0.4}\left\llbracket\normalcolor\,{\color[rgb]{0,0,0.4}X}\,\color[rgb]{0,0,0.4}\right\rrbracket}\to P\,\color[rgb]{0,0.3,0.9}\right)}.$$

$${\color[rgb]{0,0,0.4}\bar{f}\mid x\mid=fx}$$

$${\color[rgb]{0,0,0.4}\text{{\color[rgb]{0,0,0.4}$X$} is a singleton}\overset{\text{def}}{=}\Sigma(c:X),\Pi(x:X),x=c.}$$

$${\color[rgb]{0,0,0.4}\text{{\color[rgb]{0,0,0.4}$X$} is a proposition}\overset{\text{def}}{=}\Pi(x,y:X),x=y.}$$

$${\color[rgb]{0,0,0.4}(\exists(x:X),A\,x)\overset{\text{def}}{=}\mathinner{{}\color[rgb]{0,0,0.4}\left\llbracket\normalcolor\,{\color[rgb]{0,0,0.4}\Sigma(x:X),A\,x}\,\color[rgb]{0,0,0.4}\right\rrbracket}.}$$

$${\color[rgb]{0,0,0.4}(\exists!(x:X),A\,x)\overset{\text{def}}{=}\text{the type {\color[rgb]{0,0,0.4}$\Sigma(x:X),A\,x$} is a singleton}.}$$

$${\color[rgb]{0,0,0.4}f^{-1}(y)\overset{\text{def}}{=}\Sigma(x:X),fx=y.}$$

$${\color[rgb]{0,0,0.4}\Pi(X:\mathcal{U})\,\Pi(Y:\mathcal{V})\,\Pi(j:X\hookrightarrow Y)\,\Pi(f:X\to D),\,\exists(g:Y\to D),g\mathrel{\circ}j\sim f,}$$

$${\color[rgb]{0,0,0.4}\Pi(X:\mathcal{U})\,\Pi(Y:\mathcal{V})\,\Pi(j:X\hookrightarrow Y)\,\Pi(f:X\to D),\,\Sigma(f\mid j:Y\to D),f\mid j\mathrel{\circ}j\sim f.}$$

$$(f\text{scaleobj}0.7\downarrow j)y$$

$$(f\text{scaleobj}0.7\uparrow j)y$$

$${\color[rgb]{0,0,0.4}(f\scaleobj{0.7}{\,\downarrow\,}j\mathrel{\circ}j)\,x\simeq fx\simeq(f\scaleobj{0.7}{\,\uparrow\,}j\mathrel{\circ}j)\,x,}$$

$${\color[rgb]{0,0,0.4}f[p]\overset{\text{def}}{=}\operatorname{transport}fp}$$

$${\color[rgb]{0,0,0.4}f[\operatorname{refl}_{x}]=\operatorname{id}_{f\,x},\qquad\qquad f[p\operatorname{\bullet}q]=f[q]\mathrel{\circ}f[p].}$$

$${\color[rgb]{0,0,0.4}f\mathrel{\,\,\preceq\,\,}f^{\prime}\overset{\text{def}}{=}\Pi(x:X),f\,x\to f^{\prime}x,}$$

$${\color[rgb]{0,0,0.4}\tau_{y}\mathrel{\circ}f[p]=f^{\prime}[p]\mathrel{\circ}\tau_{x}.}$$

$${\color[rgb]{0,0,0.4}\begin{array}[]{lll}s\,f&\overset{\text{def}}{=}&f\scaleobj{0.7}{\,\downarrow\,}j,\\ r\,g&\overset{\text{def}}{=}&g\mathrel{\circ}j.\end{array}}$$

$${\color[rgb]{0,0,0.4}\kappa\,g\,y\,((x,p),C)\overset{\text{def}}{=}\operatorname{transport}\,g\,p\,C}$$

$${\color[rgb]{0,0,0.4}M\overset{\text{def}}{=}\Sigma(g:Y\to\mathcal{U})\,\Pi(y:Y),\text{the map {\color[rgb]{0,0,0.4}$\kappa\,g\,y:s(r\,g)\,y\to g\,y$} is an equivalence.}}$$

$${\color[rgb]{0,0,0.4}\operatorname{pr}_{1}:M\to(Y\to\mathcal{U})}$$

$${\color[rgb]{0,0,0.4}\begin{array}[]{lll}\phi\,f&\overset{\text{def}}{=}&(sf,\varepsilon\,f),\\ \gamma\,(g,e)&\overset{\text{def}}{=}&r\,g,\end{array}}$$

$${\color[rgb]{0,0,0.4}\begin{array}[]{lll}A&\overset{\text{def}}{=}&\Sigma(t:j^{-1}(y)),\Sigma(w:j^{-1}(j(\operatorname{pr}_{1}t))),f(\operatorname{pr}_{1}w)\\ B&\overset{\text{def}}{=}&\Sigma(w:j^{-1}(y)),f(\operatorname{pr}_{1}w).\end{array}}$$

$${\color[rgb]{0,0,0.4}\delta\,((x,p),C)\overset{\text{def}}{=}((x,p),(x,\operatorname{refl}_{j\,x}),C).}$$

$${\color[rgb]{0,0,0.4}\begin{array}[]{lll}s\,f&\overset{\text{def}}{=}&f\scaleobj{0.7}{\,\uparrow\,}j,\\ r\,g&\overset{\text{def}}{=}&g\mathrel{\circ}j.\end{array}}$$

$${\color[rgb]{0,0,0.4}\kappa\,g\,y\,C(x,p)\overset{\text{def}}{=}\operatorname{transport}\,g\,p^{-1}\,C}$$

$${\color[rgb]{0,0,0.4}M\overset{\text{def}}{=}\Sigma(g:Y\to\mathcal{U})\,\Pi(y:Y),\text{the map {\color[rgb]{0,0,0.4}$\kappa\,g\,y:g\,y\to s(r\,g)\,y$} is an equivalence.}}$$

$${\color[rgb]{0,0,0.4}\begin{array}[]{lll}\phi\,f&\overset{\text{def}}{=}&(sf,\varepsilon\,f),\\ \gamma\,(g,e)&\overset{\text{def}}{=}&r\,g,\end{array}}$$

$${\color[rgb]{0,0,0.4}\begin{array}[]{lll}A&\overset{\text{def}}{=}&\Pi(w:j^{-1}(y)),f(\operatorname{pr}_{1}w),\\ B&\overset{\text{def}}{=}&\Pi(t:j^{-1}(y)),\Pi(w:j^{-1}(j(\operatorname{pr}_{1}t))),f(\operatorname{pr}_{1}w).\end{array}}$$

Full text

Keywords. Injective type, flabby type, Kan extension, partial-map classifier, univalent mathematics, univalence axiom.

MSC 2010. 03B15, 03B35, 03G30, 18A40, 18C15.

1 Introduction

We investigate the injective types and the algebraically injective types in univalent mathematics, both in the absence and in the presence of propositional resizing axioms. These notions of injectivity are about the extension problem {diagram} The injectivity of a type $D:\mathcal{U}$ is defined by the surjectivity of the restriction map $(-)\mathrel{\circ}j$ along any embedding $j$:

[TABLE]

so that we get an unspecified extension $g$ of $f$ along $j$. The algebraic injectivity of $D$ is defined by a given section $(-)\mid j$ of the restriction map $(-)\mathrel{\circ}j$, following Bourke’s terminology [2]. By $\Sigma{-}\Pi$-distributivity, this amounts to

[TABLE]

so that we get a designated extension $f\mid j$ of $f$ along $j$. Formally, in this definition, $f\mid j$ can be regarded as a variable, but we instead think of the symbol “$\mid$” as a binary operator.

For the sake of generality, we work without assuming or rejecting the principle of excluded middle, and hence without assuming the axiom of choice either. Moreover, we show that the principle of excluded middle holds if and only if all pointed types are algebraically injective, and, assuming resizing, if and only if all inhabited types are injective, so that there is nothing interesting to say about (algebraic) injectivity in its presence. That pointness and inhabitedness are needed is seen by considering the embedding $\mathbb{0}\hookrightarrow\mathbb{1}$.

Under propositional resizing principles [15] (Definitions 25 and 52 below), the main results are easy to state:

Injectivity is equivalent to the propositional truncation of algebraic injectivity.

(This can be seen as a form of choice that just holds, as it moves a propositional truncation inside a $\Pi$-type to outside the $\Pi$-type, and may be related to [9].) 2. 2.

The algebraically injective types are precisely the retracts of exponential powers of universes. Here by an exponential power of a type $B$ we mean a type of the form $A\to B$, also written $B^{A}$.

In particular,

1. (a)

The algebraically injective sets are precisely the retracts of powersets. 2. (b)

The algebraically injective $(n+1)$-types are precisely retracts of exponential powers of the universes of $n$-types.

Another consequence is that any universe is embedded as a retract of any larger universe. 3. 3.

The algebraically injective types are also precisely the underlying objects of the algebras of the partial-map classifier.

In the absence of propositional resizing, we have similar results that have subtler statements that need to keep track of universe levels rather explicitly. Most constructions developed in this paper are in the absence of propositional resizing. We apply them, with the aid of a notion of algebraic flabbiness, which is related to the partial-map classifier, to derive the results that rely on resizing mentioned above.

Acknowledgements.

Mike Shulman has acted as a sounding board over the years, with many helpful remarks, including in particular the suggestion of the terminology algebraic injectivity from [2] for the notion we consider here.

2 Underlying formal system

Our handling of universes has a model in $\infty$-toposes following Shulman [14]. It differs from that of the HoTT book [15], and Coq [4], in that we don’t assume cumulativity, and it agrees with that of Agda [3].

2.1 Our univalent type theory

Our underlying formal system can be considered to be a subsystem of that used in UniMath [16].

We work within an intensional Martin-Löf type theory with types $\mathbb{0}$ (empty type), $\mathbb{1}$ (one-element type with $\operatorname{\star}:\mathbb{1}$), $\mathbb{N}$ (natural numbers), and type formers $+$ (binary sum), $\Pi$ (product), $\Sigma$ (sum) and $\operatorname{Id}$ (identity type), and a hierarchy of type universes ranged over by $\mathcal{U},\mathcal{V},\mathcal{W},\mathcal{T}$, closed under them in a suitable sense discussed below.

We take these as required closure properties of our formal system, rather than as an inductive definition. 2. 2.

We assume a universe $\mathcal{U}_{0}$, and for each universe $\mathcal{U}$ we assume a successor universe $\mathcal{U}^{+}$ with $\mathcal{U}:\mathcal{U}^{+}$, and for any two universes $\mathcal{U},\mathcal{V}$ a least upper bound $\mathcal{U}\sqcup\mathcal{V}$. We stipulate that we have $\mathcal{U}_{0}\sqcup\mathcal{U}=\mathcal{U}$ and $\mathcal{U}\sqcup\mathcal{U}^{+}=\mathcal{U}^{+}$ definitionally, and that the operation $(-)\sqcup(-)$ is definitionally idempotent, commutative, and associative, and that the successor operation $(-)^{+}$ distributes over $(-)\sqcup(-)$ definitionally. 3. 3.

We don’t assume that the universes are cumulative on the nose, in the sense that from $X:\mathcal{U}$ we would be able to deduce that $X:\mathcal{U}\sqcup\mathcal{V}$ for any $\mathcal{V}$, but we also don’t assume that they are not. However, from the assumptions formulated below, it follows that for any two universes $\mathcal{U},\mathcal{V}$ there is a map $\operatorname{lift}_{\mathcal{U},\mathcal{V}}:\mathcal{U}\to\mathcal{U}\sqcup\mathcal{V}$, for instance $X\mapsto X+\mathbb{0}_{\mathcal{V}}$, which is an embedding with $\operatorname{lift}X\simeq X$ if univalence holds (we cannot write the identity type $\operatorname{lift}X=X$, as the left- and right-hand sides live in the different types $\mathcal{U}$ and $\mathcal{U}\sqcup\mathcal{V}$, which are not (definitionally) the same in general). 4. 4.

We stipulate that we have copies $\mathbb{0}_{\mathcal{U}}$ and $\mathbb{1}_{\mathcal{V}}$ of the empty and singleton types in each universe $\mathcal{U}$ (with the subscripts often elided). 5. 5.

We stipulate that if $X:\mathcal{U}$ and $Y:\mathcal{V}$, then $X+Y:\mathcal{U}\sqcup\mathcal{V}$. 6. 6.

We stipulate that if $X:\mathcal{U}$ and $A:X\to\mathcal{V}$ then $\Pi_{X}A:\mathcal{U}\sqcup\mathcal{V}$. We abbreviate this product type as $\Pi A$ when $X$ can be inferred from $A$, and sometimes we write it verbosely as $\Pi(x:X),A\,x$.

In particular, for types $X:\mathcal{U}$ and $Y:\mathcal{V}$, we have the function type $X\to Y:\mathcal{U}\sqcup\mathcal{V}$. 7. 7.

The same type stipulations as for $\Pi$, and the same grammatical conventions apply to the sum type former $\Sigma$.

In particular, for types $X:\mathcal{U}$ and $Y:\mathcal{V}$, we have the cartesian product $X\times Y:\mathcal{U}\sqcup\mathcal{V}$. 8. 8.

We assume the $\eta$ rules for $\Pi$ and $\Sigma$, namely that $f=\lambda x,f\,x$ holds definitionally for any $f$ in a $\Pi$-type and that $z=(\operatorname{pr}_{1}z,\operatorname{pr}_{2}z)$ holds definitionally for any $z$ in a $\Sigma$ type, where $\operatorname{pr}_{1}$ and $\operatorname{pr}_{2}$ are the projections. 9. 9.

For a type $X$ and points $x,y:X$, the identity type $\operatorname{Id}_{X}x\,y$ is abbreviated as $\operatorname{Id}x\,y$ and often written $x=_{X}y$ or simply $x=y$.

The elements of the identity type $x=y$ are called identifications or paths from $x$ to $y$. 10. 10.

When making definitions, definitional equality is written “$\overset{\text{def}}{=}$”. When it is invoked, it is written e.g. “$x=y$ definitionally”. This is consistent with the fact that any definitional equality $x=y$ gives rise to an element of the identity type $x=y$ and should therefore be unambiguous. 11. 11.

When we say that something is the case by construction, this means we are expanding definitional equalities. 12. 12.

We tacitly assume univalence [15], which gives function extensionality (pointwise equal functions are equal) and propositional extensionality (logically equivalent subsingletons are equal). 13. 13.

We work with the existence of propositional, or subsingleton, truncations as an assumption, also tacit. The HoTT book [15], instead, defines type formation rules for propositional truncation as a syntactical construct of the formal system. Here we take propositional truncation as an axiom for any pair of universes $\mathcal{U},\mathcal{V}$:

[TABLE]

We write $\mid x\mid$ for the insertion of $x:X$ into the type \mathinner{{}\color[rgb]{0,0,0.4}\left\llbracket\normalcolor\,{\color[rgb]{0,0,0.4}X}\,\color[rgb]{0,0,0.4}\right\rrbracket} by the assumed function X\to\mathinner{{}\color[rgb]{0,0,0.4}\left\llbracket\normalcolor\,{\color[rgb]{0,0,0.4}X}\,\color[rgb]{0,0,0.4}\right\rrbracket}. We also denote by $\bar{f}$ the function \mathinner{{}\color[rgb]{0,0,0.4}\left\llbracket\normalcolor\,{\color[rgb]{0,0,0.4}X}\,\color[rgb]{0,0,0.4}\right\rrbracket}\to P obtained by the given “elimination rule” (X\to P)\to\mathinner{{}\color[rgb]{0,0,0.4}\left\llbracket\normalcolor\,{\color[rgb]{0,0,0.4}X}\,\color[rgb]{0,0,0.4}\right\rrbracket}\to P applied to a function $f:X\to P$. The universe $\mathcal{U}$ is that of types we truncate, and $\mathcal{V}$ is the universe where the propositions we eliminate into live. Because the existence of propositional truncations is an assumption rather than a type formation rule, its so-called “computation” rule

[TABLE]

doesn’t hold definitionally, of course, but is established as a derived identification, by the definition of proposition.

2.2 Terminology and notation

We assume that the readers are already familiar with the notions of univalent mathematics, e.g. from the HoTT book [15]. The purpose of this section is to establish terminology and notation only, particularly regarding our modes of expression that diverge from the HoTT book.

A type $X$ is a singleton, or contractible, if there is a designated $c:X$ with $x=c$ for all $x:X$:

[TABLE] 2. 2.

A proposition, or subsingleton, or truth value, is a type with at most one element, meaning that any two of its elements are identified:

[TABLE] 3. 3.

By an unspecified element of a type $X$ we mean a (specified) element of its propositional truncation \mathinner{{}\color[rgb]{0,0,0.4}\left\llbracket\normalcolor\,{\color[rgb]{0,0,0.4}X}\,\color[rgb]{0,0,0.4}\right\rrbracket}.

We say that a type is inhabited if it has an unspecified element.

If the type $X$ codifies a mathematical statement, we say that $X$ holds in an unspecified way to mean the assertion \mathinner{{}\color[rgb]{0,0,0.4}\left\llbracket\normalcolor\,{\color[rgb]{0,0,0.4}X}\,\color[rgb]{0,0,0.4}\right\rrbracket}. For example, if we say that the type $A$ is a retract of the type $B$ in an unspecified way, what we mean is that \mathinner{{}\color[rgb]{0,0,0.4}\left\llbracket\normalcolor\,{\color[rgb]{0,0,0.4}\text{{\color[rgb]{0,0,0.4}A} is a retract of {\color[rgb]{0,0,0.4}B}}}\,\color[rgb]{0,0,0.4}\right\rrbracket}. 4. 4.

Phrases such as “there exists”, “there is”, “there is some”, “for some” etc. indicate a propositionally truncated $\Sigma$, and symbolically we write

[TABLE]

For emphasis, we may say that there is an unspecified $x:X$ with $A\,x$.

When the meaning of existence is intended to be (untruncated) $\Sigma$, we use phrases such as “there is a designated”, “there is a specified”, “there is a distinguished”, “there is a given”, “there is a chosen”, “for some chosen”, “we can find” etc.

The statement that there is a unique $x:X$ with $A\,x$ amounts to the assertion that the type $\Sigma(x:X),A\,x$ is a singleton:

[TABLE]

That is, there is a unique pair $(x,a)$ with $x:X$ and $a:A\,x$. This doesn’t need to be explicitly propositionally truncated, because singleton types are automatically propositions.

The statement that there is at most one $x:X$ with $A\,x$ amounts to the assertion that the type $\Sigma(x:X),A\,x$ is a subsingleton (so we have at most one pair $(x,a)$ with $x:X$ and $a:A\,x$). 5. 5.

We often express a type of the form $\Sigma(x:X),A\,x$ by phrases such as “the type of $x:X$ with $A\,x$”.

For example, if we define the fiber of a point $y:Y$ under a function $f:X\to Y$ to be the type $f^{-1}(y)$ of points $x:X$ that are mapped by $f$ to a point identified with $y$, it should be clear from the above conventions that we mean

[TABLE]

Also, with the above terminological conventions, saying that the fibers of $f$ are singletons (that is, that $f$ is an equivalence) amounts to the same thing as saying that for every $y:Y$ there is a unique $x:X$ with $f(x)=y$.

Similarly, we say that such an $f$ is an embedding if for every $y:Y$ there is at most one $x:X$ with $f(x)=y$. In passing, we remark that, in general, this is stronger than $f$ being left-cancellable, but coincides with left-cancellability if the type $Y$ is a set (its identity types are all subsingletons). 6. 6.

We sometimes use the mathematically more familiar “maps to” notation $\mapsto$ instead of type-theoretical lambda notation $\lambda$ for defining nameless functions. 7. 7.

Contrarily to an existing convention among some practitioners, we will not reserve the word is for mathematical statements that are subsingleton types. For example, we say that a type is algebraically injective to mean that it comes equipped with suitable data, or that a type $X$ is a retract of a type $Y$ to mean that there are designated functions $s:X\to Y$ and $r:Y\to X$, and a designated pointwise identification $r\mathrel{\circ}s\sim\operatorname{id}$. 8. 8.

Similarly, we don’t reserve the words theorem, lemma, corollary and proof for constructions of elements of subsingleton types, and all our constructions are indicated by the word proof, including the construction of data or structure.

Because proposition is a semantical rather than syntactical notion in univalent mathematics, we often have situations when we know that a type is a proposition only much later in the mathematical development. An example of this is univalence. To know that this is a proposition, we first need to state and prove many lemmas, and even if these lemmas are propositions themselves, we will not know this at the time they are stated and proved. For instance, knowing that the notion of being an equivalence is a proposition requires function extensionality, which follows from univalence. Then this is used to prove that univalence is a proposition.

2.3 Formal development

A computer-aided formal development of the material of this paper has been performed in Agda [3], occasionally preceded by pencil and paper scribbles, but mostly directly in the computer with the aid of Agda’s interactive features. This paper is an unformalization of that development. We emphasize that not only numbered statements in this paper have formal counterparts, but also the comments in passing, and that the formal version has more information than what we choose to report here.

We have two versions. One of them [7] is in blackboard style, with the ideas in the order they have come to our mind over the years, in a fairly disorganized way, and with local assumptions of univalence, function extensionality, propositional extensionality and propositional truncation. The other one [6] is in article style, with univalence and existence of propositional truncations as global assumptions, and functional and propositional extensionality derived from univalence. This second version follows closely this paper (or rather this paper follows closely that version), organized in a way more suitable for dissemination, repeating the blackboard definitions, in a definitionally equal way, and reproducing the proofs and constructions that we consider to be relevant while invoking the blackboard for the routine, unenlightening ones. The blackboard version also has additional information that we have chosen not to include in the article version of the Agda development or this paper.

An advantage of the availability of a formal version is that, whatever steps we have omitted here because we considered them to be obvious or routine, can be found there, in case of doubt.

3 Injectivity with universe levels

As discussed in the introduction, in the absence of propositional resizing we are forced to keep track of universe levels rather explicitly.

1 Definition**.**

We say that a type $D$ in a universe $\mathcal{W}$ is $\mathcal{U},\mathcal{V}$-injective to mean

[TABLE]

and that it is algebraically $\mathcal{U},\mathcal{V}$-injective to mean

[TABLE]

Notice that, because we have function extensionality, pointwise equality $\sim$ of functions is equivalent to equality, and hence equal to equality by univalence. But it is more convenient for the purposes of this paper to work with pointwise equality in these definitions.

4 The algebraic injectivity of universes

Let $\mathcal{U},\mathcal{V},\mathcal{W}$ be universes, $X:\mathcal{U}$ and $Y:\mathcal{V}$ be types, and $f:X\to\mathcal{W}$ and $j:X\to Y$ be given functions, where $j$ is not necessarily an embedding. We define functions $f\scaleobj{0.7}{\,\downarrow\,}j$ and $f\scaleobj{0.7}{\,\uparrow\,}j$ of type $Y\to\mathcal{U}\sqcup\mathcal{V}\sqcup\mathcal{W}$ by

[TABLE]

2 Lemma**.**

If $j$ is an embedding, then both $f\scaleobj{0.7}{\,\downarrow\,}j$ and $f\scaleobj{0.7}{\,\uparrow\,}j$ are extensions of $f$ along $j$ up to equivalence, in the sense that

[TABLE]

and hence extensions up to equality if $\mathcal{W}$ is taken to be $\mathcal{U}\sqcup\mathcal{V}$, by univalence.

Notice that if $\mathcal{W}$ is kept arbitrary, then univalence cannot be applied because equality is defined only for elements of the same type.

Proof.

Because a sum indexed by a subsingleton is equivalent to any of its summands, and similarly a product indexed by a subsingleton is equivalent to any of its factors, and because a map is an embedding precisely when its fibers are all subsingletons. ∎

We record this corollary:

3 Lemma**.**

The universe $\mathcal{U}\sqcup\mathcal{V}$ is algebraically $\mathcal{U},\mathcal{V}$-injective, in at least two ways.

And in particular, e.g. $\mathcal{U}$ is $\mathcal{U},\mathcal{U}$-injective, but of course $\mathcal{U}$ doesn’t live in $\mathcal{U}$ and doesn’t even have a copy in $\mathcal{U}$. For the following, we say that $y:Y$ is not in the image of $j$ to mean that $j\,x\neq y$ for all $x:X$.

4 Proposition**.**

For $y:Y$ not in the image of $j$, we have $(f\scaleobj{0.7}{\,\downarrow\,}j)\,y\simeq\mathbb{0}$ and $(f\scaleobj{0.7}{\,\uparrow\,}j)\,y\simeq\mathbb{1}$.

With excluded middle, this would give that the two extensions have the same sum and product as the non-extended map, respectively, but excluded middle is not needed, as it is not hard to see:

5 Remark**.**

We have canonical equivalences $\Sigma f\simeq\Sigma(f\scaleobj{0.7}{\,\downarrow\,}j)$ and $\Pi f\simeq\Pi(f\scaleobj{0.7}{\,\uparrow\,}j)$.

Notice that the functions $f$, $f\scaleobj{0.7}{\,\downarrow\,}j$ and $f\scaleobj{0.7}{\,\uparrow\,}j$, being universe valued, are type families, and hence the notations $\Sigma f$, $\Sigma(f\scaleobj{0.7}{\,\downarrow\,}j)$, $\Pi f$ and $\Pi(f\scaleobj{0.7}{\,\uparrow\,}j)$ are just particular cases of the notations for the sum and product of a type family.

The two extensions are left and right Kan extensions in the following sense, without the need to assume that $j$ is an embedding. First, a map $f:X\to\mathcal{U}$, when $X$ is viewed as an $\infty$-groupoid and hence an $\infty$-category, and when $\mathcal{U}$ is viewed as the $\infty$-generalization of the category of sets, can be considered as a sort of $\infty$-presheaf, because its functoriality is automatic: If we define

[TABLE]

of type $f\,x\to f\,y$ for $p:\operatorname{Id}\,x\,y$, then for $q:\operatorname{Id}\,y\,z$ we have

[TABLE]

Then we can consider the type of transformations between such $\infty$-presheaves $f:X\to\mathcal{W}$ and $f^{\prime}:X\to\mathcal{W}^{\prime}$ defined by

[TABLE]

which are automatically natural in the sense that for all $\tau:f\mathrel{\,\,\preceq\,\,}f^{\prime}$ and $p:\operatorname{Id}\,x\,y$,

[TABLE]

It is easy to check that we have the following canonical transformations:

6 Remark**.**

$f\scaleobj{0.7}{\,\downarrow\,}j\mathrel{\,\,\preceq\,\,}f\scaleobj{0.7}{\,\uparrow\,}j$* if $j$ is an embedding.*

It is also easy to see that, without assuming $j$ to be an embedding,

$f\mathrel{\,\,\preceq\,\,}f\scaleobj{0.7}{\,\downarrow\,}j\mathrel{\circ}j$, 2. 2.

$f\scaleobj{0.7}{\,\uparrow\,}j\mathrel{\circ}j\mathrel{\,\,\preceq\,\,}f$.

These are particular cases of the following constructions, which are evident and canonical, even if they may be a bit laborious:

7 Remark**.**

For any $g:Y\to\mathcal{T}$, we have canonical equivalences

$(f\scaleobj{0.7}{\,\downarrow\,}j\mathrel{\,\,\preceq\,\,}g)\simeq(f\mathrel{\,\,\preceq\,\,}g\mathrel{\circ}j),$*  i.e. $f\scaleobj{0.7}{\,\downarrow\,}j$ is a left Kan extension,* 2. 2.

$(g\mathrel{\,\,\preceq\,\,}f\scaleobj{0.7}{\,\uparrow\,}j)\simeq(g\mathrel{\circ}j\mathrel{\,\,\preceq\,\,}f),$*  i.e. $f\scaleobj{0.7}{\,\uparrow\,}j$ is a right Kan extension.*

We also have that the left and right Kan extension operators along an embedding are themselves embeddings, as we now show.

8 Theorem**.**

For any types $X,Y:\mathcal{U}$ and any embedding $j:X\to Y$, left Kan extension along $j$ is an embedding of the function type $X\to\mathcal{U}$ into the function type $Y\to\mathcal{U}$.

Proof.

Define $s:(X\to\mathcal{U})\to(Y\to\mathcal{U})$ and $r:(Y\to\mathcal{U})\to(X\to\mathcal{U})$ by

[TABLE]

By function extensionality, we have that $r(s\,f)=f$, because $s$ is a pointwise-extension operator as $j$ is an embedding, and by construction we have that $s(r\,g)=(g\mathrel{\circ}j)\scaleobj{0.7}{\,\downarrow\,}j$. Now define $\kappa:\Pi(g:Y\to\mathcal{U}),s(r\,g)\mathrel{\,\,\preceq\,\,}g$ by

[TABLE]

for all $g:Y\to\mathcal{U}$, $y:Y$, $x:X$, $p:j\,x=y$ and $C:g(j\,x)$, so that $\operatorname{transport}\,g\,p\,C$ has type $g\,y$, and consider the type

[TABLE]

Because the notion of being an equivalence is a proposition and because products of propositions are propositions, the first projection

[TABLE]

is an embedding. To complete the proof, we show that there is an equivalence $\phi:(X\to\mathcal{U})\to M$ whose composition with this projection is $s$, so that $s$, being the composition of two embeddings, is itself an embedding. We construct $\phi$ and its inverse $\gamma$ by

[TABLE]

where $\varepsilon\,f$ is a proof that the map $\kappa\,(sf)\,y$ is an equivalence for every $y:Y$, to be constructed shortly. Before we know this construction, we can see that $\gamma(\phi\,f)=r(s\,f)=f$ so that $\gamma\mathrel{\circ}\phi\sim\operatorname{id}$, and that $\phi(\gamma(g,e))=(s(rg),\varepsilon(rg))$. To check that the pairs $(s(rg),\varepsilon(rg))$ and $(g,e)$ are equal and hence $\phi\mathrel{\circ}\gamma\sim\operatorname{id}$, it suffices to check the equality of the first components, because the second components live in subsingleton types. But $e\,y$ says that $s(r\,g)\,y\simeq g\,y$ for any $y:Y$, and hence by univalence and function extensionality, $s(r\,g)=g$. Thus the functions $\phi$ and $\gamma$ are mutually inverse. Now, $\operatorname{pr}_{1}\mathrel{\circ}\phi=s$ definitionally using the $\eta$-rule for $\Pi$, so that indeed $s$ is the composition of two embeddings, as we wanted to show.

It remains to show that the map $\kappa\,(sf)\,y:s(f\,y)\to s(r(s\,f))\,y$ is indeed an equivalence. The domain and codomain of this function amount, by construction, to respectively

[TABLE]

We construct an inverse $\delta:B\to A$ by

[TABLE]

It is routine to check that the functions $\kappa\,(sf)\,y$ and $\delta$ are mutually inverse, which concludes the proof. ∎

The proof of the theorem below follows the same pattern as the previous one with some portions “dualized” in some sense, and so we are slightly more economic with its formulation this time.

9 Theorem**.**

For any types $X,Y:\mathcal{U}$ and any embedding $j:X\to Y$, the right Kan extension operation along $j$ is an embedding of the function type $X\to\mathcal{U}$ into the function type $Y\to\mathcal{U}$.

Proof.

Define $s:(X\to\mathcal{U})\to(Y\to\mathcal{U})$ and $r:(Y\to\mathcal{U})\to(X\to\mathcal{U})$ by

[TABLE]

By function extensionality, we have that $r(s\,f)=f$, and, by construction, $s(r\,g)=(g\mathrel{\circ}j)\scaleobj{0.7}{\,\uparrow\,}j$. Now define $\kappa:\Pi(g:Y\to\mathcal{U}),g\mathrel{\,\,\preceq\,\,}s(r\,g)$ by

[TABLE]

for all $g:Y\to\mathcal{U}$, $y:Y$, $C:g\,y$, $x:X$, $p:j\,x=y$, so that $\operatorname{transport}\,g\,p^{-1}\,C$ has type $g(j\,x)$, and consider the type

[TABLE]

Then the first projection $\operatorname{pr}_{1}:M\to(Y\to\mathcal{U})$ is an embedding. To complete the proof, we show that there is an equivalence $\phi:(X\to\mathcal{U})\to M$ whose composition with this projection is $s$, so that it follows that $s$ is an embedding. We construct $\phi$ and its inverse $\gamma$ by

[TABLE]

where $\varepsilon\,f$ is a proof that the map $\kappa\,(sf)\,y$ is an equivalence for every $y:Y$, so that $\phi$ and $\gamma$ are mutually inverse by the argument of the previous proof.

To prove that the map $\kappa\,(sf)\,y:s(r(s\,f))\,y\to s(f\,y)$ is an equivalence, notice that its domain and codomain amount, by construction, to respectively

[TABLE]

We construct an inverse $\delta:B\to A$ by

[TABLE]

It is routine to check that the functions $\kappa\,(sf)\,y$ and $\delta$ are mutually inverse, which concludes the proof. ∎

The left and right Kan extensions trivially satisfy $f\scaleobj{0.7}{\,\downarrow\,}\operatorname{id}\sim f$ and $f\scaleobj{0.7}{\,\uparrow\,}\operatorname{id}\sim f$ because the identity map is an embedding, by the extension property, and so are contravariantly functorial in view of the following.

10 Remark**.**

For types $X:\mathcal{U}$, $Y:\mathcal{V}$ and $Z:\mathcal{W}$, and functions $j:X\to Y$, $k:Y\to Z$ and $f:X\to\mathcal{U}\sqcup\mathcal{V}\sqcup\mathcal{W}$, we have canonical identifications

[TABLE]

Proof.

This is a direct consequence of the canonical equivalences

[TABLE]

for arbitrary universes $\mathcal{U},\mathcal{V},\mathcal{W}$ and $A:\mathcal{U}$, $B:A\to\mathcal{V}$, and $C:\Sigma\,B\to\mathcal{W}$. ∎

The above and the following are applied in work on compact ordinals (reported in our repository [8]).

11 Remark**.**

For types $X:\mathcal{U}$ and $Y:\mathcal{V}$, and functions $j:X\to Y$, $f:X\to\mathcal{W}$ and $f^{\prime}:X\to\mathcal{W}^{\prime}$, if the type $f\,x$ is a retract of $f^{\prime}\,x$ for any $x:X$, then the type $(f\scaleobj{0.7}{\,\uparrow\,}j)\,y$ is a retract of $(f^{\prime}\scaleobj{0.7}{\,\uparrow\,}j)\,y$ for any $y:Y$.

The construction is routine, and presumably can be performed for left Kan extensions too, but we haven’t paused to check this.

5 Constructions with algebraically injective types

Algebraic injectives are closed under retracts:

12 Lemma**.**

If a type $D$ in a universe $\mathcal{W}$ is algebraically $\mathcal{U},\mathcal{V}$-injective, then so is any retract $D^{\prime}:\mathcal{W}^{\prime}$ of $D$ in any universe $\mathcal{W}^{\prime}$.

In particular, any type equivalent to an algebraically injective type is itself algebraically injective, without the need to invoke univalence.

Proof.

[TABLE]

For a given section-retraction pair $(s,r)$, the construction of the extension operator for $D^{\prime}$ from that of $D$ is given by $f\mid j\overset{\text{def}}{=}r\mathrel{\circ}((s\mathrel{\circ}f)\mid j)$. ∎

13 Lemma**.**

The product of any family $D_{a}$ of algebraically $\mathcal{U},\mathcal{V}$-injective types in a universe $\mathcal{W}$, with indices $a$ in a type $A$ of any universe $\mathcal{T}$, is itself algebraically $\mathcal{U},\mathcal{V}$-injective.

In particular, if a type $D$ in a universe $\mathcal{W}$ is algebraically $\mathcal{U},\mathcal{V}$-injective, then so is any exponential power $A\to D:\mathcal{T}\sqcup\mathcal{W}$ for any type $A$ in any universe $\mathcal{T}$.

Proof.

We construct the extension operator $(-)\mid(-)$ of the product $\Pi D:\mathcal{T}\sqcup\mathcal{W}$ in a pointwise fashion from the extension operators $(-)\mid_{a}(-)$ of the algebraically injective types $D_{a}$: For $f:X\to\Pi D$, we let $f\mid j:Y\to\Pi D$ be

[TABLE]

∎

14 Lemma**.**

Every algebraically $\mathcal{U},\mathcal{V}$-injective type $D:\mathcal{W}$ is a retract of any type $Y:\mathcal{V}$ in which it is embedded into.

Proof.

[TABLE]

We just extend the identity function along the embedding to get the desired retraction $r$. ∎

The following is a sort of $\infty$-Yoneda embedding:

15 Lemma**.**

The identity type former $\operatorname{Id}_{X}$ of any type $X:\mathcal{U}$ is an embedding of the type $X$ into the type $X\to\mathcal{U}$.

Proof.

To show that the $\operatorname{Id}$-fiber of a given $A:X\to\mathcal{U}$ is a subsingleton, it suffices to show that if is pointed then it is a singleton. So let $(x,p):\Sigma(x:X),\operatorname{Id}x=A$ be a point of the fiber. Applying $\Sigma$, seen as a map of type $(X\to\mathcal{U})\to\mathcal{U}$, to the identification $p:\operatorname{Id}\,x=A$, we get an identification

[TABLE]

and hence, being equal to the singleton type $\Sigma(\operatorname{Id}x)$, the type $\Sigma A$ is itself a singleton. Hence we have

[TABLE]

So by a second application of univalence we get $A\,x=(\operatorname{Id}\,x=A)$. Hence, applying $\Sigma$ on both sides, we get $\Sigma A=(\Sigma(x:X),\operatorname{Id}\,x=A)$. Therefore, because the type $\Sigma A$ is a singleton, so is the fiber $\Sigma(x:X),\operatorname{Id}\,x=A$ of $A$. ∎

16 Lemma**.**

If a type $D$ in a universe $\mathcal{U}$ is algebraically $\mathcal{U},\mathcal{U}^{+}$-injective, then $D$ is a retract of the exponential power $D\to\mathcal{U}$ of $\mathcal{U}$.

Proof.

[TABLE]

This is obtained by combining the previous two constructions, using the fact that $D\to\mathcal{U}$ lives in the successor universe $\mathcal{U}^{+}$. ∎

6 Algebraic flabbiness and resizing constructions

We now discuss resizing constructions that don’t assume resizing axioms. The above results, when combined together in the obvious way, almost give directly that the algebraically injective types are precisely the retracts of exponential powers of universes, but there is a universe mismatch. Keeping track of the universes to avoid the mismatch, what we get instead is a resizing construction without the need for resizing axioms:

17 Lemma**.**

Algebraically $\mathcal{U},\mathcal{U}^{+}$-injective types $D:\mathcal{U}$ are algebraically $\mathcal{U},\mathcal{U}$-injective too.

Proof.

By the above constructions, we first get that $D$, being algebraically $\mathcal{U},\mathcal{U}^{+}$-injective, is a retract of $D\to\mathcal{U}$. But then $\mathcal{U}$ is algebraically $\mathcal{U},\mathcal{U}$-injective, and, being a power of $\mathcal{U}$, so is $D\to\mathcal{U}$. Finally, being a retract of $D\to\mathcal{U}$, we have that $D$ is algebraically $\mathcal{U},\mathcal{U}$-injective. ∎

This is resizing down and so is not surprising. Of course, such a construction can be performed directly by considering an embedding $\mathcal{U}\to\mathcal{U}^{+}$, but the idea is to generalize it to obtain further resizing-for-free constructions, and, later, resizing-for-a-price constructions. We achieve this by considering a notion of flabbiness as data, rather than as property as in the 1-topos literature (see e.g. Blechschmidt [1]). The notion of flabbiness considered in topos theory is defined with truncated $\Sigma$, that is, the existential quantifier $\exists$ with values in the subobject classifier $\Omega$. We refer to the notion defined with untruncated $\Sigma$ as algebraic flabbiness.

18 Definition**.**

We say that a type $D:\mathcal{W}$ is algebraically $\mathcal{U}$-flabby if

[TABLE]

This terminology is more than a mere analogy with algebraic injectivity: notice that flabbiness and algebraic flabbiness amount to simply injectivity and algebraic injectivity with respect to the class of embeddings $P\to\mathbb{1}$ with $P$ ranging over subsingletons: {diagram} Notice also that an algebraically flabby type $D$ is pointed, by considering the case when $f$ is the unique map $\mathbb{0}\to D$.

19 Lemma**.**

If a type $D$ in the universe $\mathcal{W}$ is algebraically $\mathcal{U},\mathcal{V}$-injective, then it is algebraically $\mathcal{U}$-flabby.

Proof.

Given a subsingleton $P:\mathcal{U}$ and a map $f:P\to D$, we can take its extension $f\mid\operatorname{!}:\mathbb{1}\to D$ along the unique map $!:P\to\mathbb{1}$, because it is an embedding, and then we let $d\overset{\text{def}}{=}(f\mid\operatorname{!})\,\operatorname{\star}$, and the extension property gives $d=f\,p$ for any $p:P$. ∎

The interesting thing about this is that the universe $\mathcal{V}$ is forgotten, and then we can put any other universe below $\mathcal{U}$ back, as follows.

20 Lemma**.**

If a type $D$ in the universe $\mathcal{W}$ is algebraically $\mathcal{U}\sqcup\mathcal{V}$-flabby, then it is also algebraically $\mathcal{U},\mathcal{V}$-injective.

Proof.

Given an embedding $j:X\to Y$ of types $X:\mathcal{U}$ and $\mathcal{V}$, a map $f:X\to D$ and a point $y:Y$, in order to construct $(f\mid j)\,y$ we consider the map $f_{y}:j^{-1}(y)\to D$ defined by $(x,p)\mapsto f\,x$. Because the fiber $j^{-1}(y):\mathcal{U}\sqcup\mathcal{V}$ is a subsingleton as $j$ is an embedding, we can apply algebraic flabbiness to get $d_{y}:D$ with $d_{y}=f_{y}(x,p)$ for all $(x,p):j^{-1}(y)$. By the construction of $f_{y}$ and the definition of fiber, this amounts to saying that for any $x:X$ and $p:j\,x=y$, we have $d_{y}=f\,x$. Therefore we can take

[TABLE]

because we then have

[TABLE]

for any $x:X$, as required. ∎

We then get the following resizing construction by composing the above two conversions between algebraic flabbiness and injectivity:

21 Lemma**.**

If a type $D$ in the universe $\mathcal{W}$ is algebraically $(\mathcal{U}\sqcup\mathcal{T}),\mathcal{V}$-injective, then it is also algebraically $\mathcal{U},\mathcal{T}$-injective.

In particular, algebraic $\mathcal{U},\mathcal{V}$-injectivity gives algebraic $\mathcal{U},\mathcal{U}$- and $\mathcal{U}_{0},\mathcal{U}$-injectivity. So this is no longer necessarily resizing down, by taking $\mathcal{V}$ to be e.g. the first universe $\mathcal{U}_{0}$.

7 Injectivity of subuniverses

We now apply algebraic flabbiness to show that any subuniverse closed under subsingletons and under sums, or alternatively under products, is also algebraically injective.

22 Definition**.**

By a subuniverse of $\mathcal{U}$ we mean a projection $\Sigma\,A\to\mathcal{U}$ with $A:\mathcal{U}\to\mathcal{T}$ subsingleton-valued and the universe $\mathcal{T}$ arbitrary. By a customary abuse of language, we also sometimes refer to the domain of the projection as the subuniverse. Closure under subsingletons means that $A\,P$ holds for any subsingleton $P:\mathcal{U}$. Closure under sums amounts to saying that if $X:\mathcal{U}$ satisfies $A$ and every $Y\,x$ satisfies $A$ for a family $Y:X\to\mathcal{U}$, then so does $\Sigma\,Y$. Closure under products is defined in the same way with $\Pi$ in place of $\Sigma$.

Notice that $A$ being subsingleton-valued is precisely what is needed for the projection to be an embedding, and that all embeddings are of this form up to equivalence (more precisely, every embedding of any two types is the composition of an equivalence into a sum type followed by the first projection).

23 Lemma**.**

Any subuniverse of $\mathcal{U}$ which is closed under subsingletons and sums, or alternatively under subsingletons and products, is algebraically $\mathcal{U}$-flabby and hence algebraically $\mathcal{U},\mathcal{U}$-injective.

Proof.

Let $\Sigma\,A$ be a subuniverse of $\mathcal{U}$, let $P:\mathcal{U}$ be a subsingleton and $f:P\to\Sigma\,A$ be given. Then define

(1) $X\overset{\text{def}}{=}\Sigma(\operatorname{pr}_{1}\mathrel{\circ}f)$   or   (2) $X\overset{\text{def}}{=}\Pi(\operatorname{pr}_{1}\mathrel{\circ}f)$

according to whether we have closure under sums or products. Because $P$, being a subsingleton satisfies $A$ and because the values of the map $\operatorname{pr}_{1}\mathrel{\circ}f:P\to\mathcal{U}$ satisfy $A$ by definition of subuniverse, we have $a:A\,X$ by the sum or product closure property, and $d\overset{\text{def}}{=}(X,a)$ has type $\Sigma\,A$. To conclude the proof, we need to show that $d=f\,p$ for any $p:P$. Because the second component $a$ lives in a subsingleton by definition of subuniverse, it suffices to show that the first components are equal, that is, that $X=\operatorname{pr}_{1}(fp)$. But this follows by univalence, because a sum indexed by a subsingleton is equivalent to any of summands, and a product indexed by a subsingleton is equivalent to any of its factors. ∎

We index $n$-types from $n=-2$ as in the HoTT book, where the $-2$-types are the singletons. We have the following as a corollary.

24 Theorem**.**

The subuniverse of $n$-types in a universe $\mathcal{U}$ is algebraically $\mathcal{U}$-flabby, in at least two ways, and hence algebraically $\mathcal{U},\mathcal{U}$-injective.

Proof.

We have a subuniverse because the notion of being an $n$-type is a proposition. For $n=-2$, the subuniverse of singletons is itself a singleton, and hence trivially injective. For $n>-2$, the $n$-types are known to be closed under subsingletons and both sums and products. ∎

In particular:

The type $\Omega_{\mathcal{U}}$ of subsingletons in a universe $\mathcal{U}$ is algebraically $\mathcal{U},\mathcal{U}$-injective.

(Another way to see that $\Omega_{\mathcal{U}}$ is algebraically injective is that it is a retract of the universe by propositional truncation. The same would be the case for $n$-types if we were assuming $n$-truncations, which we are not.) 2. 2.

Powersets, being exponential powers of $\Omega_{\mathcal{U}}$, are algebraically $\mathcal{U},\mathcal{U}$-injective.

An anonymous referee suggested the following additional examples: (i) The subuniverse of subfinite types, i.e., subtypes of types for which there is an uunspecified equivalence with $\operatorname{Fin}(n)$ for some $n$. This subuniverse is closed under both $\Pi$ and $\Sigma$. (ii) Reflective subuniverses, as they are closed under $\Pi$. (iii) Any universe $\mathcal{U}$ seen as a subuniverse of $\mathcal{U}\sqcup\mathcal{V}$.

8 Algebraic flabbiness with resizing axioms

Returning to size issues, we now apply algebraic flabbiness to show that propositional resizing gives unrestricted algebraic injective resizing.

25 Definition**.**

The propositional resizing principle, from $\mathcal{U}$ to $\mathcal{V}$, that we consider here says that every proposition in the universe $\mathcal{U}$ has an equivalent copy in the universe $\mathcal{V}$. By propositional resizing without qualification, we mean propositional resizing between any of the universes involved in the discussion.

This is consistent because it is implied by excluded middle, but, as far as we are aware, there is no known computational interpretation of this axiom. A model in which excluded middle fails but propositional resizing holds is given by Shulman [12].

We begin with the following construction, which says that algebraic flabbiness is universe independent in the presence of propositional resizing:

26 Lemma**.**

If propositional resizing holds, then the algebraic $\mathcal{V}$-flabbiness of a type in any universe gives its algebraic $\mathcal{U}$-flabbiness.

Proof.

Let $D:\mathcal{W}$ be a type in any universe $\mathcal{W}$, let $P:\mathcal{U}$ be a proposition and $f:P\to D$. By resizing, we have an equivalence $\beta:Q\to P$ for a suitable proposition $Q:\mathcal{V}$. Then the algebraic $\mathcal{V}$-flabbiness of $D$ gives a point $d:D$ with $d=(f\mathrel{\circ}\beta)\,q$ for all $q:Q$, and hence with $d=f\,p$ for all $p:P$, because we have $p=\beta\,q$ for $q=\alpha\,p$ where $\alpha$ is a quasi-inverse of $\beta$, which establishes the algebraic $\mathcal{U}$-flabbiness of $D$. ∎

And from this it follows that algebraic injectivity is also universe independent in the presence of propositional resizing: we convert back-and-forth between algebraic injectivity and algebraic flabbiness.

27 Lemma**.**

If propositional resizing holds, then for any type $D$ in any universe $\mathcal{W}$, the algebraic $\mathcal{U},\mathcal{V}$-injectivity of $D$ gives its algebraic $\mathcal{U}^{\prime},\mathcal{V}^{\prime}$-injectivity.

Proof.

We first get the $\mathcal{U}$-flabbiness of $D$ by 19, and then its $\mathcal{U}^{\prime}\sqcup\mathcal{V}^{\prime}$-flabbiness by 27, and finally its algebraic $\mathcal{U}^{\prime},\mathcal{V}^{\prime}$-injectivity by 20. ∎

As an application of this and of the algebraic injectivity of universes, we get that any universe is a retract of any larger universe. We remark that for types that are not sets, sections are not automatically embeddings [13]. But we can choose the retraction so that the section is an embedding in our situation.

28 Lemma**.**

We have an embedding of any universe $\mathcal{U}$ into any larger universe $\mathcal{U}\sqcup\mathcal{V}$.

Proof.

For example, we have the embedding given by $X\mapsto X+\mathbb{0}_{\mathcal{V}}$. We don’t consider an argument that this is indeed an embedding to be entirely routine without a significant amount of experience in univalent mathematics, even if this may seem obvious. Nevertheless, it is certainly safe to leave it as a challenge to the reader, and a proof can be found in [6] in case of doubt. ∎

29 Theorem**.**

If propositional resizing holds, then any universe $\mathcal{U}$ is a retract of any larger universe $\mathcal{U}\sqcup\mathcal{V}$ with a section that is an embedding.

Proof.

The universe $\mathcal{U}$ is algebraically $\mathcal{U},\mathcal{U}$-injective by 3, and hence it is algebraically $\mathcal{U}^{+},(\mathcal{U}\sqcup\mathcal{V})^{+}$-injective by 27, which has the right universe assignments to apply the construction 16 that gives a retraction from an embedding of an injective type into a larger type, in this case the embedding of the universe $\mathcal{U}$ into the larger universe $\mathcal{U}\sqcup\mathcal{V}$ constructed in 28. ∎

As mentioned above, we almost have that the algebraically injective types are precisely the retracts of exponential powers of universes, up to a universe mismatch. This mismatch is side-stepped by propositional resizing. The following is one of the main results of this paper:

30 Theorem**.**

(First characterization of algebraic injectives.)* If propositional resizing holds, then a type $D$ in a universe $\mathcal{U}$ is algebraically $\mathcal{U},\mathcal{U}$-injective if and only if $D$ is a retract of an exponential power of $\mathcal{U}$ with exponent in $\mathcal{U}$.*

We emphasize that this is a logical equivalence “if and only if” rather than an $\infty$-groupoid equivalence “$\simeq$”. More precisely, the theorem gives two constructions in opposite directions. So this characterizes the types that can be equipped with algebraic-injective structure.

Proof.

$(\Rightarrow)$: Because $D$ is algebraically $\mathcal{U},\mathcal{U}$-injective, it is algebraically $\mathcal{U},\mathcal{U}^{+}$-injective by resizing, and hence it is a retract of $D\to\mathcal{U}$ because it is embedded into it by the identity type former, by taking the extension of the identity function along this embedding.

$(\Leftarrow)$: If $D$ is a retract of $X\to\mathcal{U}$ for some given $X:\mathcal{U}$, then, because $X\to\mathcal{U}$, being an exponential power of the algebraically $\mathcal{U},\mathcal{U}$-injective type $\mathcal{U}$, is algebraically $\mathcal{U},\mathcal{U}$-injective, and hence so is $D$ because it is a retract of this power. ∎

We also have that any algebraically injective $(n+1)$-type is a retract of an exponential power of the universe of $n$-types. We establish something more general first.

31 Lemma**.**

Under propositional resizing, for any subuniverse $\Sigma\,A$ of a universe $\mathcal{U}$ closed under subsingletons, we have that any algebraically $\mathcal{U},\mathcal{U}$-injective type $X:\mathcal{U}$ whose identity types $x=_{X}x^{\prime}$ all satisfy the property $A$ is a retract of the type $X\to\Sigma\,A$.

Proof.

Because the first projection $j:\Sigma\,A\to\mathcal{U}$ is an embedding by the assumption, so is the map $k\overset{\text{def}}{=}j\mathrel{\circ}(-):(X\to\Sigma A)\to(X\to\mathcal{U})$ by a general property of embeddings. Now consider the map $l:X\to(X\to\Sigma\,A)$ defined by $x\mapsto(x^{\prime}\mapsto(x=x^{\prime},p\,x\,x^{\prime}))$, where $p\,x\,x^{\prime}:A(x=x^{\prime})$ is given by the assumption. We have that $k\mathrel{\circ}l=\operatorname{Id}_{X}$ by construction. Hence $l$ is an embedding because $l$ and $\operatorname{Id}_{X}$ are, where we are using the general fact that if $g\mathrel{\circ}f$ and $g$ are embeddings then so is the factor $f$. But $X$, being algebraically $\mathcal{U},\mathcal{U}$-injective by assumption, is algebraically $\mathcal{U},(\mathcal{U}^{+}\sqcup\mathcal{T})$-injective by resizing, and hence so is the exponential power $X\to\Sigma\,A$, and therefore we get the desired retraction by extending its identity map along $l$. ∎

Using this, we get the following as an immediate consequence.

32 Theorem**.**

(Characterization of algebraic injective $(n+1)$-types.)* If propositional resizing holds, then an $(n+1)$-type $D$ in $\mathcal{U}$ is algebraically $\mathcal{U},\mathcal{U}$-injective if and only if $D$ is a retract of an exponential power of the universe of $n$-types in $\mathcal{U}$, with exponent in $\mathcal{U}$.*

33 Corollary**.**

The algebraically injective sets in $\mathcal{U}$ are the retracts of powersets of (arbitrary) types in $\mathcal{U}$, assuming propositional resizing.

Notice that the powerset of any type is a set, because $\Omega_{\mathcal{U}}$ is a set and because sets (and more generally $n$-types) form an exponential ideal.

9 Injectivity in terms of algebraic injectivity in the absence of resizing

We now compare injectivity with algebraic injectivity. The following observation follows from the fact that retractions are surjections:

34 Lemma**.**

If a type $D$ in a universe $\mathcal{W}$ is algebraically $\mathcal{U},\mathcal{V}$-injective, then it is $\mathcal{U},\mathcal{V}$-injective

The following observation follows from the fact that propositions are closed under products.

35 Lemma**.**

Injectivity is a proposition.

But of course algebraic injectivity is not. From this we immediately get the following by the universal property of propositional truncation:

36 Lemma**.**

For any type $D$ in a universe $\mathcal{W}$, the truncation of the algebraic $\mathcal{U},\mathcal{V}$-injectivity of $D$ gives its $\mathcal{U},\mathcal{V}$-injectivity.

In order to relate injectivity to the propositional truncation of algebraic injectivity in the other direction, we first establish some facts about injectivity that we already proved for algebraic injectivity. These facts cannot be obtained by reduction (in particular products of injectives are not necessarily injective, in the absence of choice, but exponential powers are).

37 Lemma**.**

Any $\mathcal{W},\mathcal{V}$-injective type $D$ in a universe $\mathcal{W}$ is a retract of any type in $\mathcal{V}$ it is embedded into, in an unspecified way.

Proof.

Given $Y:\mathcal{V}$ with an embedding $j:D\to Y$, by the $\mathcal{W},\mathcal{V}$-injectivity of $D$ there is an unspecified $r:Y\to D$ with $r\mathrel{\circ}j\sim\operatorname{id}$. Now, if there is a specified $r:Y\to D$ with $r\mathrel{\circ}j\sim\operatorname{id}$ then there is a specified retraction. Therefore, by the functoriality of propositional truncation on objects applied to the previous statement, there is an unspecified retraction. ∎

38 Lemma**.**

If a type $D^{\prime}:\mathcal{U}^{\prime}$ is a retract of a type $D:\mathcal{U}$ then the $\mathcal{W},\mathcal{T}$-injectivity of $D$ implies that of $D^{\prime}$.

Proof.

Let $r:D\to D^{\prime}$ and $s:D^{\prime}\to D$ be the given section retraction pair, and, to show that $D^{\prime}$ is $\mathcal{W},\mathcal{T}$-injective, let an embedding $j:X\to Y$ and a function $f:X\to D^{\prime}$ be given. By the injectivity of $D$, we have some unspecified extension $f^{\prime}:Y\to D$ of $s\mathrel{\circ}f:X\to D$. If such a designated extension is given, then we get the designated extension $r\mathrel{\circ}f^{\prime}$ of $f$. By the functoriality of propositional truncation on objects and the previous two statements, we get the required, unspecified extension. ∎

The universe assignments in the following are probably not very friendly, but we are aiming for maximum generality.

39 Lemma**.**

If a type $D:\mathcal{W}$ is $(\mathcal{U}\sqcup\mathcal{T}),(\mathcal{V}\sqcup\mathcal{T})$-injective, then the exponential power $A\to D$ is $\mathcal{U},\mathcal{V}$-injective for any $A:\mathcal{T}$.

Proof.

For a given embedding $j:X\to Y$ and a given map $f:X\to(A\to D)$, take the exponential transpose $g:X\times A\to D$ of $f$, then extend it along the embedding $j\times\operatorname{id}:X\times A\to Y\times A$ to get $g^{\prime}:Y\times A\to D$ and then back-transpose to get $f^{\prime}:Y\to(A\to D)$, and check that this construction of $f^{\prime}$ does give an extension of $f$ along $j$. For this, we need to know that if $j$ is an embedding then so is $j\times\operatorname{id}$, but this is not hard to check. The result then follows by the functoriality-on-objects of the propositional truncation. ∎

40 Lemma**.**

If a type $D:\mathcal{U}$ is $\mathcal{U},\mathcal{U}^{+}$ injective, then it is a retract of $D\to\mathcal{U}$ in an unspecified way.

Proof.

This is an immediate consequence of 37 and the fact that the identity type former $\operatorname{Id}_{X}:X\to(X\to\mathcal{U})$ is an embedding. ∎

With this we get an almost converse to the fact that truncated algebraic injectivity implies injectivity: the universe levels are different in the converse:

41 Lemma**.**

If a type $D:\mathcal{U}$ is $\mathcal{U},\mathcal{U}^{+}$-injective, then it is algebraically $\mathcal{U},\mathcal{U}^{+}$-injective in an unspecified way.

So, in summary, regarding the relationship between injectivity and truncated algebraic injectivity, so far we know that

if $D$ is algebraically $\mathcal{U},\mathcal{V}$-injective in an unspecified way then it is $\mathcal{U},\mathcal{V}$-injective,

and, not quite conversely,

if $D$ is $\mathcal{U},\mathcal{U}^{+}$-injective then it is algebraically $\mathcal{U},\mathcal{U}$-injective in an unspecified way.

Therefore, using propositional resizing, we get the following characterization of a particular case of injectivity in terms of algebraic injectivity.

42 Proposition**.**

(Injectivity in terms of algebraic injectivity.)* If propositional resizing holds, then a type $D:\mathcal{U}$ is $\mathcal{U},\mathcal{U}^{+}$-injective if and only if it is algebraically $\mathcal{U},\mathcal{U}^{+}$-injective in an unspecified way.*

We would like to do better than this. For that purpose, we consider the partial-map classifier in conjunction with flabbiness and resizing.

10 Algebraic flabbiness via the partial-map classifier

We begin with a generalization [5] of a familiar construction in $1$-topos theory [10].

43 Definition**.**

The lifting $\mathcal{L}_{\mathcal{T}}\,X:\mathcal{T}^{+}\sqcup\mathcal{U}$ of a type $X:\mathcal{U}$ with respect to a universe $\mathcal{T}$ is defined by

[TABLE]

When the universes $\mathcal{T}$ and $\mathcal{U}$ are the same and the last component of the triple is omitted, we have the familiar canonical correspondence

[TABLE]

that maps $A:X\to\mathcal{T}$ to $P\overset{\text{def}}{=}\Sigma\,A$ and the projection $\Sigma\,A\to X$. If the universe $\mathcal{U}$ is not necessarily the same as $\mathcal{T}$, then the equivalence becomes

[TABLE]

This says that although the total space $\Sigma\,A$ doesn’t live in the universe $\mathcal{T}$, it must have a copy in $\mathcal{T}$.

What the third component of the triple does is to restrict the above equivalences to the subtype of those $A$ whose total spaces $\Sigma\,A$ are subsingletons. If we define the type of partial maps by

[TABLE]

where $A\hookrightarrow X$ is the type of embeddings, then for any $X,Y:\mathcal{T}$, we have an equivalence

[TABLE]

so that $\mathcal{L}_{\mathcal{T}}$ is the partial-map classifier for the universe $\mathcal{T}$. When the universe $\mathcal{U}$ is not necessarily the same as $\mathcal{T}$, the lifting classifies partial maps in $\mathcal{U}$ whose embeddings have fibers with copies in $\mathcal{T}$.

This is a sort of an $\infty$-monad “across universes” [8], and modulo providing coherence data, which we haven’t done at the time of writing, but which is not needed for our purposes. We could call this a “wild monad”, but we will refer to it as simply a monad with this warning.

In order to discuss the lifting in more detail, we first characterize its equality types. We denote the projections from $\mathcal{L}_{\mathcal{T}}\,X$ by

[TABLE]

For $l,m:\mathcal{L}_{\mathcal{T}}\,X$, define

[TABLE]

as indicated in the commuting triangle

[TABLE]

44 Lemma**.**

The canonical transformation $(l=m)\to(l\backsimeq m)$ that sends $\operatorname{refl}_{l}$ to the identity equivalence paired with $\operatorname{refl}_{\upsilon\,l}$ is an equivalence.

The unit $\eta:X\to\mathcal{L}_{\mathcal{T}}X$ is given by

[TABLE]

where $i$ is a proof that $\mathbb{1}$ is a proposition.

45 Lemma**.**

The unit $\eta_{X}:X\to\mathcal{L}_{\mathcal{T}}X$ is an embedding.

Proof.

This is easily proved using the above characterization of equality. ∎

46 Lemma**.**

The unit satisfies the unit equations for a monad.

Proof.

Using the above characterization of equality, the left and right unit laws amount to the fact that the type $\mathbb{1}$ is the left and right unit for the operation $(-)\times(-)$ on types. ∎

Next, $\mathcal{L}_{\mathcal{T}}$ is functorial by mapping a function $f:X\to Y$ to the function $\mathcal{L}_{\mathcal{T}}f:\mathcal{L}_{\mathcal{T}}X\to\mathcal{L}_{\mathcal{T}}Y$ defined by

[TABLE]

This commutes with identities and composition definitionally. We define the multiplication $\mu_{X}:\mathcal{L}_{\mathcal{T}}(\mathcal{L}_{\mathcal{T}}\,X)\to\mathcal{L}_{\mathcal{T}}\,X$ by

[TABLE]

47 Lemma**.**

The multiplication satisfies the associativity equation for a monad.

Proof.

Using the above characterization of equality, we see that this amounts to the associativity of $\Sigma$, which says that for $P:\mathcal{T}$, $Q:X\to\mathcal{T}$, $R:\Sigma\,Q\to\mathcal{T}$ we have $(\Sigma(t:\Sigma\,Q),R\,t)\simeq(\Sigma(p:P)\,\Sigma(q:Q\,p),R(p,q))$. ∎

The naturality conditions for the unit and multiplication are even easier to check, and we omit the verification. We now turn to algebras. We omit the direct verification of the following.

48 Lemma**.**

Let $X:\mathcal{U}$ be any type.

A function $\alpha:\mathcal{L}_{\mathcal{T}}X\to X$, that is, a functor algebra, amounts to a family of functions $\bigsqcup_{P}:(P\to X)\to X$ with $P:\mathcal{T}$ ranging over subsingletons.

We will write $\bigsqcup_{P}\phi$ as $\bigsqcup_{p:P}\,\phi\,p$. 2. 2.

The unit law for monad algebras amounts to, for any $x:X$,

[TABLE]

which is equivalent to, for all subsingletons $P$, functions $\phi:P\to X$ and points $p_{0}:P$,

[TABLE]

Therefore a functor algebra satisfying the unit law amounts to the same thing as algebraic flabbiness data. In other words, the algebraically $\mathcal{T}$-flabby types are the algebras of the pointed functor $(\mathcal{L}_{\mathcal{T}},\eta)$. In particular, monad algebras are algebraically flabby. 3. 3.

The associativity law for monad algebras amounts to, for any subsingleton $P:\mathcal{T}$ and family $Q:P\to\mathcal{T}$ of subsingletons, and any $\phi:\Sigma\,Q\to X$,

[TABLE]

So the associativity law for algebras plays no role in flabbiness. But of course we can have algebraic flabbiness data that is associative, such as not only the free algebra $\mathcal{L}_{\mathcal{T}}X$, but also the following two examples that connect to the opening development of this paper on the injectivity of universes, in particular the construction 10:

49 Lemma**.**

The universe $\mathcal{T}$ is a monad algebra of $\mathcal{L}_{\mathcal{T}}$ in at least two ways, with $\bigsqcup=\Sigma$ and $\bigsqcup=\Pi$.

We now apply these ideas to injectivity.

50 Lemma**.**

Any algebraically $\mathcal{T},\mathcal{T}^{+}$-injective type $D:\mathcal{T}$ is a retract of $\mathcal{L}_{\mathcal{T}}D$.

Proof.

Because the unit is an embedding, and so we can extend the identity of $D$ along it. ∎

51 Theorem**.**

(Second characterization of algebraic injectives.)* With propositional resizing, a type $D:\mathcal{T}$ is algebraically $\mathcal{T},\mathcal{T}$-injective if and only if it is a retract of a monad algebra of $\mathcal{L}_{\mathcal{T}}$.*

Proof.

$(\Rightarrow)$: Because $D$ is algebraically $\mathcal{T},\mathcal{T}$-injective, it is algebraically $\mathcal{T},\mathcal{T}^{+}$-injective by resizing, and hence it is a retract of $\mathcal{L}_{\mathcal{T}}D$. $(\Leftarrow)$: Algebraic injectivity is closed under retracts. ∎

52 Definition**.**

Now, instead of propositional resizing, we consider the propositional impredicativity of the universe $\mathcal{U}$, which says that the type $\Omega_{\mathcal{U}}$ of propositions in $\mathcal{U}$, which lives in the next universe $\mathcal{U}^{+}$, has an equivalent copy in $\mathcal{U}$. We refer to this kind of impredicativity as $\Omega$-resizing.

It is not hard to see that propositional resizing implies $\Omega$-resizing for all universes other than the first one [8], and so all the assumption of $\Omega$-resizing does is to account for the first universe too.

53 Lemma**.**

Under $\Omega$-resizing, for any type $X:\mathcal{T}$, the type $\mathcal{L}_{\mathcal{T}}X:\mathcal{T}^{+}$ has an equivalent copy in the universe $\mathcal{T}$.

Proof.

We can take $\Sigma(p:\Omega^{\prime}),\operatorname{pr}_{1}(\rho\,p)\to X$ where $\rho:\Omega^{\prime}\to\Omega_{\mathcal{T}}$ is the given equivalence. ∎

We apply this lifting machinery to get the following, which doesn’t mention lifting in its formulation.

54 Theorem**.**

(Characterization of injectivity in terms of algebraic injectivity.) In the presence of $\Omega$-resizing, the $\mathcal{T},\mathcal{T}$-injectivity of a type $D$ in a universe $\mathcal{T}$ is equivalent to the propositional truncation of its algebraic $\mathcal{T},\mathcal{T}$-injectivity.

Proof.

We already know that the truncation of algebraic injectivity (trivially) gives injectivity. For the other direction, let $L$ be a resized copy of $\mathcal{L}_{\mathcal{T}}D$ in the universe $\mathcal{T}$. Composing the unit with the equivalence given by resizing, we get an embedding $D\to L$, because embeddings are closed under composition and equivalences are embeddings. Hence $D$ is a retract of $L$ in an unspecified way by the injectivity of $D$, by extending its identity. But $L$, being equivalent to a free algebra, is algebraically injective, and hence, being a retract of $L$ in an unspecified way, $D$ is algebraically injective in an unspecified way, because retracts of algebraically injectives are algebraically injective, by the functoriality of truncation on objects. ∎

As an immediate consequence, by reduction to the above results about algebraic injectivity, we have the following corollary.

55 Theorem**.**

Under $\Omega$-resizing and propositional resizing, if a type $D$ in a universe $\mathcal{T}$ is $\mathcal{T},\mathcal{T}$-injective , then it is also $\mathcal{U},\mathcal{V}$-injective for any universes $\mathcal{U}$ and $\mathcal{V}$.

Proof.

The type $D$ is algebraically $\mathcal{T},\mathcal{T}$-injective in an unspecified way, and so by functoriality of truncation on objects and algebraic injective resizing, it is algebraically $\mathcal{U},\mathcal{V}$-injective in an unspecified way, and hence it is $\mathcal{U},\mathcal{V}$-injective. ∎

At the time of writing, we are not able to establish the converse. In particular, we don’t have the analogue of 27.

11 The equivalence of excluded middle with the (algebraic) injectivity of all pointed types

Algebraic flabbiness can also be applied to show that all pointed types are (algebraically) injective if and only if excluded middle holds, where for injectivity resizing is needed as an assumption, but for algebraic injectivity it is not.

The decidability of a type $X$ is defined to be the assertion $X+(X\to\mathbb{0})$, which says that we can exhibit a point of $X$ or else tell that $X$ is empty. The principle of excluded middle in univalent mathematics, for the universe $\mathcal{U}$, is taken to mean that all subsingleton types in $\mathcal{U}$ are decidable:

[TABLE]

As discussed in the introduction, we are not assuming or rejecting this principle, which is independent of the other axioms. Notice that, in the presence of function extensionality, this principle is a subsingleton, because products of subsingletons are subsingletons and because $P+(P\to\mathbb{0})$ is a subsingleton for any subsingleton $P$. So in the following we get data out of a proposition.

56 Lemma**.**

If excluded middle holds in the universe $\mathcal{U}$, then every pointed type $D$ in any universe $\mathcal{W}$ is algebraically $\mathcal{U}$-flabby.

Proof.

Let $d$ be the given point of $D$ and $f:P\to D$ be a function with subsingleton domain. If we have a point $p:P$, then we can take $f\,p$ as the flabbiness witness. Otherwise, if $P\to\mathbb{0}$, we can take $d$ as the flabbiness witness. ∎

For the converse, we use the following.

57 Lemma**.**

If the type $P+(P\to\mathbb{0})+\mathbb{1}$ is algebraically $\mathcal{W}$-flabby for a given subsingleton $P$ in a universe $\mathcal{W}$, then $P$ is decidable.

Proof.

Denote by $D$ the type $P+(P\to\mathbb{0})+\mathbb{1}$ and let $f:P+(P\to\mathbb{0})\to D$ be the inclusion. Because $P+(P\to\mathbb{0})$ is a subsingleton, the algebraic flabbiness of $D$ gives $d:D$ with $d=f\,z$ for all $z:P+(P\to\mathbb{0})$. Now, by definition of binary sum, $d$ must be in one of the three components of the sum that defines $D$. If it were in the third component, namely $\mathbb{1}$, then $P$ couldn’t hold, because if it did we would have $p:P$ and hence, omitting the inclusions into sums, and considering $z=p$, we would have, $d=fp=p$, because $f$ is the inclusion, which is not in the $\mathbb{1}$ component. But also $P\to\mathbb{0}$ couldn’t hold, because if it did we would have $\phi:P\to\mathbb{0}$ and hence, again omitting the inclusion, and considering $z=\phi$, we would have $d=f\,\phi=\phi$, which again is not in the $\mathbb{1}$ component. But it is impossible for both $P$ and $P\to\mathbb{0}$ to fail, because this would mean that we would have functions $P\to\mathbb{0}$ (the failure of $P$) and $(P\to\mathbb{0})\to\mathbb{0}$ (the failure of $P\to\mathbb{0}$), and so we could apply the second function to the first to get a point of the empty type, which is not available. Therefore $d$ can’t be in the third component, and so it must be in the first or the second, which means that $P$ is decidable. ∎

From this we immediately conclude the following:

58 Lemma**.**

If all pointed types in a universe $\mathcal{W}$ are algebraically $\mathcal{W}$-flabby, then excluded middle holds in $\mathcal{W}$.

And then we have the same situation for algebraically injective types, by reduction to algebraic flabbiness:

59 Lemma**.**

If excluded middle holds in the universe $\mathcal{U}\sqcup\mathcal{V}$, then any pointed type $D$ in any universe $\mathcal{W}$ is algebraically $\mathcal{U},\mathcal{V}$-injective.

Putting this together with some universe specializations, we have the following construction.

60 Theorem**.**

All pointed types in a universe $\mathcal{U}$ are algebraically $\mathcal{U},\mathcal{U}$-injective if and only if excluded middle holds in $\mathcal{U}$.

And we have a similar situation with injective types.

61 Lemma**.**

If excluded middle holds, then every inhabited type of any universe is injective with respect to any two universes.

Proof.

Because excluded middle gives algebraic injectivity, which in turn gives injectivity. ∎

Without resizing, we have the following.

62 Lemma**.**

If every inhabited type $D:\mathcal{W}$ is $\mathcal{W},\mathcal{W}^{+}$-injective, then excluded middle holds in the universe $\mathcal{W}$.

Proof.

Given a proposition $P$, we have that the type $D\overset{\text{def}}{=}P+(P\to\mathbb{0})+\mathbb{1}_{\mathcal{W}}$ is injective by the assumption. Hence it is algebraically injective in an unspecified way by Proposition 42. And so it is algebraically flabby in an unspecified way. By the lemma, $P$ is decidable in an unspecified way, but then it is decidable because the decidability of a proposition is a proposition. ∎

With resizing we can do better:

63 Lemma**.**

Under $\Omega$-resizing, if every inhabited type in a universe $\mathcal{U}$ is $\mathcal{U},\mathcal{U}$-injective, then excluded middle holds in $\mathcal{U}$.

Proof.

Given a proposition $P$, we have that the type $D\overset{\text{def}}{=}P+(P\to\mathbb{0})+\mathbb{1}_{\mathcal{U}}$ is injective by the assumption. Hence it is injective in an unspecified way by Theorem 54. And so it is algebraically flabby in an unspecified way. By the lemma, $P$ is decidable in an unspecified way, and hence decidable. ∎

64 Theorem**.**

Under $\Omega$-resizing, all inhabited types in a universe $\mathcal{U}$ are $\mathcal{U},\mathcal{U}$-injective if and only if excluded middles holds in $\mathcal{U}$.

It would be interesting to get rid of the resizing assumption, which, as we have seen, is not needed for the equivalence of the algebraic injectivity of all pointed types with excluded middle.