A Higher Structure Identity Principle

TL;DR

This paper establishes a Structure Identity Principle for complex theories on types of h-level 3 within Univalent Foundations, using a novel notion of saturation for a broad class of definable structures.

Contribution

It introduces a general saturation concept and proves a Structure Identity Principle for high-level types in Univalent Foundations, advancing the understanding of structural equivalences.

Findings

Proves a Structure Identity Principle for h-level 3 types.

Defines a new notion of saturation for structures.

Applies to a broad class of structures in Univalent Foundations.

Abstract

We prove a Structure Identity Principle for theories defined on types of $h$-level 3 by defining a general notion of saturation for a large class of structures definable in the Univalent Foundations.

Equations

$$l(K)=\left\{\begin{array}[]{ll}1&\mbox{if $K$ is the codomain only of $1_{K}$}\\ \underset{f\colon K_{f}\rightarrow K}{\text{sup}}l(K_{f})+1&\mbox{otherwise}\end{array}\right.$$

$$d{t}_0=d{t}_2,c{t}_1=c{t}_2,d{t}_1=c{t}_0$$

$$ds=dt,cs=ct$$

$$\bigg{(}\underset{x,x^{\prime}\colon A}{\Pi}f(x)=f(x^{\prime})\rightarrow x=x^{\prime}\bigg{)}\times\bigg{(}\underset{y\colon B}{\Pi}\underset{x\colon A}{\Sigma}f(x)=y\bigg{)}$$

$${\text{Struc}}_{{\mathcal{L}}_{\text{rg}}}{=}_{\text{df}}\underset{O:\mathcal{U}}{\Sigma }\underset{A:O\to O\to \mathcal{U}}{\Sigma }\underset{x:O}{\Pi }A(x,x)\to \mathcal{U}$$

$$\textbf{Struc}_{\mathcal{L}_{\text{rg}}^{=_{A}}}=_{\text{df}}\underset{\mathcal{M}\colon\textbf{Struc}_{\mathcal{L}_{\text{rg}}}}{\Sigma}\>\>\bigg{(}\underset{x,y\colon O^{\mathcal{M}}}{\Pi}A^{\mathcal{M}}(x,y)\times A^{\mathcal{M}}(x,y)\rightarrow\mathcal{U}\bigg{)}$$

$$||\underset{x:O^{\mathcal{M}}}{\Sigma }\underset{f:A^{\mathcal{M}}(x,x)}{\Pi }{I}^{\mathcal{M}}(f)|{|}_1$$

$${\text{Mod}}_{{\mathbb{T}}_1}{=}_{\text{df}}\underset{\mathcal{M}:{\text{Struc}}_{\mathcal{L}}}{\Sigma }||\underset{x:O^{\mathcal{M}}}{\Sigma }\underset{f:A^{\mathcal{M}}(x,x)}{\Pi }{I}^{\mathcal{M}}(f)|{|}_1$$

$$\underset{s\in S}{\times }{R}_s$$

$${\mathcal{L}}_x{=}_{\text{df}}\{R\in \text{ob}\mathcal{L}|R>K\text{ and }\forall q\in \mathcal{L}(R,K)\forall p_1,p_2\in \mathcal{L}(K,K^{\prime }),p_{1}q=p_{2}q\Rightarrow x_{p_1}=x_{p_2}\}$$

$$\text{Ind}(x,y)\in {\text{Form}}_{\mathcal{L}}(\text{dep}(x)\cup \text{dep}(y))$$

$$A(\alpha )\simeq A(\beta )\in {\text{Form}}_{\mathcal{L}}(\partial \alpha \cup \partial \beta )$$

$${\text{Ind}}_R^p(x,y)$$

$${\Gamma }_{\alpha ,\beta }=\partial \alpha \cup \partial \beta \setminus (\text{dep}({\alpha }_p)\cup \text{dep}({\beta }_p))\}/{\sim }_c$$

$${\text{Ind}}_R(x,y)$$

$${\text{Ind}}_{{=}_A}^s(f,g)=\{\forall h(f{=}_{A}h\simeq g{=}_{A}h),f{=}_{A}f\simeq g{=}_{A}f,f{=}_{A}g\simeq g{=}_{A}g\}$$

$$\text{Ind}(x,y){=}_{\text{df}}\underset{R\in {\mathcal{L}}_x\cap {\mathcal{L}}_y}{\bigwedge }{\text{Ind}}_R(x,y)$$

$$\text{Ind}(f,g)$$

$$=\{\forall h(f{=}_{A}h\simeq g{=}_{A}h),f{=}_{A}f\simeq g{=}_{A}f,f{=}_{A}g\simeq g{=}_{A}g\}\wedge$$

$$\{\forall h(h{=}_{A}f\simeq h{=}_{A}g),f{=}_{A}f\simeq f{=}_{A}g,g{=}_{A}f\simeq g{=}_{A}g\}$$

$$K(\alpha )\simeq K(\beta )$$

$$\displaystyle\>\>\>\>\>\>\>\>\>\big{[}\forall x,x^{\prime}\colon K(\alpha)\forall y,y^{\prime}\colon K(\beta).\text{Ind}(x,y)\wedge\text{Ind}(x^{\prime},y^{\prime})\wedge y\cong y^{\prime}\rightarrow x\cong x^{\prime}\big{]}\wedge$$

$$\displaystyle\>\>\>\>\>\>\>\>\>\big{[}\forall y\colon K(\beta)\exists x\colon K(\alpha).\text{Ind}(x,y)\big{]}$$

$$A(x,x)\simeq A(y,y)$$

$$\displaystyle\big{[}\forall f\colon A(x,x)$$

$$\displaystyle\big{[}\forall f,f^{\prime}\colon A(x$$

$$\displaystyle\big{[}\forall g\colon A(y,y)$$

$$\displaystyle\big{[}\forall f\colon A(x,x)$$

$$\displaystyle\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\rightarrow(I(g)\simeq I(h))\big{]}\wedge$$

$$\displaystyle\big{[}\forall f,f^{\prime}\colon A(x$$

$$\displaystyle\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\>\rightarrow(I(f)\simeq I(f^{\prime}))\big{]}\wedge$$

$$\displaystyle\big{[}\forall g\colon A(y,y)$$

$${\text{Ind}}_R^p(x,y)\iff {\text{Ind}}_R^p(x^{\prime },y)\iff {\text{Ind}}_R^p(x,y^{\prime })\iff x\cong x^{\prime }\iff y\cong y^{\prime }\iff \top$$

$$\forall x:K(\alpha )\exists y:K(\beta ).\top \wedge \forall y:K(\beta )\exists x:K(\alpha ).\top$$

$${\text{refl}}_{\text{Ind}}$$

$${\text{sym}}_{\text{Ind}}$$

$${\text{tran}}_{\text{Ind}}$$

Full text

Formalizing mathematics in the framework of the Univalent Foundations [HTT] presents unique challenges and opportunities. One of the main opportunities is the ability to formalize higher-level mathematics (categories, higher categories etc.) in an invariant way by imposing appropriate saturation conditions. This is done, for example, in [HTT] for category theory (cf. Definition 9.1.6). An interesting challenge is how to express general saturation conditions that apply to wide classes of structures that can be formalized in UF. The main contribution of this paper is to provide such a general definition of a saturation condition for a wide class of definable structures and to use it to prove a Structure Identity Principle for all “category-level” (or “$3$-level”) such structures.

To illustrate, consider the following theorem from [HTT]:

By regarding univalent categories as a “saturated” version of an unsaturated structure (i.e. of precategories) we can regard the above result as a specific instance of a more general result of the following form:

The purpose of this paper is to make precise and prove a result of this form, such that Theorem 9.4.16 follows as a special case (as an assurance of adequacy).

This is done as follows. An “$\mathcal{L}$-theory $\mathbb{T}$” will be given by a theory over a FOLDS signature $\mathcal{L}$ in the sense of Makkai [MFOLDS], i.e. a finite inverse category $\mathcal{L}$. A “model $\mathcal{M}$” of $\mathbb{T}$ (or just simply an “$\mathcal{L}$-structure”) will be given by an interpretation of FOLDS into HoTT as has been described in [TsemHMT]. An “$\mathcal{L}$-equivalence” between two such models $\mathcal{M}$ and $\mathcal{N}$ will be given by Makkai’s notion of FOLDS $\mathcal{L}$-equivalence, which in set theory is defined as the existence of a span of fiberwise surjective $\mathcal{L}$-homomorphisms from $\mathcal{M}$ to $\mathcal{N}$. What remains is to define what a “saturated” model is in this setting and indeed this is the main contribution of this paper.

The general definition of saturation is based on the following intuitive idea: a structure is saturated if any two indistinguishable components in it are identical. To make this idea precise we will define for any FOLDS signature $\mathcal{L}$ a general notion of isomorphism for any sort $K$ in $\mathcal{L}$ and any $x,y\colon K$ in the form of an $\mathcal{L}$-formula $x\cong y$. The intuition behind $x\cong y$ is that “$x$ and $y$ are indistinguishable by any sort which depends on $K$, in any position”. Spelling out exactly how “indistinguishable” and “position” are to be formalized constitutes the main task of the syntactic portion of the paper. Roughly, this is done by a mutually inductive definition of a formula $\text{Ind}(x,y)$ expressing indistinguishability (up to equivalence) with respect to sorts “upstairs” (Definition 2.5) and then a notion of equivalence which says that the indistinguishability relation $\text{Ind}(x,y)$ is a bijection (up to indistinguishability) (Definition 2.10).

We can then interpret the formula $x\cong y$ for any $\mathcal{L}$-structure $\mathcal{M}$ and given this we can define what it means for such an $\mathcal{M}$ to be saturated at any sort $K$ and also associated notions of total saturation, saturation at a given level etc. This forms the key definition of this paper (Definition 3.2) which provides a very wide notion of saturation of which the known examples of saturated structures become special instances. For example, we will show that the totally saturated models of the theory of categories are the univalent categories (Proposition 4.13) whereas precategories are the “$2$-saturated” such models (Proposition 4.10).

Finally, given this general notion of saturation, we will prove a precise version of Pre-Theorem 0.2 for FOLDS signatures $\mathcal{L}$ of “height” 3. Signatures of this height can be thought of as expressing theories whose saturated models are given by structures on $1$-types, i.e. on types of $h$-level 3. The theory of precategories is an example of such a theory. This is done in Theorem 4.9, the main result of this paper, which can be thought of as a Structure Identity Principle for structures of $h$-level $3$.

Outline of the Paper

In Section 1 we fix notation and introduce the relevant concepts from FOLDS. In Section 2 we give the definition of $x\cong y$ for any FOLDS signature $\mathcal{L}$ and any $x,y\colon K$ (Definitions 2.5 and 2.10). In Section 3 we define saturation for FOLDS $\mathcal{L}$-structures in type theory (Definition 3.2) and prove certain useful properties of our definitions. Finally, in Section 4 we internalize the notion of FOLDS equivalence in type theory and use this definition to prove a Structure Identity Principle for $3$-level structures (Theorem 4.9). We also provide proofs that our higher Structure Identity Principle gives the right answer in the case of the theory of categories (Propositions 4.10 and 4.13).

1. Preliminaries and Notation

1.1. FOLDS

By FOLDS we understand the system of Makkai introduced in [MFOLDS]. We here introduce the relevant concepts. A FOLDS signature $\mathcal{L}$ is a finite inverse category. We assume each signature $\mathcal{L}$ comes with a level function $l\colon\text{ob}\mathcal{L}\rightarrow\mathbb{N}$ defined as follows

[TABLE]

Note that “top-level” sorts are assigned level $1$, contrary to Makkai’s original definition. This is done to foreshadow that these sorts, when saturated, will be interpreted as types of $h$-level 1. However, we will write $K>K^{\prime}$ to denote that $K$ has a lower level than $K^{\prime}$ (i.e. that $l(K)<l(K^{\prime})$ in order to think of $K>K^{\prime}$ as saying that $K$ is “higher” (and therefore depends on) $K^{\prime}$. We also write $\textrm{h}(\mathcal{L})$ for the height of $\mathcal{L}$, i.e. the maximum level of any sort $K$ in $\mathcal{L}$ (since we are assuming that $\mathcal{L}$ is finite, the height will also always be finite). For any $K\in\text{ob}\mathcal{L}$ we will write $\mathcal{L}\downarrow K$ for the comma category under $K$ in $\mathcal{L}$. We will generally use the notation $\mathcal{L}(K,K^{\prime})$ for the hom-sets of $\mathcal{L}$.

Variables for $\mathcal{L}$ are given by a functor $V\colon\mathcal{L}\rightarrow\textbf{Set}$ satisfying certain obvious conditions, e.g. that for any $K\neq K^{\prime}$, $V(K)$ and $V(K^{\prime})$ are countably infinite disjoint sets etc. We will write $x\colon K$ for $x\in V(K)$, for any $K\in\text{ob}\mathcal{L}$. For any $x\colon K$ and $f\in\mathcal{L}(K,K_{f})$ we write $x_{f}$ for $V(f)(x)$. It is helpful to think of $f$ as a position and $x_{f}$ as the variable that $x$ depends on in position $f$. We write $\text{dep}(x)$ for the set $\{x_{f}\>|\>\text{dom}(f)=K\}$, i.e. the set of dependent variables of $x$ and $\partial x$ for the the set of dependent variables of $x$ but omitting $x$, i.e the boundary of $x$.

A context is a finite subfunctor of $V$. A context morphism is a natural transformation $s\colon\Gamma\rightarrow\Delta$. For any two contexts $\Gamma$ and $\Delta$ we write $\Gamma\cup\Delta$ for their union as subobjects of $V$, i.e. the functor that takes $K\mapsto\Gamma(K)\cup\Delta(K)$. It is not hard to see that both $\text{dep}(x)$ and $\partial x$ define contexts. We will use the symbol $=$ for equality of contexts and variables.

We define the syntax associated to $\mathcal{L}$ by an inductive definition in the usual way (except the clauses for quantifiers are a little more involved that first-order logic) and we write $\textbf{Form}_{\mathcal{L}}(\Gamma)$ for the set of $\mathcal{L}$-formulas in context $\Gamma$. We write FV($\phi$) for the free variables of an $\mathcal{L}$-formula $\phi$. Substitution along a context morphism is defined in the expected way and we write $s(\phi)$ for the result of substituting the variables in a formula $\phi$ in context $\Gamma$ along $s\colon\Gamma\rightarrow\Delta$. As usual, we consider formulas up to $\alpha$-equivalence, denoted by $\equiv_{\alpha}$, i.e. up to renaming of their bound variables. A theory $\mathbb{T}$ in $\mathcal{L}$ is a set of $\mathcal{L}$-sentences. It is also useful (for the sake of Definition 2.5) to define the coarser notion of contextual equivalence of formulas $\phi$ (in context $\Gamma$) and $\psi$ (in context $\Delta$), denoted $\sim_{c}$, as follows: $\phi\sim_{c}\psi$ iff there exists an isomorphism $s\colon\Gamma\rightarrow\Delta$ such that $s(\phi)\equiv_{\alpha}\psi$. In other words, two formulas are contextually equivalent if we can rename the free variables of one in such a way as to make it $\alpha$-equivalent to the other. This notion is helpful in distinguishing repeat uses of the same variable in formulas, e.g. $\phi(x,x)$ is not contextually equivalent to $\phi(x,y)$ but $\phi(x,y)$ is contextually equivalent to $\phi(z,w)$.

For $R\in\text{ob}\mathcal{L}$ with $l(R)=1$ and $\alpha\colon R$ we write $R(\alpha)$ as syntactic sugar for the formula $\exists\alpha\colon R.\top$. This means that $\text{FV}(R(\alpha))=\partial\alpha$ which means that if $\partial\alpha=\partial\beta$ then $R(\alpha)\equiv_{\alpha}R(\beta)$.

For a set of variables $\Gamma$ (not necessarily a context) we write $\forall\Gamma\phi$ for the universal closure of $\phi$ under all variables in $\Gamma$. When this is done we will assume that $\forall\Gamma\phi$ is well-formed, i.e. that $\text{FV}(\forall\Gamma\phi)$ is a well-formed context. For a given set of formulas $S$, by $\bigwedge S$ we will mean the conjunction of all formulas in $S$ (and similarly for $S_{1}\wedge S_{2}$). We will also reserve the symbol $\Leftrightarrow$ for logical equivalence over a standard deductive system for FOLDS (cf. [MFOLDS] for details). Alternatively, for the purposes of this paper one may take the logical consequence relation $\Rightarrow$ to mean simply derivability in the type-theoretic semantics of FOLDS formulas (cf. [TsemHMT] for a detailed explanation of these semantics). For example without any loss of content one may simply take something like $\phi\Rightarrow\psi$ to mean that given a term of the interpretation of the formula $\phi$ as a type one can produce a term of the type $\psi$ in type theory. We will write $\mathbb{T}\models\phi\Leftrightarrow\psi$ to denote $\mathbb{T}$-provable logical equivalence of $\phi$ and $\psi$.

Several examples of FOLDS signatures will come in handy for the purpose of illustration, so we define them here, with the level of each sort displayed on the left. We will denote by $\mathcal{L}_{\text{rg}}$ the FOLDS signature

\textstyle{1}$$\textstyle{I\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{i}$$\textstyle{2}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{d}$$\scriptstyle{c}$$\textstyle{3}$$\textstyle{O}

subject to the relation $di=ci$. $\mathcal{L}_{\text{rg}}$ can be thought of as a signature useful for formalizing reflexive graphs.

By $\mathcal{L}_{\text{rg}}^{=_{A}}$ we will denote the FOLDS signature extending $\mathcal{L}_{\text{rg}}$ where we add an “equality” on $A$

[TABLE] \textstyle{1}$$\textstyle{I\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{i}$$\textstyle{=_{A}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{s}$$\scriptstyle{t}$$\textstyle{2}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{d}$$\scriptstyle{c}$$\textstyle{3}$$\textstyle{O}

subject to the relations $di=ci$, $ds=dt$, $cs=ct$.

By $\mathcal{L}_{\text{cat}}$ we will denote the following FOLDS signature

[TABLE] \textstyle{1}$$\textstyle{\circ\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{t_{0}}$$\scriptstyle{t_{1}}$$\scriptstyle{t_{2}}$$\textstyle{I\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{i}$$\textstyle{=_{A}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{t}$$\scriptstyle{s}$$\textstyle{2}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{c}$$\scriptstyle{d}$$\textstyle{3}$$\textstyle{O}

subject to the same relations as $\mathcal{L}_{\text{rg}}^{=_{A}}$ in addition to the following:

[TABLE]

[TABLE]

By $\mathbb{T}_{\text{cat}}$ we will denote the $\mathcal{L}_{\text{cat}}$-theory of categories axiomatized in the usual way, i.e. by adding axioms expressing that $\circ$ is an associative operation for which $I$ picks out a right and left unit etc. (cf. [TsemHMT] for details).

1.2. Homotopy Type Theory

On the semantic side, we will assume that we will work with some Homotopy Type Theory to which we will refer generically as type theory. The system in [HTT] will do just fine, for example. In particular, we will assume that all the types in terms of which $\mathcal{L}$-structures are defined live in some univalent universe $\mathcal{U}$. The terms proposition, set, $n$-type, $h$-level, precategory, univalent category etc. refer to the standard definitions as given e.g. in [HTT]. We will denote by PreCat the type of precategories and by UniCat the type of univalent categories. For a given type $A$ and $a,b\colon A$ we will write $a=_{A}b$ for the identity type of $a$ and $b$, often abbreviating to $a=b$ when $A$ is clear from the context. For a given $f\colon A\rightarrow B$ we will also use the abbreviation $\mathtt{bij}(f)$ for the type

[TABLE]

We use the notation $||A||_{\mathbf{n}}$ for the $n$-truncation of a type $A$, where $n$ will denote the $h$-level, e.g. for $n=1$, $||A||_{\mathbf{1}}$ is the propositional truncation.

Any FOLDS signature $\mathcal{L}$ can be translated as data in type theory in a straightforward way, giving us a notion of a type $\textbf{Str}_{\mathcal{L}}$ of $\mathcal{L}$-structures a term $\mathcal{M}$ of which can be thought of as an $\mathcal{L}$-structure (cf. [TsemHMT] for details). This is done by extracting a $\Sigma$-type from $\mathcal{L}$ by induction on the level of $\mathcal{L}$. For example, we have

[TABLE]

Whenever we pick a specific $\mathcal{L}$-structure $\mathcal{M}\colon\textbf{Struc}_{\mathcal{L}}$ we will denote by $K^{\mathcal{M}}$ the interpretation of any sort $K\in\text{ob}\mathcal{L}$. For example, the data of $\mathcal{M}\colon\textbf{Struc}_{\mathcal{L}_{\text{rg}}}$ can be written as $\langle O^{\mathcal{M}},A^{\mathcal{M}},I^{\mathcal{M}}\rangle$. To further illustrate the notation, we can for instance define

[TABLE]

Similarly, all $\mathcal{L}$-formulas can be translated under the usual propositions-as-types translation of the quantifiers and logical connectives (with $\exists$ interpreted as truncated $\Sigma$ and $\vee$ interpreted as truncated $+$ ensuring that the interpretations are all $h$-props). For example, for the $\mathcal{L}_{\text{rg}}$-sentence $\exists x\colon O.\forall f\colon A(x,x).I(f)$ will be interpreted in an $\mathcal{L}$-structure $\mathcal{M}$ as the proposition

[TABLE]

When necessary we will write $\phi^{\mathcal{M}}$ to refer to the interpretation of a certain $\mathcal{L}$-formula into an $\mathcal{L}$-structure $\mathcal{M}$. We can then obtain a notion of satisfaction of a formula $\phi$ in an $\mathcal{L}$-structure $\mathcal{M}$ and therefore a notion of a model $\mathcal{M}$ of an $\mathcal{L}$-theory $\mathbb{T}$ (where a theory $\mathbb{T}$ is a set of $\mathcal{L}$-sentences). We write $\textbf{Mod}_{\mathbb{T}}$ for the type of $\mathbb{T}$-models, i.e. those $\mathcal{L}$-structures that satisfy all $\phi\in\mathbb{T}$. For example, for the $\mathcal{L}_{\text{rg}}$-theory $\mathbb{T}_{1}=\{\exists x\colon O.\forall f\colon A(x,x).I(f)\}$ we have

[TABLE]

Finally, note that a well-formed context $\Gamma$ in the sense of FOLDS clearly gives rise to a well-formed context $\Gamma^{\mathcal{M}}$ in type theory, and so we will freely use the notation $\Gamma^{\mathcal{M}}$ to denote the interpretation of $\Gamma$ in some $\mathcal{L}$-structure $\mathcal{M}$.

1.3. Note on Metatheory

Throughout this paper we work in a set-theoretic meta-theory. This should already be clear by our use of e.g. the symbol $\in$ in our definition of a FOLDS signature and its associated notions. However, we aim for this set-theoretic metatheory to be “foundation-agnostic” in that our definitions and arguments could equally well be formalized within an extensional set theory like ZF or a suitable model of a structural set theory inside the Univalent Foundations.

One further clarification is in order, to avoid any confusion. Since our metalanguage is set-theoretic we will often refer to expressions in type theory using set-theoretic abbreviations. For example, the symbol

[TABLE]

might refer to a well-formed type in type theory (a non-dependent sum with $S$-many components) but is not itself to be understood as a well-formed type in type theory. Rather, it is a description of such a type in our set-theoretic metalanguage (hence the use of “$\in$” under $\times$). Similarly, in Section 2 below we will construct set-theoretically certain FOLDS formulas which we then use to describe certain well-formed types in type theory. But our FOLDS formulas, as constructed, are not themselves to be understood as constructed inside type theory. In particular, our description of the relevant formulas will contain certain distinctions between variables that will be internally invisible to the type theory.

2. A Syntactic Definition of Isomorphism

Fix a FOLDS signature $\mathcal{L}$. Let $x\colon K$ for some $K\in\text{ob}\mathcal{L}$. Then we define the set of $x$-compatible sorts as follows:

[TABLE]

If $R\in\mathcal{L}_{x}$ we say that $x$ is $R$-compatible. The idea is that a certain variable is not $R$-compatible if its dependent variables violate some identity that $R$ requires in order to be defined. The following example illustrates this.

Example 2.1**.**

In $\mathcal{L}_{\text{rg}}$ a variable $f\colon A$ with $f_{d}=x$ and $f_{c}=y$ (and where $x\neq y$) is not $I$-compatible. This is because $di=ci$ yet $f_{c}\neq f_{d}$ as just stated. However, in $\mathcal{L}_{\text{rg}}^{=_{A}}$ $f$ is $=_{A}$-compatible (since $=_{A}$ does not “require” an identification between “source” and “target”).

Remark 2.2*.*

If $\partial x=\partial y$ then $\mathcal{L}_{x}=\mathcal{L}_{y}$. In other words, variables with the same boundary are compatible with exactly the same sorts.

The idea of the syntactic definition of isomorphism for $K$ goes as follows. For any variables $x,y\colon K$ we will define by mutual induction a formula

[TABLE]

that expresses the fact that $x$ and $y$ are “indistinguishable up to equivalence” by any of the sorts they are jointly compatible with (i.e. for all $R\in\mathcal{L}_{x}\cap\mathcal{L}_{y}$) and where “equivalence” will be defined, for any $\alpha,\beta\colon A$, as a formula

[TABLE]

Our first goal is to define these formulas (by mutual induction).

We begin with the definition of indistinguishability, i.e. of the formula $\text{Ind}(x,y)$. Let $x,y\colon K$ and $R\in\mathcal{L}_{x}\cap\mathcal{L}_{y}$ and $p\in\mathcal{L}(R,K)$. Then we have the following two definitions expressing respectively “$x$ and $y$ cannot be distinguished by $R$ in position $p$, up to equivalence” and “$x$ and $y$ cannot be distinguished by $R$ in any position, up to equivalence”:

[TABLE]

Remark 2.3*.*

The use of $\sim_{c}$ in $\text{Ind}_{R}^{p}$ ensures that $\text{Ind}_{R}^{p}(x,y)$ is finite. Strictly speaking, this makes $\text{Ind}_{R}^{p}(x,y)$ a “conjunction” of equivalence classes of formulas up to contextual equivalence. We brush over the difficulty by assuming we in each case choose a canonical representative for the equivalence class.

Example 2.4**.**

Take $\mathcal{L}_{\text{rg}}^{=A}$. Then we have

[TABLE]

where we have used the standard abbreviation $f=_{A}g$ for the sort $=_{A}(f,g)$. Intuitively, $\text{Ind}^{s}_{A}(f,g)$ expresses the fact that “binary relation” $=_{A}$ should not distinguish between $f$ and $g$ when they are “plugged in” position $s$, i.e. in the “source” position, which we take to be the left-hand side. And “does not distinguish” is in turn understood as the existence of an equivalence (to be defined below) between the sorts $f=_{A}h$ and $g=_{A}h$ that we obtain by plugging $f$ and $g$ into the $s$ position, for any $h$. Clearly this is something that we would expect of the binary relation of equality, although of course at this point this is simply uninterpreted syntax.

Definition 2.5** ($\text{Ind}(x,y),x\cong y$).**

For $x,y\colon K$ we define the following formula

[TABLE]

which we express as $x$ and $y$ are indistinguishable. In the special case when $\partial x=\partial y$ we write $x\cong y$ for $\text{Ind}(x,y)$ and say that $x$ and $y$ are isomorphic.

Observe that we have $\text{FV}(\text{Ind}(x,y))=\text{dep}(x)\cup\text{dep}(y)$. $\text{Ind}(x,y)$ captures the intended meaning that “$x$ and $y$ are indistinguishable up to equivalence by any $x$-compatible and $y$-compatible $R$, in any position”. Of course, for this definition to be useful we also need to define equivalence as it appears in $\text{Ind}_{R}^{p}(x,y)$ (i.e. in the formula $\forall\Gamma_{\alpha,\beta}R(\alpha)\simeq R(\beta)$), which we do below. But even before we do that, we can draw some useful conclusions in some degenerate cases.

Example 2.6**.**

In $\mathcal{L}_{\text{rg}}$ let $f,g\colon A(x,y)$. Then $\mathcal{L}_{f}=\mathcal{L}_{g}=\varnothing$ which means $f\cong g\equiv_{\alpha}\top$ (as the empty conjunction). This is a strange but I think correct conclusion. For if two terms cannot be distinguished by any data in the FOLDS signature (i.e. they have no compatible sorts) then the appropriate saturation condition is to regard them as always isomorphic.

Example 2.7**.**

A bit stranger is the situation where, say, $f\colon A(x,x)$ and $g\colon A(x,y)$, still in $\mathcal{L}_{\text{rg}}$. In this case, we have $\mathcal{L}_{f}\neq\varnothing$, but $\mathcal{L}_{f}\cap\mathcal{L}_{g}=\varnothing$, and so Definition 2.5 dictates that we should regard $f$ and $g$ as always indistinguishable. Formally, this does not seem to be problematic but it is a little harder to make sense of since there is certainly something in the syntax that distinguishes $f$ and $g$, namely that in the case of the former we have $f_{d}=f_{c}$ but the analogous equation does not hold of $g$.

Example 2.8**.**

In $\mathcal{L}_{\text{rg}}^{=_{A}}$, let $f,g\colon A(x,y)$. Then $\mathcal{L}_{f}=\mathcal{L}_{g}=\{=_{A}\}$ and we have

[TABLE]

Proposition 2.9**.**

For $K\in\emph{\text{ob}}\mathcal{L},l(K)=1,x,y\colon K$ we have $\emph{\text{Ind}}(x,y)\equiv_{\alpha}\top$.

Proof.

We have $\mathcal{L}_{x}=\mathcal{L}_{y}=\varnothing$ hence $\text{Ind}(x,y)$ is an empty conjunction and therefore the same thing as $\top$. ∎

We now turn our attention to the definition of $\simeq$.

Definition 2.10** ($K(\alpha)\simeq K(\beta)$).**

For $K\in\text{ob}\mathcal{L}$ and $\alpha,\beta\colon K$ we define the following formula:

[TABLE]

When the formula holds we say that $K(\alpha)$ is equivalent to $K(\beta)$.

To aid understanding, here is the intended meaning behind $K(\alpha)\simeq K(\beta)$: the first conjunct expresses that $\text{Ind}(x,y)$ is a functional relation (up to $\cong$), the second line expresses that $\text{Ind}(x,y)$ is injective (up to $\cong$), and the third line express that $\text{Ind}(x,y)$ is surjective. Putting all this together, $K(\alpha)\simeq K(\beta)$ can be understood as saying “$\text{Ind}(x,y)$ is an equivalence up to $\cong$”.

Note that we have $\text{FV}(K(\alpha)\simeq K(\beta))=\partial\alpha\cap\partial\beta$. Indeed, since $K(\alpha)\simeq K(\beta)$ depends only on the respective boundaries of $\alpha$ and $\beta$ it is usually helpful to write $K(\partial\alpha)\simeq K(\partial\beta)$ when the variables in the boundary can be explicitly listed. For example, we can write $A(x,y)$ for the sort of “arrows” in $\mathcal{L}_{\text{rg}}$ dependent on $x,y\colon O$ instead of the more alienating $A(f)$ (for some $f$ that depends on $x$ and $y$).

Example 2.11**.**

In $\mathcal{L}_{\text{rg}}$ let $x,y\colon O$. Then we have:

[TABLE]

The only sort that could distinguish two variables $f\colon A(x,x)$ and $g\colon A(y,y)$ in $\mathcal{L}_{\text{rg}}$ is $I$. Therefore, $\text{Ind}(f,g)$ becomes $(I(f)\simeq I(g))$ as prescribed by the definition of Ind. So what we get, intuitively, is that $A(x,x)$ and $A(y,y)$ are equivalent iff there is a one-to-one correspondence between “terms” $f$ of $A(x,x)$ and “terms” $g$ of $A(y,y)$ that give equivalent sorts when plugged into $I$, i.e. such that $I(f)\simeq I(g)$. Except this “one-to-one correspondence” is one-to-one only up to $\cong$ which in the case of $\mathcal{L}_{\text{rg}}$ amounts to the exact same property, namely $g\cong h$ iff $g$ and $h$ produce equivalent sorts when plugged into the “type family” $I$. We clearly here want to regard $I$ as a predicate (e.g. picking out which “arrows” are “identities”) which would make the equivalence $I(f)\simeq I(g)$ a logical equivalence. This is what the next proposition establishes for sorts, like $I$, of level $1$.

Proposition 2.12**.**

For $K\in\emph{\text{ob}}\mathcal{L}$, $l(K)=1$ we have $K(\alpha)\simeq K(\beta)\Leftrightarrow K(\alpha)\leftrightarrow K(\beta)$

Proof.

Note that $\mathcal{L}_{\alpha}=\mathcal{L}_{\beta}=\varnothing$ which means that for $x,x^{\prime}\colon K(\alpha)$ and $y^{\prime},y\colon K(\beta)$ we have

[TABLE]

Therefore, by Proposition 2.9, we can see that $K(\alpha)\simeq K(\beta)$ is logically equivalent to

[TABLE]

which in turn is logically equivalent to $K(\alpha)\leftrightarrow K(\beta)$. ∎

Using propositions 2.9 and 2.12 we can successively obtain formulas for $x\cong y$ for $x,y\colon K$ for sorts $K$ or arbitrarily high level. We will write $\cong_{K}$ for the isomorphism relation defined on a sort $K$, or $\cong_{K(\alpha)}$ whenever we want to make the specific context explicit. We now prove the following crucial result, which is the last general result we will carry out “formally”, i.e. assuming an arbitrary formal system for FOLDS.

Proposition 2.13**.**

Let $\mathcal{L}$ be a FOLDS signature. For any $K\in\text{ob}\mathcal{L}$, $\emph{\text{Ind}}(x,y)$ is an equivalence relation. That is, it satisfies the following three properties:

[TABLE]

[TABLE]

[TABLE]

In particular, for any $K\in\text{ob}\mathcal{L}$, $x\cong y$ is an equivalence relation.

.

Proof.

We proceed by induction on the level of $K$.

Base Step: For any sort $K$ with $l(K)=1$ the statement follows immediately from Proposition 2.9.

Inductive Step: For any choices of $\alpha,\beta,\gamma$ define the following formulas:

[TABLE]

[TABLE]

[TABLE]

Let us denote the conjunction of the three statements above as $(\text{eqr}^{K}_{\simeq})$ and similarly let us denote by $(\text{eqr}^{K}_{\text{Ind}})$ the conjunction of the three sentences in the statement of the Proposition. Similarly, let us write $(\text{eqr}_{\text{Ind}}^{n})$ for the statement that for any sort $K$ with $l(K)\geq n$, $(\text{eqr}^{K}_{\text{Ind}})$ holds and $(\text{eqr}^{n}_{\simeq})$ for the analogous statement for $\simeq$. The proof of the inductive step now proceeds in two steps. First we prove that $(\text{eqr}^{n}_{\text{Ind}})\Rightarrow(\text{eqr}^{n}_{\simeq})$ and then that $(\text{eqr}^{n}_{\simeq})\Rightarrow(\text{eqr}^{n+1}_{\text{Ind}})$. Put together these give $(\text{eqr}^{n}_{\text{Ind}})\Rightarrow(\text{eqr}^{n+1}_{\text{Ind}})$ which is exactly what the inductive step requires us to prove. We take them in turn.

$(\text{eqr}^{n}_{\text{Ind}})\Rightarrow(\text{eqr}^{n}_{\simeq})$: For $(\text{refl}_{\simeq})$ we have:

[TABLE]

The last form is obtained because when $x,y$ are of the same sort we write $x\cong y$ instead of $\text{Ind}(x,y)$. The first conjunct $\forall x\colon K(\alpha)\exists y\colon K(\alpha).x\cong y\wedge(\forall y^{\prime}\colon K(\alpha).x\cong y^{\prime}\rightarrow y\cong y^{\prime})$ follows from the reflexivity of $\cong$, which is given by the inductive hypothesis. The second conjunct $\forall x,x^{\prime}\colon K(\alpha)\forall y,y^{\prime}\colon K(\alpha).x\cong y\wedge x^{\prime}\cong y^{\prime}\wedge y\cong y^{\prime}\rightarrow x\cong x^{\prime}$ follows from the symmetry and transitivity of $\cong$, which is once again given by the inductive hypothesis. Finally, the third conjunct $\forall y\colon K(\alpha)\exists x\colon K(\alpha).x\cong y$ follows from the reflexivity of $\cong$ which is once again given by the inductive hypothesis. For $(\text{sym}_{\simeq})$ we have:

[TABLE]

By the inductive hypothesis, we can assume that Ind is symmetric, which means that if $\text{Ind}(x,y)$ defines an “equivalence up to $\cong$” then $\text{Ind}(y,x)$ also defines such an equivalence. We can use this basic idea to deduce each of the conjuncts of the RHS from the LHS. We deduce the conjunct $\forall y\colon K(\alpha)\exists x\colon K(\beta).\text{Ind}(x,y)$ on the RHS as an illustration. We have:

[TABLE]

By an exactly analogous argument we can establish $(\text{tran}_{\simeq})$.

$(\text{eqr}^{n}_{\text{Ind}})\Rightarrow(\text{eqr}^{n+1}_{\text{Ind}})$: Let $K$ be a sort with $l(K)=n+1$. Firstly, note that it suffices to establish $(\text{eqr}_{\text{Ind}_{R}^{p}})$ for any $R>K$ and $p\colon R\rightarrow K$ since Ind is a conjunction over all such $R$ and $p$. Thus, the properties to be shown are the following:

[TABLE]

[TABLE]

[TABLE]

We take each of the three statements to be shown in turn. Firstly, for $(\text{refl}_{\text{Ind}_{R}^{p}})$ we have:

[TABLE]

where the equality follows since $\alpha$ and $\beta$ in the general definition of $\text{Ind}_{R}^{p}(x,y)$ are stipulated to differ only in the variable they assign to position $p$, which is here going to be the same variable. We therefore get that $\text{Ind}_{R}^{p}(x,x)$ holds iff $R(\alpha)\simeq R(\alpha)$ holds, and we know that the latter is the case from the inductive hypothesis together with the first part of the inductive step above, since $R>K$.

Secondly, for $(\text{sym}_{\text{Ind}_{R}^{p}})$ we have:

[TABLE]

Thirdly, for $(\text{tran}_{\text{Ind}_{R}^{p}})$ we have:

[TABLE]

This establishes the fact that $\text{Ind}(x,y)$ is an equivalence relation, thus completing the inductive step. ∎

We conclude this section by comparing our syntactic definitions to the usual notions. In $\mathcal{L}_{\text{cat}}$, for $x,y\colon O$ let $\text{Iso}(x,y)$ denote the formula expressing that $x$ and $y$ are isomorphic in the traditional sense (“There exist mutually inverse $f\colon A(x,y)$ and $g\colon A(y,x)$”) Call this notion categorical isomorphism. The following proposition days that in $\mathbb{T}_{\text{cat}}$ the two notions of isomorphism are logically equivalent.

Proposition 2.14**.**

$\mathbb{T}_{\text{cat}}\models\text{\emph{Iso}}(x,y)\Leftrightarrow x\cong y$**

Proof.

Firstly, note that by the axioms for equality on $A$ we will get that for any $f,f^{\prime}\colon A(x,y)$

[TABLE]

This allows us to replace (up to logical equivalence) the $=_{A}$ as it appears in $\text{Iso}(x,y)$ with our notion of $\cong_{A}$. We will assume we have done so. The ($\Rightarrow$) direction follows from the well-known result (proven e.g. in [MFOLDS]) that two categorically isomorphic objects in a category satisfy exactly the same $\mathcal{L}_{\text{cat}}$-formulas, and are therefore indistinguishable in exactly the sense of $x\cong y$. For the ($\Leftarrow$) direction, note that from the Yoneda Lemma we know that $x$ and $y$ are categorically isomorphic if and only if their images under the Yoneda embedding are isomorphic, i.e. if we have a natural isomorphism from $\textbf{y}(-,x)$ to $\textbf{y}(-,y)$. The existence of such a natural isomorphism can be expressed as the following $\mathcal{L}_{\text{cat}}$-formula

[TABLE]

By the Yoneda Lemma we have $\mathbb{T}_{\text{cat}}\models\forall x\forall y\text{Iso}(x,y)\Leftrightarrow\text{Yso}(x,y)$. But $\text{Yso}(x,y)$ is clearly a consequence of $x\cong y$ since both conjuncts appear in the definitions given above if, using Proposition 2.12, we regard $\leftrightarrow$ as an instance of $\simeq$. We thus get $x\cong y\Rightarrow\text{Iso}(x,y)$ ∎

Remark 2.15*.*

An important difference with our general notion $\cong$ and the usual notions of isomorphim is that $x\cong y$ is not necessarily “witnessed” by some other variable, e.g. an arrow $f$ as in $\text{Iso}(x,y)$. Thus, at this level, it is not possible to define a set of isomorphisms $x\cong y$, but rather only a proposition expressing whether or not $x$ and $y$ are isomorphic. To overcome this limitation, in Section 3 we will interpret the existential quantifiers as untruncated $\Sigma$-types, which will recover in the semantics the intuitively correct $h$-level.

3. Saturation in Type Theory

We now interpret our syntactic definition of isomorphism in type theory. However, in order to interpret $x\cong y$ as defined in Section 2 we make one crucial change to the usual interpretation, which is that we will not truncate the existential quantifiers that appear in the definition of $\simeq$ in Definition 2.10 and interpret them instead as full $\Sigma$-types. This is made precise in the following definition.

Definition 3.1** (Interpretation of $\cong$ in type theory).**

Let $\mathcal{L}$ be a FOLDS signature and $\mathcal{M}$ an $\mathcal{L}$-structure. For $K\in\text{ob}\mathcal{L}$ and $\alpha,\beta\colon K^{\mathcal{M}}$ we define the following type (in context $(\partial\alpha\cup\partial\beta)^{\mathcal{M}}$):

[TABLE]

By mutual induction we also define for $x,y\colon K^{\mathcal{M}}$ the following type (in context $(\text{dep}(x)\cup\text{dep}(y))^{\mathcal{M}}$):

[TABLE]

Whenever $x,y\colon K^{\mathcal{M}}$ are such that $\partial x=\partial y$ we write $x\cong^{\mathcal{M}}y$ for $\text{Ind}^{\mathcal{M}}(x,y)$. Thus, given any FOLDS signature $\mathcal{L}$, any $K\in\text{ob}\mathcal{L}$ we obtain a relation (in an appropriate context):

[TABLE]

Notation**.**

Whenever the sort of $x$ and $y$ is understood we will usually denote the type $\cong_{K^{\mathcal{M}}}(x,y)$ as simply $x\cong y$.

Let $\mathcal{M}$ be an $\mathcal{L}$-structure and $K$ any sort in $\mathcal{L}$, with $K^{\mathcal{M}}$ its interpretation. Proposition 2.13 holds also in type theory (since the proof was purely formal) and so the relation $\cong_{K^{\mathcal{M}}}$ will be reflexive. In particular, this means that given any context $\Gamma$ appropriate to $K$ we have

[TABLE]

where $\rho_{x}$ is some term witnessing the reflexivity. This gives us a canonical map

[TABLE]

by the usual induction on identity.

Definition 3.2** (Saturation).**

Let $\mathcal{L}$ be a FOLDS signature, $K\in\text{ob}\mathcal{L}$, $\Gamma$ a context appropriate to $K$ and $\mathcal{M}$ an $\mathcal{L}$-structure. Then the saturation for $K^{\mathcal{M}}$ is the following proposition (in context $\Gamma^{\mathcal{M}}$):

[TABLE]

For an $\mathcal{L}$-structure $\mathcal{M}$, we say that $K$ is saturated (or that $\mathcal{M}$ is $K$-saturated) if $\textbf{Sat}(K^{\mathcal{M}})$ is inhabited. We will say that an $\mathcal{L}$-structure is saturated at level $n$ (or $n$-saturated) if it is $K$-saturated for any $K\in\text{ob}\mathcal{L}$ with $l(K)\leq n$. We will also say that an $\mathcal{L}$-structure $\mathcal{M}$ is totally saturated if it is saturated at every level. We write $\textbf{SatStr}_{\mathcal{L}}$ (resp. $\textbf{SatStr}_{\mathcal{L}}^{n}$) for the type of totally saturated (resp. $n$-saturated) $\mathcal{L}$-structures and $\textbf{SatMod}_{\mathbb{T}}$ (resp. $\textbf{SatMod}_{\mathbb{T}}^{n}$) for the type of totally saturated (resp. $n$-saturated) $\mathbb{T}$-models (for some $\mathcal{L}$-theory $\mathbb{T}$).

Based on Definition 3.2 we regard $\textbf{Struc}_{\mathcal{L}}$ (resp. $\textbf{Mod}_{\mathbb{T}}$) as the type of “totally unsaturated” types of $\mathcal{L}$-structures (resp. models of $\mathbb{T}$). The following example illustrates the idea.

Example 3.3**.**

[TABLE]

It is important to note the difference between $=_{\text{df}}$ and $\simeq$ above. The RHS in the first line is the definition of $\textbf{Struc}_{\mathcal{L}_{\text{rg}}}$ whereas the RHS of the second line is a consequence of Proposition 2.9.

The most relevant notion for practical purposes is saturation at a particular level (or total saturation). This is because $K$-saturation for an individual $K$ may be of very little use unless we know that everything that depends on $K$ is already saturated. For example, it is not of much use to state the saturation condition for objects in a precategory unless we already know that the hom-sets are $h$-sets. On the contrary, if we know that $\mathcal{L}$ is saturated at level $n$ and $K$ is a sort of level $n$, then $K$-saturation means that isomorphism in $K$ is expressed in terms of the identity types of sorts of lower level, since these have already been declared equivalent to isomorphism. This has the consequence that saturation at a particular level correlates very well with $h$-levels as the following proposition establishes.

Proposition 3.4**.**

Let $\mathcal{L}$ be a FOLDS signature and $\mathcal{M}$ an $\mathcal{L}$-structure saturated at level $n$. Then for any $K\in\text{ob}\mathcal{L}$ with $l(K)=n$, $K^{\mathcal{M}}$ is of $h$-level $n$.

Proof.

We proceed by induction on the level of $K$. For the case $l(K)=1$ note that $\mathcal{M}$ is $1$-saturated if and only if for any sort $K$ of level $1$, the map

[TABLE]

is an equivalence. But by Proposition 2.9 we have $(x\cong^{\mathcal{M}}y)\equiv_{\alpha}\top$ and hence $\mathtt{idtoiso_{x,y}}$ is the unique map into 1. Therefore, we have

[TABLE]

and the RHS is equivalent to $\mathtt{isprop}(K^{\mathcal{M}})$. Therefore, $K$ is saturated in $\mathcal{M}$ if and only if $K^{\mathcal{M}}$ is of $h$-level 1. Now assume that the proposition holds for $n$ and let $K$ be a sort of level $n+1$ and $\mathcal{M}$ an $\mathcal{L}$-structure saturated at level $n+1$. Saturation for $K$ asserts the equivalence between the identity type on $K$ with $x\cong_{K}y$. But $x\cong y$, as a type dependent on $K^{\mathcal{M}}$, consists of the following (non-dependent) product:

[TABLE]

But $\text{Ind}_{R}^{p}$ is itself a non-dependent product of $\Pi$-types of the form

[TABLE]

Since $R^{\mathcal{M}}(\beta)$ and $R^{\mathcal{M}}(\alpha)$ are of $h$-level $n$ by the inductive hypothesis, then by the explicit form of $R(\alpha)\simeq^{\mathcal{M}}R(\beta)$ (cf. Definition 3.1) we also get that $R(\alpha)\simeq^{\mathcal{M}}R(\beta)$ is of $h$-level $n$. Since (dependent or non-dependent) products preserve $h$-level we get that $(x\cong y)^{\mathcal{M}}$ is of $h$-level $n$. Thus, if $K^{\mathcal{M}}$ is saturated, its identity types will be of $h$-level $n$, and thus $K^{\mathcal{M}}$ will itself be of $h$-level $n+1$, as required. ∎

The following lemma is also an easy consequence of our definitions. It makes precise in what way the syntactically defined notion of equivalence becomes a “functional” notion in the semantics, as long as everything “above” has been saturated.

Lemma 3.5**.**

Let $\mathcal{L}$ be a FOLDS signature and $\mathcal{M}$ an $\mathcal{L}$-structure saturated at level $n$. Then for any $K\in\text{ob}\mathcal{L}$ with $l(K)=n$ we have:

[TABLE]

Proof.

By inspecting the definition of we can see that the first type in $K(\alpha)\simeq^{\mathcal{M}}K(\beta)$ is equivalent to the type of functions $K^{\mathcal{M}}(\alpha)\rightarrow K^{\mathcal{M}}(\beta)$, since $\cong^{\mathcal{M}}$ can simply be replaced by $=_{K^{\mathcal{M}}}$ since we are assuming $\mathcal{M}$ is $n$-saturated. And the last two types state exactly that this function is injective and (split) surjective, and hence bijective. ∎

Remark 3.6*.*

Saturation as defined by Definition 3.2 relies essentially on the type-theoretic semantics of FOLDS. This means that saturated models of $\mathbb{T}$ are defined “semantically” since we have not provided a way of expressing the condition of saturation in the syntax of FOLDS. One might therefore wonder if there is a way to define saturation in an entirely syntactic manner in FOLDS, and then obtain the usual saturated notions by interpreting that definition. This can indeed be done as long as we syntactically define “transport bijections” that for each “inhabitant” of $x\cong_{K}y$ yield an “equivalence” between $A(x,\mathbf{w})$ and $A(y,\mathbf{w})$ for any $A$ dependent on $K$. We do this in full generality in [TsemHMTII] for the purposes of a completeness proof, but this machinery is somewhat independent of the purposes of this paper.

4. A Higher Structure Identity Principle

A Structure Identity Principle in the sense of [HTT] asserts something along the lines of: “Isomorphism between structures of a certain kind is equivalent to identity.” In [HTT] such a statement was proven for set-level structures, i.e. for first-order structures in the traditional sense. Here we prove a generalized Structure Identity Principle where by “structure” we will understand saturated $\mathcal{L}$-structures for (finite) FOLDS signatures $\mathcal{L}$ of height $3$ and by “isomorphic” we will understand the pre-existing notion of FOLDS equivalence, suitably internalized in type theory.

Let us first define FOLDS equivalence. Fix an $\mathcal{L}$ and let us for the time being work “extrenally” i.e. in a traditional set-theoretic set-up, writing $M,N,\dots$ instead of $\mathcal{M},\mathcal{N},\dots$ to distinguish the two notions of $\mathcal{L}$-structure. An $\mathcal{L}$-structure is a functor $M\colon\mathcal{L}\rightarrow\textbf{Set}$ and a homomorphism of $\mathcal{L}$-structures is a natural transformation between the corresponding functors. Write $y$ for the Yoneda embedding and $\hat{y}$ for subfunctor of $y$ that misses the identity on the given object. For $K\in\text{ob}\mathcal{L}$ a $K$-boundary of an $\mathcal{L}$-structure $M$ is a natural transformation $\delta\colon\hat{y}K\Rightarrow M$ and we define the fiber of $M(K)$ over $\delta$ as the set $M(K)[\delta]=\{a\in M(K)\colon\partial a=\delta\}$. Now let $M,N$ be $\mathcal{L}$-structures and let $f\colon M\rightarrow N$ be an $\mathcal{L}$-structure homomorphism and let $\delta$ be a $K$-boundary of $M$. This induces a $K$-boundary $f\circ\delta$ of $N$ by composition with $f$ and thereby induces a map $f_{\delta}$ on the fibers that takes $a\mapsto f_{K}(a)$. (The fact that this is well-defined follows from the naturality of $f$.) We now say that $f$ is fiberwise surjective if and only if for all $K$ in $\mathcal{L}$ and all $K$-boundaries $\delta$ the map $m_{\delta}\colon M(K)[\delta]\rightarrow M(K)[m\circ\delta]$ is surjective.

Definition 4.1** ([MFOLDS]).**

We say that $M$ and $N$ are FOLDS $\mathcal{L}$-equivalent if there exists an $\mathcal{L}$-structure $P$ and fiberwise surjective homomorphisms $m\colon P\rightarrow M$ and $n\colon P\rightarrow N$.

We now internalize this definition in type theory. To even write it down, however, we will now restrict ourselves to signatures $\mathcal{L}$ of height $3$ and we will assume that $\textbf{Str}_{\mathcal{L}}$ is given by the $\Sigma$-type where the relations in $\mathcal{L}$ have been “written in”. To be more precise, we will adopt the following notational conventions. For the rest of the paper $\mathcal{L}$ is a FOLDS signature of height $3$.

Notation**.**

We denote the objects in $\mathcal{L}$ of level $3$ by $\mathbf{O}=O_{1},\dots,O_{n}$, those of level $2$ by $\mathbf{A}=A_{1},\dots A_{m}$ and those of level $1$ by $\mathbf{R}=R_{1},\dots,R_{k}$. We will abbreviate a sequence of variable declarations $x_{1}\colon O_{1},\dots,x_{n}\colon O_{n}$ as $\mathbf{x}\colon\mathbf{O}$, leaving the indexing implicit. Similarly, we will abbreviate a product $A_{1}\rightarrow B_{1}\times\dots\times A_{n}\rightarrow B_{n}$ as $\mathbf{A}\rightarrow\mathbf{B}$. In general, whenever there is any boldface character in our definitions below, this will mean that the definition is taken over the whole (non-dependent) product that the implicit indexing suggests. For example, an expression of the form $\underset{\mathbf{x}\colon\mathbf{O}}{\Pi}T(m_{\mathbf{O}}(\mathbf{x}))$ is an abbreviation for

[TABLE]

Definition 4.2** ($\mathcal{L}$-homomorphism).**

Let $\mathcal{M}$ and $\mathcal{N}$ be $\mathcal{L}$-structures. The type of $\mathcal{L}\textbf{-homomorphisms}$ between $\mathcal{M}$ and $\mathcal{N}$ is defined as

[TABLE]

As suggested by the notation above, for any $m\colon\text{Hom}_{\mathcal{L}}(\mathcal{M},\mathcal{N})$ and $K\in\text{ob}\mathcal{L}$ we will write $m_{K}(\textbf{x})$ for the component of $m$ corresponding to sort $K$ in some choice of variables $\mathbf{x}$.

Definition 4.3** (Split Surjective Map).**

Let $f\colon A\rightarrow B$ be any map. Then $f$ is a split surjection if the following type is inhabited

[TABLE]

Remark 4.4*.*

The type $\mathtt{sps}(f)$ is not a proposition, and this is necessary. We must therefore think of $\mathtt{sps}(f)$ as the type of splittings of $f$ and there could be many distinct such splittings.

Definition 4.5**.**

Let $m\colon\text{Hom}_{\mathcal{L}}(\mathcal{M},\mathcal{N})$. We define

[TABLE]

We define the type of fiberwise surjective maps from $\mathcal{M}$ to $\mathcal{N}$ as

[TABLE]

We call a term $m\colon\textbf{FibSurj}(\mathcal{M},\mathcal{N})$ a fiberwise surjection.

Remark 4.6*.*

Once again, we need to make clear here that $\textbf{FibSurj}(\mathcal{M},\mathcal{N})$ is not a $\Sigma$-type comprised of an $\mathcal{L}$-homomorphism that satisfies a property, since $\mathtt{fibsurj}(f)$ will not in general be a proposition. One must rather think of fiberwise surjective maps as $\mathcal{L}$-homomrphisms together with a choice of a splitting that witnesses the fact that it is surjective.

Notation**.**

As usual we will abuse notation and treat $m\colon\textbf{FibSurj}(\mathcal{M},\mathcal{N})$ as if it were comprised purely of its “functional” part. We will thus describe the action of $m$ on terms of $\mathcal{M}$ simply by appending $m$ to the given terms, suppressing subscripts. For example, we will write $mx$ for the result of applying $m_{O}$ to some $x\colon O^{\mathcal{M}}$ and similarly we will write $mf$ for the result of applying $m_{A}(\mathbf{x})$ to some $f\colon A^{\mathcal{M}}(\mathbf{x})$. When it is required to make the particular splitting with which some $m\colon\textbf{FibSurj}(\mathcal{M},\mathcal{N})$ comes equipped we will refer to it by $s$ and describe its action in the same abbreviated manner as we do with $m$.

Definition 4.7** (Type-Theoretic FOLDS Equivalence).**

For any FOLDS signature $\mathcal{L}$ (of height $3$) and any $\mathcal{M},\mathcal{N}\colon\textbf{Str}_{\mathcal{L}}$ we define

[TABLE]

Exactly analogously we define $\simeq_{\mathcal{L}}$ on $\textbf{Mod}_{\mathbb{T}}$, $\textbf{SatStr}_{\mathcal{L}}$ and $\textbf{SatMod}_{T}$ for any $\mathcal{L}$-theory $\mathbb{T}$.

Definition 4.7 thus gives us a relation $\simeq_{\mathcal{L}}\colon\textbf{SatMod}_{\mathbb{T}}\times\textbf{SatMod}_{\mathbb{T}}\rightarrow\mathcal{U}$. All the components are now in place for us to prove our higher structure identity principle. To do so, we first require the following lemma.

Lemma 4.8**.**

Let $\mathcal{L}$ be a FOLDS signature with $\textrm{h}(\mathcal{L})=3$, $\mathcal{M}$ and $\mathcal{N}$ be saturated $\mathcal{L}$-structures, and $m\colon\emph{{FibSurj}}(\mathcal{M},\mathcal{N})$ a fiberwise surjective $\mathcal{L}$-homomorphism.

1. (1)

For any $f\colon A(\mathbf{x}),g\colon A(\mathbf{y})$ we have $\emph{\text{Ind}}^{\mathcal{N}}(mf,mg)\leftrightarrow\emph{\text{Ind}}^{\mathcal{M}}(f,g)$. In particular, we have $mf\cong mg\leftrightarrow f\cong g$. 2. (2)

For any $x,y\colon O$ we have $(mx\cong^{\mathcal{M}}my)\simeq(x\cong^{\mathcal{N}}y)$.

Proof.

For (1) we have that $\text{Ind}^{\mathcal{M}}(f,g)$ will be of the following form

[TABLE]

and similarly $\text{Ind}^{\mathcal{N}}(mf,mg)$ will be of the following form

[TABLE]

Since each $\mathbf{R}$ in the above types will be propositions so will the whole of $\text{Ind}^{\mathcal{M}}(f,g)$ and $\text{Ind}^{\mathcal{N}}(f,g)$. Therefore, it suffices to prove that they are logically equivalent. To that end define the maps

[TABLE]

and

[TABLE]

The fact that $mf\cong mg\leftrightarrow f\cong g$ follows by as the special case when $\mathbf{x}=\mathbf{y}$.

For (2), we define maps as shown:

[TABLE]

It is easy to check that $d$ and $e$ are inverses to each other, thus establishing the required equivalence. ∎

We are now ready to state and prove the main result of this paper which is a fully precise version of the guiding Pre-Theorem 0.2 in the Introduction.

Theorem 4.9** (Higher Structure Identity Principle).**

For any $\mathcal{L}$ with $\textrm{h}(\mathcal{L})=3$, any $\mathcal{L}$-theory $\mathbb{T}$ and for any saturated $\mathbb{T}$-models $\mathcal{M}$ and $\mathcal{N}$ of an $\mathcal{L}$-theory $\mathbb{T}$ we have

[TABLE]

Proof.

Let $\mathcal{M}$ and $\mathcal{N}$ be saturated models for some $\mathcal{L}$-theory $\mathbb{T}$. Clearly, it suffices to prove that $\textbf{FibSurj}(\mathcal{M},\mathcal{N})\simeq\mathcal{M}=_{\textbf{SatMod}_{\mathbb{T}}}\mathcal{N}$. We define a map

[TABLE]

Let $m\colon\textbf{FibSurj}(\mathcal{M},\mathcal{N})$. By univalence, to produce a term of type $\mathcal{M}=_{\textbf{SatMod}_{\mathbb{T}}}\mathcal{N}$ it suffices to produce component-wise equivalences for all the defining data of $\mathcal{M}$ and $\mathcal{N}$. Since $m$ is assumed fiberwise surjective we know that it provides component-wise surjections between the defining data of $\mathcal{M}$ and $\mathcal{N}$. Thus, it suffices to prove that $m$ is also component-wise an injection. We do so by taking the data of $\mathcal{L}$ level-by-level, abusing notation by ignoring the necessary transfers.

Since $\mathcal{M}$ and $\mathcal{N}$ are saturated, by Proposition 3.4 each $\mathbf{R}^{\mathcal{M}}(\mathbf{x})$ and $\mathbf{R}^{\mathcal{N}}(\mathbf{y})$ will be of $h$-level 1. Therefore, all the

[TABLE]

are trivially also injections, and therefore equivalences.

Now consider $m_{\mathbf{A}}(\mathbf{x})\colon A^{\mathcal{M}}(\mathbf{x})\rightarrow A^{\mathcal{N}}(m\mathbf{x})$. By Proposition 3.4 once again we know that $m_{\mathbf{A}}(\mathbf{x})$ is a map of $h$-sets and therefore to show that it is an equivalence it suffices to show $m_{\mathbf{A}}(\mathbf{x})(\alpha)=m_{\mathbf{A}}(\mathbf{x})(\beta)\rightarrow\alpha=\beta$. But then note that we have the following composite map

[TABLE]

where (1) is by induction on identity, (2) is by the first part of Lemma 4.8 since $m$ is assumed fiberwise surjective and (3) is because $\mathcal{M}$ is assumed saturated.

Finally, for $m_{\mathbf{O}}\colon\mathbf{O}^{\mathcal{M}}\rightarrow\mathbf{O}^{\mathcal{N}}$, to show that it is injective it suffices to show that there is an equivalence $(x=y)\simeq(mx=my)$ for any $x,y\colon\mathbf{O}$. Since both $\mathcal{M}$ and $\mathcal{N}$ are saturated this is equivalent to showing that $(x\cong y)\simeq(mx\cong my)$. But since $m$ is fiberwise surjective, this follows from the second part of Lemma 4.8.

This completes the definition of the map $k$. Now we need to show that $k$ is itself an equivalence. To see this note that by univalence any $p\colon\mathcal{M}=_{\textbf{SatMod}_{\mathbb{T}}}\mathcal{N}$ gives rise to a fiberwise surjective homomorphism $m_{p}$ with components given by the equivalences that $p$ induces. This gives a map

[TABLE]

which can easily be seen to be a two-sided inverse for $k$. Thus, $k$ is an equivalence, and this completes the proof. ∎

In order to test the adequacy of our Structure Identity Principle we need to show that it specializes to familiar cases. In this case, we need to show that Theorem 9.4.16 of [HTT] follows as a special case of our Theorem 4.9. The next series of Propositions and Lemmas aim exactly at demonstrating this.

Proposition 4.10**.**

The type ${\textbf{\emph{SatMod}}_{\mathbb{T}_{\text{cat}}}^{2}}$ of $2$-saturated models of the $\mathcal{L}_{\text{cat}}$-theory of categories is equivalent to the type PreCat of precategories.

Proof.

By the axioms for $=_{A}$ in the theory of categories we can obtain that

[TABLE]

So if $\mathcal{C}$ is any $2$-saturated $\mathbb{T}_{\text{cat}}$-model we will have

[TABLE]

And since $(f=_{A}g)^{\mathcal{C}}$ will be of $h$-level 1 (by Proposition 3.4) this means exactly that $A^{\mathcal{C}}(x,y)$ is a set for all $x,y\colon O^{\mathcal{C}}$. What remains to be shown is that the (interpretations of) the axioms of $\mathbb{T}_{\text{cat}}$ correspond exactly to the axioms for precategories (but in relational form). This is straightforward and already established in [TsemHMT] as Proposition 7.1 and has even been formalized in [UniMath]. ∎

Lemma 4.11**.**

Let $\mathcal{C}$ be a precategory. For every $x,y,z\colon O^{\mathcal{C}}$, $\alpha\colon A^{\mathcal{C}}(z,x)\rightarrow A^{\mathcal{C}}(z,y)$ and $h\colon A^{\mathcal{C}}(z,x)$ we have

[TABLE]

Proof.

Since both types are propositions (since we assume that $\mathcal{C}$ is a precategory, and therefore identity in any hom-set will be a proposition) it suffices to show that they are logically equivalent.

For

[TABLE]

note that by the definition of Ind, $\text{Ind}^{\mathcal{C}}(h,\alpha(h))$ will contain the following proposition among the cartesian product that defines it:

[TABLE]

Since the RHS is trivially inhabited, the above type logically entails

[TABLE]

as required.

In the other direction, the only non trivial biconditional in $\text{Ind}^{\mathcal{C}}(h,\alpha(h))$ given the data will be

[TABLE]

But this follows immediately from

[TABLE]

as required. ∎

Lemma 4.12**.**

Let $\mathcal{C}$ be a precategory. For every $x,y\colon O^{\mathcal{C}}$ we have

[TABLE]

Proof.

By Lemma 3.5 we know that $A(z,x)\simeq^{\mathcal{C}}A(z,y)$ is equivalent to the type of bijections from $A^{\mathcal{C}}(z,x)$ to $A^{\mathcal{C}}(z,y)$. Since each $\mathcal{C}$ is a precategory, $A^{\mathcal{C}}(z,x)$ and $A^{\mathcal{C}}(z,y)$ are sets, and therefore bijections are equivalences, which means that $A(z,x)\simeq^{\mathcal{C}}A(z,y)$ is the type of (semantic) equivalences $A^{\mathcal{C}}(z,x)\simeq A^{\mathcal{C}}(z,y)$. Exactly the same reasoning applies to $A(x,z)\simeq^{\mathcal{C}}A(y,z)$, $A(x,x)\simeq^{\mathcal{C}}A(x,y)$, $A(x,x)\simeq^{\mathcal{C}}A(y,y)$ and $A(x,y)\simeq^{\mathcal{C}}A(y,y)$ which are the rest of the conjuncts of $x\cong y$ if we follow Definition 3.1. Thus, to prove the Lemma it suffices to show

[TABLE]

which follows from the elementary result in category theory that precomposition by an arrow induces a bijection on every hom-set iff postcomposition also does. ∎

Proposition 4.13**.**

The type $\textbf{\emph{SatMod}}_{\mathbb{T}_{\text{cat}}}$ of totally saturated models of the $\mathcal{L}_{\text{cat}}$-theory of categories is equivalent to the type UniCat of univalent categories.

Proof.

By Proposition 4.10 it suffices to show that for any precategory $\mathcal{C}$ and any $x,y\colon O^{\mathcal{C}}$ we have $\text{Iso}^{\mathcal{C}}(x,y)\simeq x\cong y$. To see this observe the following series of equivalences:

[TABLE]

∎

Corollary 4.14** ([HTT], Theorem 9.4.16).**

For any univalent categories $\mathcal{C}$ and $\mathcal{D}$, the type of categorical equivalences $\mathcal{C}\simeq_{\text{\emph{cat}}}\mathcal{D}$ is equivalent to $\mathcal{C}=_{\emph{{UniCat}}}\mathcal{D}$.

Proof.

By Theorem 4.9 what remains now is to show that in UniCat, the relation $\simeq_{\mathcal{L}_{\text{cat}}}$ is equivalent to categorical equivalence as defined in [HTT]. But this is immediate by inspection. ∎

Remark 4.15*.*

Propositions 4.10 and 4.13 in our opinion provide the correct taxonomy of category theory in the Univalent Foundations. In particular, we should regard precategories not as “unsaturated” categories but rather as the $2$-saturated $\mathbb{T}_{\text{cat}}$-models. This leaves two more “category theories” that currently have no name: the “totally unsaturated” models $\textbf{Mod}_{\mathbb{T}_{\text{cat}}}$ and the $1$-saturated models $\textbf{SatMod}_{\mathbb{T}_{\text{cat}}}^{1}$. There are thus four different category theories in the Univalent Foundations with respect to saturation as we have defined it. They can be thought of as follows, with the obvious inclusions:

[TABLE]

We believe this is the right point of view to take with respect to category theory (and other theories) in the Univalent Foundations.

Remark 4.16*.*

As the series of inclusions above suggests, clearly one can now ask to what extent we can have “Rezk completion”-type operations that reverse (in appropriate ways) the above inclusions. This is clearly an avenue worth pursuing further. In particular, the following question seems to us of immediate interest: Given an $\mathcal{L}$-theory $\mathbb{T}$, for which $n\geq\textrm{h}(\mathcal{L})$ can we construct an adjoint to the inclusion $\textbf{SatMod}_{\mathbb{T}_{\text{cat}}}^{n}\hookrightarrow\textbf{SatMod}_{\mathbb{T}_{\text{cat}}}^{n-1}$? Answers to this question seem to us unlikely to be pursued at least initially for any $\mathcal{L}$ with $\textrm{h}(\mathcal{L})>3$.

Finally, let us mention that in principle there is no obstacle to extending the proof of Theorem 4.9 to signatures $\mathcal{L}$ of arbitrarily large finite height. There are however two main difficulties. Firstly, finding a sufficiently practical way of packaging the syntax of such an $\mathcal{L}$ so as to define the relevant notions of $\mathcal{L}$-homomorphism, $\mathcal{L}$-equivalence etc. Secondly, proving the higher analogues of Lemma 4.8 which would require establishing equivalences between $n$-types of ever larger $n$. Solving these difficulties seems not entirely out of reach. Proving a version of Theorem 4.9 for all $n>1$ therefore seems to us an interesting open problem.

Acknowledgments

I thank Peter LeFanu Lumsdaine for the discussion that initiated this paper. This work was partially supported by NSF DMS-1554092 (P.I. Harry Crane).