# For Finitary Induction-Induction, Induction is Enough

Ambrus Kaposi, András Kovács, Ambroise Lafont

► To cite this version:

Ambrus Kaposi, András Kovács, Ambroise Lafont. For Finitary Induction-Induction, Induction is Enough. TYPES 2019: 25th International Conference on Types for Proofs and Programs, Jun 2019, Oslo, Norway. pp.6:1-6:30, 10.4230/LIPIcs.TYPES.2019.6 . hal-03594037

HAL Id: hal-03594037

https://imt-atlantique.hal.science/hal-03594037

Submitted on 2 Mar 2022

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# For Finitary Induction-Induction, Induction is Enough

Ambrus Kaposi

Eötvös Loránd University, Budapest, Hungary

akaposi@inf.elte.hu

András Kovács

Eötvös Loránd University, Budapest, Hungary

kovacsandras@inf.elte.hu

Ambroise Lafont

IMT Atlantique, Inria, LS2N CNRS, Nantes, France

ambroise.lafont@gmail.com

## Abstract

Inductive-inductive types (IITs) are a generalisation of inductive types in type theory. They allow the mutual definition of types with multiple sorts where later sorts can be indexed by previous ones. An example is the Chapman-style syntax of type theory with conversion relations for each sort where e.g. the sort of types is indexed by contexts. In this paper we show that if a model of extensional type theory (ETT) supports indexed W-types, then it supports finitely branching IITs. We use a small internal type theory called the theory of signatures to specify IITs. We show that if a model of ETT supports the syntax for the theory of signatures, then it supports all IITs. We construct this syntax from indexed W-types using preterms and typing relations and prove its initiality following Streicher. The construction of the syntax and its initiality proof were formalised in Agda.

2012 ACM Subject Classification Theory of computation → Logic

Keywords and phrases type theory, inductive types, inductive-inductive types

Digital Object Identifier 10.4230/LIPIcs.TYPES.2019.6

Funding Ambrus Kaposi: this author was supported by the National Research, Development and Innovation Fund of Hungary, financed under the Thematic Excellence Programme funding scheme, Project no. ED_18-1-2019-0030, by the New National Excellence Program of the Ministry for Innovation and Technology, Project no. ÚNKP-19-4-ELTE-874, and by the Bolyai Fellowship of the Hungarian Academy of Sciences, Project no. BO/00659/19/3.

András Kovács: this author was supported by the European Union, co-financed by the European Social Fund (EFOP-3.6.3-VEKOP-16-2017-00002).

Ambroise Lafont: this author was supported by the CoqHoTT ERC Grant 637339.

Acknowledgements The authors would like to thank Thorsten Altenkirch, Rafaël Bocquet, Simon Boulier, Fredrik Nordvall-Forsberg and Jakob von Raumer for discussions on the topics of this paper. We also thank the anonymous reviewers for their helpful comments and suggestions.

## 1 Introduction

Many mutual inductive types can be reduced to indexed inductive types, where the index disambiguates different sorts. For example, consider the mutual inductive datatype with two sorts `isEven` and `isOdd`, defined by the following constructors.

`isEven : N → Set`

`isOdd : N → Set`

`zeroEven : isEven zero`

<figure><img src="image_2.png" /></figure>

© Ambrus Kaposi, András Kovács and Ambroise Lafont; licensed under Creative Commons License CC-BY

25th International Conference on Types for Proofs and Programs (TYPES 2019).

Editors: Marc Bezem and Assia Mahboubi; Article No. 6; pp. 6:1–6:31

Leibniz International Proceedings in Informatics

<figure><img src="image_3.png" /></figure>

LIPICS Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
## 6:2 For Finitary Induction-Induction, Induction is Enough

$$43 \quad \text{sucEven} : (n : \mathbb{N}) \to \text{isOdd} n \to \text{isEven} (\text{suc } n)$$

$$44 \quad \text{sucOdd} : (n : \mathbb{N}) \to \text{isEven} n \to \text{isOdd} (\text{suc } n)$$

This can be reduced to the following single inductive family where `isEven? true` represents `isEven` and `isEven? false` represent `isOdd`.

$$48 \quad \text{isEven?} : \text{Bool} \to \mathbb{N} \to \text{Set}$$

$$49 \quad \text{zeroEven} : \text{isEven? true zero}$$

$$50 \quad \text{sucEven} : (n : \mathbb{N}) \to \text{isEven? false } n \to \text{isEven? true } (\text{suc } n)$$

$$51 \quad \text{sucOdd} : (n : \mathbb{N}) \to \text{isEven? true } n \to \text{isEven? false } (\text{suc } n)$$

Inductive-inductive types (IITs [26]) allow the mutual definition of a type and a family of types over the first one. IITs were originally introduced to represent the well-typed syntax of type theory itself, and a prominent example is still Chapman's [13] syntax for a type theory. A minimised version is the IIT of contexts and types given by the following constructors.

$$57 \quad \text{Con} : \text{Set}$$

$$58 \quad \text{Ty} : \text{Con} \to \text{Set}$$

$$59 \quad \text{empty} : \text{Con}$$

$$60 \quad \text{ext} : (\Gamma : \text{Con}) \to \text{Ty } \Gamma \to \text{Con}$$

$$61 \quad \text{U} : (\Gamma : \text{Con}) \to \text{Ty } \Gamma$$

$$62 \quad \text{El} : (\Gamma : \text{Con}) \to \text{Ty} (\text{ext } \Gamma (\text{U } \Gamma))$$

This type has two sorts, `Con` and `Ty`. The `ext` constructor of `Con` refers to `Ty` and the `Ty-constructor` `U` refers to `Con`, hence the two sorts have to be defined simultaneously. Moreover, `Ty` is indexed over `Con`. This precludes a reduction analogous to the reduction of `isEven-isOdd`, as we would get a type indexed over itself. Another unique feature of IITs (which also holds for higher inductive types [29]) is that later constructors can refer to previous constructors: in our case, `El` mentions `ext`.

The elimination principle for the above IIT has the following two motives (one for each sort) and four methods (one for each constructor).

$$72 \quad \text{Con}^D : \text{Con} \to \text{Set}$$

$$73 \quad \text{Ty}^D : \text{Con}^D \Gamma \to \text{Ty } \Gamma \to \text{Set}$$

$$74 \quad \text{empty}^D : \text{Con}^D \text{ empty}$$

$$75 \quad \text{ext}^D : (\Gamma^D : \text{Con}^D \Gamma) \to \text{Ty}^D \Gamma^D A \to \text{Con}^D (\text{ext } \Gamma A)$$

$$76 \quad \text{U}^D : (\Gamma^D : \text{Con}^D \Gamma) \to \text{Ty}^D \Gamma^D (\text{U } \Gamma)$$

$$77 \quad \text{El}^D : (\Gamma^D : \text{Con}^D \Gamma) \to \text{Ty}^D (\text{ext}^D \Gamma^D (\text{U}^D \Gamma^D)) (\text{El } \Gamma)$$

Above we used implicit quantifications for $\Gamma : \text{Con}$ and $A : \text{Ty } \Gamma$ to ease readability, e.g. $\text{Ty}^D$ has an implicit parameter $\Gamma$ before its explicit parameter of type $\text{Con}^D \Gamma$.

Given the above motives and methods the elimination principle provides two functions

$$82 \quad \text{elimCon} : (\Gamma : \text{Con}) \to \text{Con}^D \Gamma$$

$$83 \quad \text{elimTy} : (A : \text{Ty } \Gamma) \to \text{Ty}^D (\text{elimCon } \Gamma) A$$

with the following computation rules.

$$86 \quad \text{elimCon empty} = \text{empty}^D$$
$$ \text{elimCon}(\text{ext}\ \Gamma\ A) = \text{ext}^D(\text{elimCon}\ \Gamma)(\text{elimTy}\ A) $$

$$ \text{elimTy}(\mathbf{U}\ \Gamma) = \mathbf{U}^D(\text{elimCon}\ \Gamma) $$

$$ \text{elimTy}(\mathbf{El}\ \Gamma) = \mathbf{El}^D(\text{elimCon}\ \Gamma) $$

The functions elimCon and elimTy are an example of a recursive-recursive definition (using nomenclature from [26]). This means two mutually defined functions where the type of the second function depends on the first function. The proof assistant Agda [28] allows defining such functions (even from non-IITs) and is currently the only proof assistant supporting IITs<fnref n="1" />.

Reducing IITs to inductive types (more precisely, to indexed W-types) is an open problem. Forsberg [26] presented a reduction in extensional type theory, however, this only provides a simpler, non-recursive-recursive elimination principle. Hugunin [19] reduced several IITs to inductive types, working inside a cubical type theory, but he also only constructed the simple eliminator. To illustrate the difference, we list the motives, methods and the simple elimination principle for the Con-Ty example. Again, we use implicit quantifications.

$$ \text{Con}^S : \text{Con} \to \text{Set} $$

$$ \mathbf{Ty}^S : \mathbf{Ty}\ \Gamma \to \text{Set} $$

$$ \text{empty}^S : \text{Con}^S \text{ empty} $$

$$ \text{ext}^S : \text{Con}^S \Gamma \to \mathbf{Ty}^S A \to \text{Con}^S (\text{ext} \Gamma A) $$

$$ \mathbf{U}^S : \text{Con}^S \Gamma \to \mathbf{Ty}^S (\mathbf{U} \Gamma) $$

$$ \mathbf{El}^S : \text{Con}^S \Gamma \to \mathbf{Ty}^S (\mathbf{El} \Gamma) $$

$$ \text{selimCon} : (\Gamma : \text{Con}) \to \text{Con}^S \Gamma $$

$$ \text{selimTy} : (A : \mathbf{Ty} \Gamma) \to \mathbf{Ty}^S A $$

This simple elimination principle is not capable of defining standard (metacircular) interpretation [4] of our small syntax. Using pattern matching notation, this interpretation is the following:

$$ \llbracket - \rrbracket : \text{Con} \to \text{Set}_1 $$

$$ \llbracket - \rrbracket : \llbracket \Gamma \rrbracket \to \text{Set}_1 $$

$$ \llbracket \text{empty} \rrbracket := \top $$

$$ \llbracket \text{ext} \ \Gamma \ A \rrbracket := (\gamma : \llbracket \Gamma \rrbracket) \times \llbracket A \rrbracket \gamma $$

$$ \llbracket \mathbf{U} \ \Gamma \rrbracket \gamma := \text{Set} $$

$$ \llbracket \mathbf{El} \ \Gamma \rrbracket (\gamma, X) := X $$

The reason that we need the general elimination principle to define $\llbracket - \rrbracket$ is that $\llbracket - \rrbracket$ for types refers to $\llbracket - \rrbracket$ for contexts, hence this function is recursive-recursive.

Kaposi, Kovács, and Altenkirch [21] introduced a small type theory, called the theory of signatures, to describe quotient inductive-inductive types (QIIT). QIITs are generalisations of IITs where equality constructors are also allowed. A QIIT signature is a context in the theory of QIIT signatures, for example natural numbers are specified by the context $(\mathbf{Nat} : \mathbf{U}, \mathbf{zero} : \mathbf{Nat}, \mathbf{succ} : \mathbf{Nat} \to \mathbf{Nat})$ of length three $(\mathbf{Nat}, \mathbf{zero} \text{ and } \mathbf{succ} \text{ are variable names})$. The theory of QIIT signatures is itself a QIIT. In ibid., it is proved that if a model of extensional type theory supports the theory of QIIT signatures, then it supports all QIITs.

<footnote n="1">¹ An experimental version of Coq with IITs is also available on GitHub.</footnote>
## 6:4 For Finitary Induction-Induction, Induction is Enough

By omitting the equality type former from the theory of QIIT signatures, we obtain a theory of IIT signatures and the construction is still valid. It follows that if a model of extensional type theory supports the theory of IIT signatures, it supports all IITs.

In this paper we show that any model of extensional type theory with indexed W-types supports the theory of IIT signatures, and as a consequence all IITs. The difficulty in this construction is that the theory of IIT signatures is itself a QIIT, it is both inductive-inductive and has equality constructors. However, it can be seen as the well-typed syntax of a small type theory without any computation rules. Hence we can represent the syntax of normal forms without quotienting. We construct this well-typed normal syntax using preterms and typing relations from indexed W-types. Finally, we prove the elimination principle in the style of the initiality proof of Streicher.

Streicher [30] constructs the syntactic model of type theory using well-typed preterms and then shows initiality of this model by (1) defining a partial map to any other model by induction on preterms and (2) showing that whenever this partial function receives a well-typed preterm on its input it actually gives an output. Instead of defining a partial function, we define the graph of the same function as a relation and then show that it is functional as a second step. This can be seen as an indexed variant of the construction using partial functions.

Just as [21], we only consider finitary IITs, that is, constructors can only have a finite number of recursive arguments. An example constructor for Con-Ty which is not allowed is the following:

$$ \Pi_{\infty} : (\Gamma : \mathrm{Con}) \to (\mathbb{N} \to \mathrm{Ty} \Gamma) \to \mathrm{Ty} \Gamma $$

## Structure of paper and list of contributions

We describe related work in Section 1.1, and explain our notation and Agda formalisaton in Section 1.2. Then the following three sections describe our three contributions:

- Section 2. We define what it means for a model of extensional type theory (ETT, Definition 1) to support all inductive-inductive types (IITs): Definition 12. The novel contribution here is a (predicative) Church encoding of signatures following [8].

- Section 3. In Theorem 23, we show that if a model of ETT supports the theory of IIT signatures (Definition 15), then it supports IITs. This is an adaptation of a proof in [21].

- Section 4. Our main contribution is showing that if a model of ETT supports indexed W-types, then it supports the theory of IIT signatures (Theorem 57), and hence, all IITs (Corollary 58).

We list further work in Section 5.

The contents of this paper were presented at the TYPES 2019 conference in Oslo [22].

## 1.1 Related Work

The current work builds heavily on the work of Kaposi et al. [21] on finitary quotient inductive-inductive types (QIITs); we reuse both QIIT syntax and semantics by restricting to IITs, and we reuse the term model construction of QIITs as well. We also make use of the extension to infinitary QIITs [24] to derive the specification of the elimination principle for the theory of IIT signatures.

IITs (although not by this name) were first used to describe the well-typed syntax of type theory [15, 13]. Agda supported these general inductive definitions even before they were named IITs and given semantics by Nordvall Forsberg and Setzer [27]. Nordvall Forsberg's
thesis [26] contains a specification similar in style to Dybjer and Setzer's codes for inductive-
recursive types [17]. He also develops a categorical semantics based on dialgebras and provides
a reduction of IITs to indexed inductive types, however only constructs the simple elimination
principle as opposed to the general one. Altenkirch et al. [2] define signatures for QIITs
(thus IITs as well) and their categorical semantics, however without proving existence of
initial algebras. Their notion of signature, like Nordvall Forsberg's, involves more encoding
overhead than ours.

Cartmell [12] introduced generalised algebraic theories using a type-theoretic syntax.
Removing equations from his signatures and only considering finite signatures, we obtain
finitary IIT signatures similar to ours. He does not consider constructing initial algebras
using simpler classes of inductive types.

Hugunin [19] constructs several IITs in cubical Agda from inductive types. In this setting, the lack of UIP makes constructions significantly more involved, and essentially involves coinductive-coinductive well-formedness predicates defined as homotopy limits. Hugunin does not consider a generic syntax of IITs and only works on specific examples (although the examples vary greatly). He also only constructs simple elimination principles.

Streicher [30] presents an interpretation of the well-formed presyntax of a type theory
into a categorical model, which is an important ingredient in constructing an initial model,
although he does not present details on the construction of the term model or its initiality
proof. Our initiality proof can be seen as an indexed variant of his construction (see Subsection
4.2 for a comparison).

Voevodsky was interested in constructing initial models of type theories from presyntaxes.
Inspired by this, Brunerie et al. [10] formalised Streicher's proof in Agda for a type theory
with Π, Σ, N, identity types and an infinite hierarchy of universes. They used UIP, function
extensionality and quotient types in the formalisation. In this paper we construct a type
theory without computation rules, hence we avoid using quotients.

Intrinsic (well-typed) syntaxes for type theories were constructed using IITs [13], inductive-
recursive types [15, 6] and QIITs [4]. In this paper we avoid using such general classes of
inductive types as our goal is to reduce IITs to indexed inductive types.

Reducing general classes of inductive types to simpler classes has a long tradition in type
theory. Indexed W-types were reduced to W-types [3] (using the essentially Streicher's idea
of preterms and a typing predicate), small inductive-recursive types to indexed W-types [25],
mutual inductive types to indexed W-types [23], W-types to natural numbers and quotients
[1]. (Q)IITs can be reduced to quotient inductive types using the reduction of generalised
algebraic theories to essentially algebraic theories [12]. Using the same reduction as mutual
inductive types to indexed inductive types, (Q)IITs with more than two sorts can be reduced
to (Q)IITs with only two sorts [20].

Awodey, Frey and Speight [8] construct inductive types using a restricted Church encoding
in a type theory with an impredicative universe. We use the predicative version of their
encoding to define IIT signatures.

Our reduction of IITs to indexed inductive types goes through two steps: first we construct
a concrete QIIT using inductive types, then we construct all IITs from this particular QIIT.
A more direct approach is proposed by [5]: here the initial algebra would be constructed
directly for any IIT signature without going through an intermediate step.

1.2 Notation and Formalisation

► **Definition 1** (Model of extensional type theory (ETT)). By a model of ETT we mean a category with families (CwF) [16, 18] with a countable predicative hierarchy of universes
6:6 For Finitary Induction-Induction, Induction is Enough

closed under the following type formers: Π, Σ, ⊤ and an identity type with uniqueness of
identity proofs and equality reflection.

We will use Agda-like type theoretic syntax to work in the internal language of models of
ETT:

Universes are written Set$_i$. We usually omit level indices in this paper.

Π types are notated as (x : A) → B, or as A → B when non-dependent. We sometimes
omit function arguments, by implicitly generalising over variables.

Σ-types, notated either as (x : A) × B, or as $\sum_x B$ when we want to leave the type of the
first projection implicit. Projections are either named or given by $\text{proj}_1$ and $\text{proj}_2$. We
use $A \times B$ for non-dependent pairs.

The unit type $\top$ has the constructor tt which is definitionally equal to all elements of $\top$.

The equality (identity) type is written $t = u$, it has a constructor `refl`: $t = t$, and equality reflection, hence we use the same `=` sign for definitional equality. We occasionally indicate by $e_1, \dots, e_n \# t$ that $t$ is well-typed thanks to the equalities $e_1, \dots, e_n$. To construct proofs, sometimes we write equational reasoning, e.g. $fa \stackrel{e}{=} fb$ where $e : a = b$. We also have uniqueness of identity proofs (UIP), expressing $(e : t = t) \rightarrow e = \text{refl}$. Note that function extensionality, expressing $((x : A) \rightarrow f x = g x) \rightarrow f = g$ is derivable.

The contents of Section 4 were formalised in Agda, the formalisation is available at
https://github.com/amblafont/UniversalII. Agda's pattern matching mechanism im-
plies uniqueness of identity proofs, we assumed function extensionality as an axiom and used
rewrite rules [14] to obtain limited equality reflection.

2 A Definition of Inductive-Inductive Types

In this section we specify what it means that a model of ETT supports IITs. We first define the notion of IIT signature. Signatures for algebraic theories are usually given by inductive definitions. On the one hand, we take this even further: our notion of signature is given by a small type theory tailor-made to describe signatures, which we call the *theory of IIT signatures*. On the other hand we would like to avoid using a complicated inductive definition (a type theory is a quotient inductive-inductive type [4]) to describe a simpler class of inductive types. Hence we use a Church encoding [8] of the theory of IIT signatures, thereby avoiding the need for pre-existing inductive definitions. Another feature of our signatures is that they can include types from the model of ETT (such as $\mathbb{N}$ in the `isEven-isOdd`). This is why signatures are specified internally to the particular model of ETT.<fnref n="2" />

We define the theory of IIT signatures by saying what its algebras (models) are. We call
the *theory of IIT signatures algebras* simply *signature algebras*. The theory of signatures is a
small type theory consisting of a (1) a substitution calculus (category with families, CwF
[16]) equipped with (2) a universe, (3) a function space where the domain is in the universe
and (4) another function space with external domain. We explain the usage of these type
formers through examples after the definition.

<footnote n="2">² There is another method inspired by Capriotti [11] which allows stating what it means that any CwF $\mathcal{C}$ (not necessarily a model of ETT) supports IITs with definitional computation rules. In this method, signatures are described in the internal language of $\hat{\mathcal{C}}$, the presheaf model over $\mathcal{C}$. We do not use this approach because it is more technical, and it would not strengthen our main result Corollary 58 as the proof of Theorem 57 needs $\mathcal{C}$ to be a model of ETT.</footnote>
**► Definition 2** (Signature algebra, SignAlg). In a model of ETT, a signature algebra is an iterated Σ type consisting of the following four (families of) sets, 17 operations and 18 equalities.

(1) *Substitution calculus*

Con : Set

Ty : Con → Set

Sub : Con → Con → Set

Tm : (Γ : Con) → Ty Γ → Set

id : Sub Γ Γ

- - : Sub Θ Δ → Sub Γ Θ → Sub Γ Δ

ass : (σ ◦ δ) ◦ ν = σ ◦ (δ ◦ ν)

idl : id ◦ σ = σ

idr : σ ◦ id = σ

-[–] : Ty Δ → Sub Γ Δ → Ty Γ

-[–] : Tm Δ A → (σ : Sub Γ Δ) → Tm Γ (A[σ])

[id] : A[id] = A

[◦] : A[σ ◦ δ] = A[σ][δ]

[id] : t[id] = t

[◦] : t[σ ◦ δ] = t[σ][δ]

• : Con

ε : Sub Γ ·

·η : (σ : Sub Γ ·) → σ = ε

-▷- : (Γ : Con) → Ty Γ → Con

- , - : (σ : Sub Γ Δ) → Tm Γ (A[σ]) → Sub Γ (Δ▷A)

π₁ : Sub Γ (Δ▷A) → Sub Γ Δ

π₂ : (σ : Sub Γ (Δ▷A)) → Tm Γ (A[π₁σ])

π₁β : π₁(σ, t) = σ

π₂β : π₂(σ, t) = t

πη : (π₁ σ, π₂ σ) = σ

, ◦ : (σ, t) ◦ δ = (σ ◦ δ, t[δ])

(2) *Universe*

U : Ty Γ

El : Tm Γ U → Ty Γ

U[] : U[σ] = U

El[] : (El a)[σ] = El (a[σ])

(3) *Inductive parameters*

Π : (a : Tm Γ U) → Ty (Γ▷El a) → Ty Γ

- @ - : Tm Γ (Π a B) → (u : Tm Γ (El a)) → Tm Γ (El (B[id, u]))

Π[] : (Π a B)[σ] = Π (a[σ]) (B[σ ◦ p, q])

@[] : (t @ α)[σ] = (t[σ]) @ (α[σ])
6:8 For Finitary Induction-Induction, Induction is Enough

(4) External parameters

299

$$
\hat{\Pi} : (T : \mathit{Set}) \to (T \to \mathit{Ty} \Gamma) \to \mathit{Ty} \Gamma
$$

300

$$
- \hat{a} - : \mathrm{Tm} \Gamma (\hat{\Pi} T B) \to (\alpha : T) \to \mathrm{Tm} \Gamma (B \alpha)
$$

301

$$
\hat{\Pi}[] : (\hat{\Pi} T B)[\sigma] = \hat{\Pi} T (\lambda\alpha.(B\alpha)[\sigma])
$$

302

$$
\hat{a}[] : (t \hat{a} \alpha)[\sigma] = (t[\sigma]) \hat{a} \alpha
$$

303

304

Given an $M: \text{SignAlg}$, we denote its components by $\text{Con}^M$, $\text{Ty}^M$, $\text{Sub}^M$, $\text{Tm}^M$, $\text{id}^M$, and so on. We omit the indices if there is only one signature algebra in scope (e.g. in Definition 3 and Example 4).

305

306

307

► **Definition 3 (Abbreviations).** For a signature algebra, we use wk : Sub (Γ ⊲ A) Γ to mean π₁ id. We recover de Bruijn indices by setting 0 := π₂ id and 1 + n := n[wk]. Π a (B[wk]) is abbreviated by a ⇒ B, Π T (λ_=.B) by T ⇒ B.

308

309

310

► **Example 4 (Example contexts in a signature algebra).** Given a signature algebra, we can define a context which specifies natural numbers. For readability, an informal version of the same context is displayed on the right using variable names.

311

312

313

$$
\bullet \triangleright U \triangleright z : E|0 \triangleright s : 1 \Rightarrow E|1
$$

314

$$
\bullet \triangleright N : U \triangleright z : E|N \triangleright s : N \Rightarrow E|N
$$

315

316

317

318

319

320

We start with the empty context •, then we declare a sort U, then we declare an operator producing an element of the sort denoted by E|0 where 0 is the de Bruijn index referring to the sort. Finally, we declare an operator which takes as input an element of the sort (now it became de Bruijn index 1) and produces an element of the same sort. Note the asymmetry of the function type ⇒: the domain needs to be an element of U, while the codomain can be any type (including another function type). This ensures strict positivity of the operators.

321

322

323

324

Lists with elements of a given $T : \mathit{Set}$ type are given by the following context. Here we use the function space with external domain $\Rightarrow$ to include a $T$ in the signature. For readability, we omit the $\lambda$ and the superscripts and we do not write the compatibility condition. On the right we list the same signature with variable names.

$$
\bullet \triangleright U \triangleright E|0 \triangleright T \Rightarrow 1 \Rightarrow E|1
$$

325

$$
\bullet \triangleright L : U \triangleright \mathit{nil} : E|L \triangleright \mathit{cons} : T \Rightarrow L \Rightarrow E|L
$$

327

The Con-Ty example from Section 1 is given by the following context.

328

• ▷

329

U ▷

Con : U ▷

330

0 ⇒ U ▷

Ty : Con ⇒ U ▷

331

E|1 ▷

empty : E|Con ▷

332

Π 2 (2 @ 0 ⇒ E|3)▷

ext : Π (Γ : Con) (Ty @ Γ ⇒ E|Con)▷

333

Π 3 (E| (3 @ 0))▷

U : Π (Γ : Con) (E| (Ty @ Γ))▷

334

Π 4 (E| (4 @ (2 @ 0 @ (1 @ 0))))

El : Π (Γ : Con) (E| (Ty @ (ext @ Γ @ (U @ Γ))))

335

The above examples are contexts in any signature algebra, and we could take this as a definition of signature: (M : SignAlg) → Con<sup>M</sup> is the usual Church-encoding of contexts. However (as we will see in Remark 24) the notion of constructor for such signatures would be too strong. Another approach would be to assume that there is a syntax for signature algebras (an initial signature algebra), and then a signature would be a context in this signature algebra. We will define syntactic signatures using this approach in the next section

336

337

338

339

340

341
(Definition 16), but for now we do not want to assume the existence of any inductive type. Instead, we will use a restricted Church encoding. This requires the notion of morphism of signatures.

The notion of morphism is determined by the notion of algebra [24], but we include it here for completeness.

**► Definition 5 (Signature morphism, SignMor).** A morphism from signature algebras M to N denoted SignMor M N consists of four functions and 17 equalities expressing that the functions preserve the operations of the two algebras. We use the same naming as in Definition 2 and use superscripts to denote which algebra is meant.

(1) *Substitution calculus*

Con : Con<sup>M</sup> &rarr; Con<sup>N</sup>

Ty : Ty<sup>M</sup> &Gamma; &rarr; Ty<sup>N</sup> (Con &Gamma;)

Sub : Sub<sup>M</sup> &Gamma; &Delta; &rarr; Sub<sup>N</sup> (Con &Gamma;) (Con &Delta;)

Tm : Tm<sup>M</sup> &Gamma; A &rarr; Tm<sup>N</sup> (Con &Gamma;) (Ty A)

id : Sub id<sup>M</sup> = id<sup>N</sup>

o : &sigma; &circ;<sup>M</sup> &delta; = Sub &sigma; &circ;<sup>N</sup> Sub &delta;

[] : A[&sigma;]<sup>M</sup> = Ty A[Sub &sigma;]<sup>N</sup>

[] : t[&sigma;]<sup>M</sup> = Tm t[Sub &sigma;]<sup>N</sup>

· : Con·<sup>M</sup> = ·<sup>N</sup>

epsilon : Sub &epsilon;<sup>M</sup> = &epsilon;<sup>N</sup>

▷ : Con(&Gamma;▷<sup>M</sup> A) = Con &Gamma;▷<sup>N</sup> Ty A

, : Sub(&sigma;,<sup>M</sup> t) = Sub &sigma;,<sup>N</sup> Tm t

pi<sub>1</sub> : Sub(&pi;<sub>1</sub><sup>M</sup> &sigma;) = &pi;<sub>1</sub><sup>N</sup> (Sub &sigma;)

pi<sub>2</sub> : Tm(&pi;<sub>2</sub><sup>M</sup> &sigma;) = &pi;<sub>2</sub><sup>N</sup> (Sub &sigma;)

(2) *Universe*

U : Ty U<sup>M</sup> = U<sup>N</sup>

El : Ty (El<sup>M</sup> a) = El<sup>N</sup> (Tm a)

(3) *Inductive parameters*

Π : Ty (Π<sup>M</sup> a B) = Π<sup>N</sup> (Tm a) (Ty B)

@ : Tm (t @<sup>M</sup> u) = Tm t @<sup>N</sup> Tm u

(4) *External parameters*

Î : Ty (Î<sup>M</sup> T B) = Î<sup>N</sup> T (&lambda;&alpha; . Ty (B &alpha;))

@ : Tm (t @<sup>M</sup> &alpha;) = Tm t @<sup>N</sup> &alpha;

Given an $f : \text{SignMor } M N$, we denote its first four components just by $f_{\text{Con}}$, $f_{\text{Ty}}$, $f_{\text{Sub}}$, $f_{\text{Tm}}$ or just write $f$ if it is clear which one is meant.

We define IIT signatures using the Church encoding introduced by Awodey, Frey and Speight [8]. A difference is that we avoid impredicativity. This restricts the possible eliminations on signatures: we can only eliminate into a universe which is smaller than the level of signatures. However, this still covers all eliminations in this paper, and it is also not an issue for us that signatures do not live in the smallest universe.
6:10 For Finitary Induction-Induction, Induction is Enough

383 ▶ Definition 6 (IIT signature). An IIT signature is a context in an arbitrary signature algebra,
384 which is also compatible with morphisms:

$$
\begin{equation*}
\begin{split}
\text{Sign} &:= (\mathit{sig} : (M : \mathit{SignAlg}) \to \mathit{Con}^M) \times \\
&\qquad ((MN : \mathit{SignAlg})(f : \mathit{SignMor} MN) \to f_{\mathit{Con}}(\mathit{sig} M) = \mathit{sig} N).
\end{split}
\end{equation*}
$$

388 The compatibility condition says that if we obtain an *M*-context using *sig* at signature
389 algebra *M* and then we transport it to *N* using *f*, we get the same *N*-context as directly
390 applying *sig* to *N*.

391 The lack of impredicativity implies that our notion of signatures do not form a signature
392 algebra.

393 ▶ Lemma 7. There is no M : SignAlg, in which Con<sup>M</sup> = Sign.

394 ▶ Proof. If the Con component in SignAlg is Set<sub>i</sub>, then SignAlg is in Set<sub>i+1</sub>, but as Sign is
395 defined as (SignAlg &rarr; ...) &times; ..., it is at least in Set<sub>i+1</sub>, so we can't choose Con<sup>M</sup> : Set<sub>i</sub> to
396 be Sign : Set<sub>i+1</sub>. &black;
400

397 Note that the notion of IIT signature is relative to a model of ETT: it is expressed as a
term (of a function type) in the model. This is necessary because of the function space $\hat{\Pi}$,
398 which has as domain an arbitrary type in the model. We make use of $\hat{\Pi}$ in signatures with
399 external parameters, like the type of the elements in lists.
400

401 ▶ Example 8 (Example signature) . Now we can formally describe the contexts given in
402 Example 4 as signatures. For natural numbers, we have the following pair of functions. The
403 second function returns an equality proof which we describe using equational reasoning.

$$
\begin{equation*}
\begin{split}
(nat, natc) &:= \\
            & \quad (\lambda M . (\cdot^M \triangleright^M U^M \triangleright^M E^I^M 0^M \triangleright^M 1^M \Rightarrow^M E^I^M 1^M), \\
            & \quad \lambda M N f . f_{\text{Con}} (\cdot^M \triangleright^M U^M \triangleright^M E^I^M 0^M \triangleright^M 1^M \Rightarrow^M E^I^M 1^M) = \\
            & \quad f_{\text{Con}} (\cdot^M \triangleright^M U^M \triangleright^M E^I^M 0^M) \triangleright^N f_{\text{Ty}} (1^N \Rightarrow^N E^I^N 1^N) = \\
            & \quad f_{\text{Con}} (\cdot^M \triangleright^M U^M) \triangleright^N f_{\text{Ty}} (E^I^M 0^M) \triangleright^N f_{\text{Tm}} 1^N \Rightarrow^M f_{\text{Ty}} (E^I^N 1^N) = \\
            & \quad f_{\text{Con}} \cdot^M \triangleright^N f_{\text{Ty}} U^M \triangleright^N E^I^N (f_{\text{Tm}} 0^M) \triangleright^N 1^M \Rightarrow^M E^I^M (f_{\text{Tm}} 1^N) = \\
            & \quad \cdot^N \triangleright^N U^N \triangleright^N E^I^N 0^N \triangleright^N 1^N \Rightarrow^N E^I^N 1^N)
\end{split}
\end{equation*}
$$

412 The first component builds the context describing natural numbers in *M*, the second one
413 uses the fact that *f* is a morphism, that is, it preserves all operations.

414 The signatures for lists and Con-Ty can be given analogously.

415 Given a model of ETT and an IIT signature in it, we would like to say what it means
416 that the model supports the given IIT. For this we define the signature algebra ADS which
417 will provide notions of algebras, displayed algebras and sections for each signature. This is
418 the same as the $-^A$, $-^D$ and $-^S$ operations in [21]. Before defining ADS, we illustrate its
419 usage by an example.

420 ▶ Example 9 (Algebras, displayed algebras and sections for natural numbers) . For the signature
421 of natural numbers as given in Example 8, algebras are given by the Σ-type ( N : Set ) × N ×
422 ( N → N ) . A displayed algebra over ( N, z, s ) is given by the Σ-type

$$
423 (N^D : N \to \mathbf{Set}) \times N^D z \times ((n : N) \to N^D n \to N^D (sn)),
$$
and a section of a displayed algebra ($N^D$, $z^D$, $s^D$) over $(N, z, s)$ is given by the $\Sigma$-type

$$ (N^S : (n : N) \to N^D n) \times (N^S z = z^D) \times ((n : N) \to N^S (sn) = s^D n (N^S n)). $$

Displayed algebras over the initial algebra are called motives and methods of the eliminator, while a section of a displayed algebra over the initial algebra is the eliminator together with its computation rules.

**► Definition 10 (The signature algebra ADS).** We define an element of SignAlg by listing all its components Con, Ty, Sub, and so on, one per row. Each such component has three parts denoted by $^A$, $^D$ and $^S$, respectively. The equality components of SignAlg are omitted as they are all *reflexivity*.

$$ (\Gamma^A : \text{Set}) \quad \times (\Gamma^D : \Gamma^A \to \text{Set}) \quad \times (\Gamma^S : (\gamma : \Gamma^A) \to \Gamma^D \gamma \to \text{Set}) $$

$$ (A^A : \Gamma^A \to \text{Set}) \quad \times (A^D : \Gamma^D \gamma \to A^A \gamma \to \text{Set}) \quad \times (A^S : \Gamma^S \gamma \gamma^D \to (\alpha : A^A \gamma) \to A^D \gamma^D \alpha \to \text{Set}) $$

$$ (\sigma^A : \Gamma^A \to \Delta^A) \quad \times (\sigma^D : \Gamma^D \gamma \to \Delta^D (\sigma^A \gamma)) \quad \times (\sigma^S : \Gamma^S \gamma \gamma^D \to \Delta^S (\sigma^A \gamma) (\sigma^D \gamma^D)) $$

$$ (t^A : (\gamma : \Gamma^A) \to A^A \gamma) \quad \times (t^D : (\gamma^D : \Gamma^D \gamma) \to A^D \gamma^D (t^A \gamma)) \quad \times (t^S : (\gamma^S : \Gamma^S \gamma \gamma^D) \to A^S (t^A \gamma) (t^D \gamma^D)) $$

$$ \text{id}^A \gamma := \gamma \qquad \text{id}^D \gamma^D := \gamma^D \qquad \text{id}^S \gamma^S := \gamma^S $$

$$ (\sigma \circ \delta)^A \gamma := \sigma^A (\delta^A \gamma) \qquad (\sigma \circ \delta)^D \gamma^D := \sigma^D (\delta^D \gamma^D) \qquad (\sigma \circ \delta)^S \gamma^S := \sigma^S (\delta^S \gamma^S) $$

$$ (A[\sigma])^A \gamma := A^A (\sigma^A \gamma) \qquad (A[\sigma])^D \gamma^D := A^D (\sigma^D \gamma^D) \qquad (A[\sigma])^S \gamma^S := A^S (\sigma^S \gamma^S) $$

$$ (t[\sigma])^A \gamma := t^A (\sigma^A \gamma) \qquad (t[\sigma])^D \gamma^D := t^D (\sigma^D \gamma^D) \qquad (t[\sigma])^S \gamma^S := t^S (\sigma^S \gamma^S) $$

$$ \begin{array}{l} \cdot^A := \top \\ \cdot^D := \top \\ \cdot^S := \top \end{array} $$

$$ \epsilon^A := \text{tt} \qquad \epsilon^D := \text{tt} \qquad \epsilon^S := \text{tt} $$

$$ (\Gamma \triangleright A)^A := (\Gamma \triangleright A)^D (\gamma, \alpha) := (\Gamma \triangleright A)^S (\gamma, \alpha) (\gamma^D, \alpha^D) := (\gamma^S : \Gamma^S \gamma \gamma^D) \times A^S \gamma^S \alpha \alpha^D $$

$$ (\sigma, t)^A \gamma := (\sigma^A \gamma, t^A \gamma) \qquad (\sigma, t)^D \gamma^D := (\sigma^D \gamma^D, t^D \gamma^D) \qquad (\sigma, t)^S \gamma^S := (\sigma^S \gamma^S, t^S \gamma^S) $$

$$ (\pi_1 \sigma)^A \gamma := \text{proj}_1 (\sigma^A \gamma) \qquad (\pi_1 \sigma)^D \gamma^D := \text{proj}_1 (\sigma^D \gamma^D) \qquad (\pi_1 \sigma)^S \gamma^S := \text{proj}_1 (\sigma^S \gamma^S) $$

$$ (\pi_2 \sigma)^A \gamma := \text{proj}_2 (\sigma^A \gamma) \qquad (\pi_2 \sigma)^D \gamma^D := \text{proj}_2 (\sigma^D \gamma^D) \qquad (\pi_2 \sigma)^S \gamma^S := \text{proj}_2 (\sigma^S \gamma^S) $$

$$ U^A \gamma := \text{Set} \qquad U^D \gamma^D T := T \to \text{Set} \qquad U^S \gamma^S T T^D := (\alpha : T) \to T^D \alpha $$

$$ (\text{El} a)^A \gamma := a^A \gamma \qquad (\text{El} a)^D \gamma^D := a^D \gamma^D \alpha \qquad (\text{El} a)^S \gamma^S \alpha \alpha^D := (a^S \gamma^S \alpha = \alpha^D) $$

$$ (\Pi a B)^A \gamma := (\Pi a B)^D \gamma^D f := (\alpha : a^A \gamma) \to B^A (\gamma, \alpha) \qquad (\alpha : a^A \gamma) \to B^A (\gamma, \alpha) \to B^D (\gamma^D, \alpha^D) (f \alpha) \qquad (f^D (a^S \gamma^S \alpha)) $$

$$ (t \@ u)^A \gamma := t^A \gamma (u^A \gamma) \qquad (t \@ u)^D \gamma^D := t^D \gamma^D (u^D \gamma^D) \qquad (t \@ u)^S \gamma^S := \text{refl}_{a^S \gamma^S \alpha} (f \alpha) $$

$$ (\hat{\Pi} T B)^A \gamma := (\hat{\Pi} T B)^D \gamma^D f := (\alpha : T) \to (B \alpha)^A \gamma \qquad (\alpha : T) \to (B \alpha)^D \gamma^D (f \alpha) \qquad (B \alpha)^S \gamma^S (f \alpha) (f^D \alpha) $$

$$ (t \hat{\@} \alpha)^A \gamma := t^A \gamma \alpha \qquad (t \hat{\@} \alpha)^D \gamma^D := t^D \gamma^D \alpha \qquad (t \hat{\@} \alpha)^S \gamma^S := t^S \gamma^S \alpha $$

Definition 10 can be explained by columns (see [21, Sections 4 and 6] for more details) or by rows (see [21, Section 7.4]).

We first explain it by columns: the first column ($^A$ components) corresponds to the standard model (set model, metacircular interpretation [4]): contexts are sets, types are
6:12 For Finitary Induction-Induction, Induction is Enough

families, terms are functions, the universe U is given by Set, function spaces are given by the external function space. The D column is a logical predicate interpretation, A and D together are a unary version of the parametric model for dependent types [7]. Contexts are predicates, types are families of predicates, terms say that the A interpretation respects the predicates (this is usually called fundamental lemma of the logical predicate). U is given by predicate space, the predicate at a Π type holds for a function if it respects the predicates. For Π̂, the predicate is defined pointwise. The last column S is a modified dependent logical relation which refers to both A and D. Contexts are binary relations where the second parameter depends on the first one, types are dependent variants of this, terms say that the relation is respected by A and D, respectively. U is however not relation space, but a function and (El a)S is the graph of the function aS. ΠS for a function again says that the function respects the relation, however we do not simply say

$$ (\Pi a B)^S \gamma^S f f^D := (\alpha : a^A \gamma)(\alpha^D : a^D \gamma^D \alpha)(\alpha^S : (El a)^S \gamma^S \alpha^D) \to B^S \dots, $$

as (El a)S γS α αD is just an equality aS γS α = αD which we can singleton contract. So we omit αD and this equality as an input and replace αD by aS γS α in the definition.

When viewing ADS by rows, we can see that it is a part of the CwF model of type theory [21, Section 7.4]. In the CwF model, a context is given by a CwF. Now, from the category part of the CwF, we only have objects (ΓA), and from the families, we have the families for types ΓD and terms ΓS. Types are the corresponding parts of displayed CwFs, substitutions are parts of CwF morphisms, terms are parts of CwF sections. U is part of the CwF of sets, El a is the part of the discrete displayed CwF coming from a (which is a CwF-morphism from Γ to the CwF of sets). Π is given by a dependent product of displayed CwFs where it is essential that the domain is discrete, Π̂ is the pointwise direct product.

► **Definition 11 (The set signature algebra A).** A : SignAlg is given by the first A components of ADS (Definition 10), that is, ConA := Set, TyA Γ := Γ → Set, SubA Γ Δ := Γ → Δ, and so on. There is a morphism from ADS to A defined by -A at each component, which we also denote by -A : SignMor ADS A.

► **Definition 12 (A model of ETT supports IITs).** A model of ETT supports IITs if for any signature (sig, sigc) : Sign there is a

$$ \text{con}_{\text{sig}} : (\text{sig ADS})^A $$

and an

$$ \text{elim}_{\text{sig}} : (\gamma^D : (\text{sig ADS})^D \text{con}_{\text{sig}}) \to (\text{sig ADS})^S \text{con}_{\text{sig}} \gamma^D. $$

In other words, for any signature, we have an algebra called con (constructors) and for any displayed algebra over the constructors, we have a section (called the eliminator).

One can check that Definition 12 gives the right notion of constructors and elimination principle for the signatures in Example 8.

► **Example 13 (A model of ETT supports natural numbers).** For the signature (nat, natc) of natural numbers in Example 8, the type of connat is

$$ \begin{align*} (\text{nat ADS})^A &= \\ (\text{ADS} \triangleleft \text{ADS} \ U\text{ADS} \triangleleft \text{ADS} \ El\text{ADS} \ 0\text{ADS} \triangleleft \text{ADS} \ 1\text{ADS} \Rightarrow \text{ADS} \ El\text{ADS} \ 1\text{ADS})^A &= \\ (((\cdot \triangleleft U) \triangleleft El(\pi_2 \text{id})) \triangleleft (\pi_2(\pi_1 \text{id})) \Rightarrow El(\pi_2(\pi_1 \text{id})))^A &= \end{align*} $$
$$ 
\begin{align*}
& (\gamma'' : (\gamma' : ((\gamma : \cdot^A) \times \mathbf{U}^A \gamma)) \times (\mathrm{El}(\pi_2 \mathrm{id}))^A \gamma') \times (\Pi (\pi_2 (\pi_1 \mathrm{id})) (\pi_2 (\pi_1 (\pi_1 \mathrm{id})))^A \gamma'' = \\
& \qquad (\gamma'' : (\gamma' : ((\gamma : \top) \times \mathrm{Set})) \times (\mathrm{proj}_2 \gamma')) \times (\mathrm{proj}_2 (\mathrm{proj}_1 \gamma'') \to \mathrm{proj}_2 (\mathrm{proj}_1 \gamma''))
\end{align*}
$$

506

507

508

509

which is a left-nested Σ type isomorphic to its right-nested counterpart

$$ (N : \mathrm{Set}) \times (N \times (N \to N)). $$

510

511

Writing (((tt, Nat), zero), suc) for con<sub>nat</sub>, the type of elim<sub>nat</sub> computes as follows.

$$ 
\begin{align*}
(\gamma^D : (\mathit{nat\ ADS})^D \mathit{con}_{\mathit{nat}}) \to (\mathit{nat\ ADS})^S \mathit{con}_{\mathit{nat}} \gamma^D &= \\
& \quad (\gamma^D : (((\cdot \triangleright U) \triangleright \mathrm{El}(\pi_2 \mathrm{id})) \triangleright (\pi_2(\pi_1 \mathrm{id})) \Rightarrow \mathrm{El}(\pi_2(\pi_1 \mathrm{id})))^D \mathit{con}_{\mathit{nat}}) \to \\
& \quad (((\cdot \triangleright U) \triangleright \mathrm{El}(\pi_2 \mathrm{id})) \triangleright (\pi_2(\pi_1 \mathrm{id})) \Rightarrow \mathrm{El}(\pi_2(\pi_1 \mathrm{id})))^S \mathit{con}_{\mathit{nat}} \gamma^D = \\
& \quad (\gamma^D : (((\cdot \triangleright U) \triangleright \mathrm{El}(\pi_2 \mathrm{id})) \triangleright (\pi_2(\pi_1 \mathrm{id})) \Rightarrow \mathrm{El}(\pi_2(\pi_1 \mathrm{id})))^D \\
& \qquad (((\mathit{tt}, \mathit{Nat}), \mathit{zero}), \mathit{suc}) \to \\
& \quad (((\cdot \triangleright U) \triangleright \mathrm{El}(\pi_2 \mathrm{id})) \triangleright (\pi_2(\pi_1 \mathrm{id})) \Rightarrow \mathrm{El}(\pi_2(\pi_1 \mathrm{id})))^S (((\mathit{tt}, \mathit{Nat}), \mathit{zero}), \mathit{suc}) \gamma^D = \\
& \quad (((\mathit{tt}, N^D), z^D), s^D) : (\gamma^{D''} : (\gamma^{D'} : (((\gamma^D : \cdot^D \mathit{tt}) \times \mathbf{U}^D \gamma^D \mathit{Nat})) \times (\mathrm{El}(\pi_2 \mathrm{id}))^D \gamma^{D'} \mathit{zero}) \times \\
& \qquad (\Pi (\pi_2(\pi_1 \mathrm{id})) (\pi_2(\pi_1(\pi_1 \mathrm{id}))))^D \gamma^{D''} \mathit{suc}) \to \\
& \quad (((\cdot \triangleright U) \triangleright \mathrm{El}(\pi_2 \mathrm{id})) \triangleright (\pi_2(\pi_1 \mathrm{id})) \Rightarrow \mathrm{El}(\pi_2(\pi_1 \mathrm{id})))^S (((\mathit{tt}, \mathit{Nat}), \mathit{zero}), \mathit{suc}) \\
& \quad (((\mathit{tt}, N^D), z^D), s^D) = \\
& \quad (((\mathit{tt}, N^D), z^D), s^D) : (\gamma^{D''} : (\gamma^{D'} : (((\gamma^D : \cdot^D \mathit{tt}) \times \mathbf{U}^D \gamma^D \mathit{Nat})) \times (\mathrm{El}(\pi_2 \mathrm{id}))^D \gamma^{D'} \mathit{zero}) \times \\
& \qquad (\Pi (\pi_2(\pi_1 \mathrm{id})) (\pi_2(\pi_1(\pi_1 \mathrm{id}))))^D \gamma^{D''} \mathit{suc}) \to \\
& \quad (\gamma^{S''} : (\gamma^{S'} : (((\gamma^S : \cdot^S \mathit{tt} \mathit{tt}) \times \mathbf{U}^S \gamma^S \mathit{Nat} N^D)) \times (\mathrm{El}(\pi_2 \mathrm{id}))^S \gamma^{S'} \mathit{zero} z^D) \times \\
& \qquad (\Pi (\pi_2(\pi_1 \mathrm{id})) (\pi_2(\pi_1(\pi_1 \mathrm{id}))))^S \gamma^{S''} \mathit{suc} s^D = \\
& \quad (((\mathit{tt}, N^D), z^D), s^D) : (\gamma^{D''} : (\gamma^{D'} : (((\gamma^D : \top) \times (\mathit{Nat} \to \mathit{Set}))) \times \mathrm{proj}_2 \gamma^{D'} \mathit{zero}) \times \\
& \qquad (\mathrm{proj}_2 (\mathrm{proj}_1 \gamma^{D''}) n \to \mathrm{proj}_2 (\mathrm{proj}_1 \gamma^{D''}) (\mathit{suc} n)) \to \\
& \quad (\gamma^{S''} : (\gamma^{S'} : (((\gamma^S : \top) \times ((n : \mathit{Nat}) \to N^D n))) \times \mathrm{proj}_2 \gamma^{S'} \mathit{zero} = z^D) \times \\
& \qquad ((n : \mathit{Nat}) \to \mathrm{proj}_2 (\mathrm{proj}_1 (\mathrm{proj}_1 \gamma^{S''})) (\mathit{suc} n) = s^D (\mathrm{proj}_2 (\mathrm{proj}_1 (\mathrm{proj}_1 \gamma^{S''}) n))
\end{align*}
$$

512

513

514

515

516

517

518

519

520

521

522

523

524

525

526

527

528

529

530

This is again a left-nested version of the expected elimination principle

$$ 
\begin{align*}
(N^D : \mathit{Nat} \to \mathit{Set}) (z^D : N^D \mathit{zero}) (s^D : (n : \mathit{Nat}) \to N^D n \to N^D (\mathit{suc} n)) \to \\
(N^S : (n : \mathit{Nat}) \to N^D n) \times (N^S \mathit{zero} = z^D) \times ((n : \mathit{Nat}) \to N^S (\mathit{suc} n) = s^D (N^S n))
\end{align*}
$$

532

533
6:14 For Finitary Induction-Induction, Induction is Enough

535 ▶ Remark 14. The computation rules of the elimination principle are only expected up to the internal equality type, but as we work with a model of ETT, we also get them as definitional equalities by equality reflection.

538 **3 Constructing all IITs from the Theory of IIT Signatures**

In the previous section, using the notions of signature algebras and signature morphisms, we defined IIT signatures and what it means for a model of ETT to support all IITs. In this section we show that if a model of ETT supports the theory of IIT signatures, then it supports all IITs. Using the Church encoding of Definition 6, every model of ETT can describe ITT signatures. In contrast, in Definition 15, we will require existence of an initial signature algebra.

The contents of this section are an adjustment of [21, Sections 4 and 6] to our setting.

546 ▶ **Definition 15.** A model of ETT supports the theory of IIT signatures if there is a signature algebra $\mathcal{I}$ : $\text{SignAlg}$ equipped with a unique morphism $\llbracket - \rrbracket_M : \text{SignMor} | M$ into any algebra $M$. Sometimes we omit the subscript $M$. We call $\mathcal{I}$ the syntax or initial algebra, the morphism $\llbracket - \rrbracket$ is called *recursor*.

550 ▶ **Definition 16 (Syntactic signatures).** In a model of ETT supporting the theory of ITT signatures, we call elements of $\text{Con}^1$ syntactic signatures.

One may wonder what is the relationship between the two notion of signatures.

553 ▶ **Lemma 17.** In a model of ETT supporting the theory of ITT signatures, signatures and syntactic signatures are isomorphic.

555 **Proof.** We can turn a $(\mathit{sig}, \mathit{sigc}) : \text{Sign}$ into $\text{Con}^1$ by $\mathit{sig} |$ and an $\Omega : \text{Con}^1$ into a $\text{Sign}$ by $\left( \lambda M. \llbracket \Omega \rrbracket_M, \lambda M N f. (f \llbracket \Omega \rrbracket_M = (f \circ \llbracket - \rrbracket_M) \Omega = \llbracket \Omega \rrbracket_N) \right)$ where the equality proof in the second component comes from uniqueness of the cursor (we have to define composition of morphisms $\circ$ for this). The compositions of these two maps are the identities: $(\mathit{sig}, \mathit{sigc})$ is mapped to $(\lambda M. \llbracket \mathit{sig} I \rrbracket_M, \dots) = (\lambda M. \llbracket - \rrbracket_M (\mathit{sig} I), \dots)$ which is equal to $(\lambda M. \mathit{sig} M, \dots)$ because of $\mathit{sigc}$; $\Omega$ is mapped to $\llbracket \Omega \rrbracket_I = \Omega$ by uniqueness of $\llbracket - \rrbracket$. ◀

We will define the term signature algebra by which we obtain the constructors $\text{con}$ for any IIT signature. Then we will define another signature algebra which provides the eliminator. Before doing these, we illustrate the idea of both constructions on natural numbers.

564 ▶ **Example 18.** For natural numbers, we will define the constructors $\text{con}$ as the following natural number algebra ($\mathbf{Nat}$, $\mathbf{zero}$, $\mathbf{suc}$). We write variable names instead of de Bruijn indices for readability.

$$567 \mathbf{Nat} := \mathbf{Tm}^1 (\cdot \triangleright N : U \triangleright z : \mathbf{ElN} \triangleright s : N \Rightarrow \mathbf{ElN}) (\mathbf{ElN})$$

$$568 \mathbf{zero} := z$$

$$569 \mathbf{suc} := \lambda t. (s @ t)$$

Natural numbers are simply $l$-terms of type $\mathbf{ElN}$ in the context which is the syntactic signature for natural numbers. In this context, the only way to define a term of type $\mathbf{ElN}$ is to use $z$ and $s$, corresponding to the **zero** and **suc** constructors.

To define the action of the eliminator on a natural number $n : \mathbf{Nat}$, let's look at the type of the displayed algebra interpretation of the number:

$$576 \llbracket n \rrbracket_{\text{ADS}^D} : (\gamma^D : \llbracket \cdot \triangleright N : U \triangleright z : \mathbf{ElN} \triangleright s : N \Rightarrow \mathbf{ElN} \rrbracket^D \text{con}) \to \llbracket \mathbf{ElN} \rrbracket^D (\llbracket n \rrbracket^A \text{con})$$
This says that for a displayed algebra $\gamma^D = (N^D, z^D, s^D)$ over con (i.e. the motives and methods of the eliminator), we get a witness of the predicate $[[\mathrm{El} \ N]]^D = N^D$ at the algebra interpretation of $n$. This is not yet good, as we would like to get $N^D n$ instead of $N^D ([[n]]^A \mathrm{con})$ as a result. However, interpretation into the term signature algebra will imply that $n = [[n]]^A \mathrm{con}$.

**► Definition 19 (Term signature algebra IC<sub>-</sub>).** For an $\Omega : \mathrm{Con}^I$, we define $\mathrm{IC}_\Omega : \mathrm{SignAlg}$ which we call the term signature algebra. It is equipped with a morphism $\Omega^{-1} : \mathrm{SignMor}(\mathrm{IC}_\Omega) \to \mathrm{I}$. We define $\mathrm{IC}_\Omega$ by listing its components Con, Ty, Sub, and so on, one per row. Each component has two parts denoted by $^1$ and $^C$. The $^1$ part just reuses the corresponding components from $\mathrm{I}$, and thus the morphism $\Omega^{-1}$ is defined as the obvious projection. We omit the equality components, as they come from $\mathrm{UIP}$ or are trivial. We also omit the components for terms and substitutions as their $^C$ parts consist of uninformative equational reasoning.

$$
\begin{align*}
\Gamma^1 : \mathrm{Con}^1 &\qquad \Gamma^C : \mathrm{Sub}^1 \Omega \Gamma^1 \to [[\Gamma]]_A \\
A^1 : \mathrm{Ty}^1 \Gamma^1 &\qquad A^C : (\nu : \mathrm{Sub}^1 \Omega \Gamma^1) \to \mathrm{Tm}^1 \Omega (A^1[\nu]) \to [[A]]_A (\Gamma^C \nu) \\
\sigma^1 : \mathrm{Sub}^1 \Gamma^1 \Delta^1 &\qquad \sigma^C : \Delta^C (\sigma^1 \circ \nu) = [[\sigma]]_A (\Gamma^C \nu) \\
t^1 : \mathrm{Tm}^1 \Gamma^1 A^1 &\qquad t^C : A^C \nu (t^1[\nu]) = [[t]]_A (\Gamma^C \nu) \\
(A[\sigma])^1 := A^1[\sigma^1]^1 &\qquad (A[\sigma])^C \nu t := A^C (\sigma^1 \circ \nu) t \\
.^1 := .^1 &\qquad .^C \nu := \mathrm{tt} \\
(\Gamma \triangleright A)^1 := \Gamma^1 \triangleright^1 A^1 &\qquad (\Gamma \triangleright A)^C \nu := (\Gamma^C (\pi_1 \nu), A^C (\pi_1 \nu) (\pi_2 \nu)) \\
U^1 := U^1 &\qquad U^C \nu a := \mathrm{Tm}^1 \Omega (\mathrm{El}^1 a) \\
(\mathrm{El} a)^1 := \mathrm{El}^1 a^1 &\qquad (\mathrm{El} a)^C \nu t := \varepsilon_{ac} \nu \# t \\
(\Pi a B)^1 := \Pi^1 a^1 B^1 &\qquad (\Pi a B)^C \nu t := \lambda\alpha.B^C (\nu, \varepsilon_{ac} \nu \# \alpha) (t \varepsilon_{ac} \nu \# \alpha) \\
(\hat{\Pi} T B)^1 := \hat{\Pi}^1 T B^1 &\qquad (\hat{\Pi} T B)^C \nu t := \lambda\alpha.(B \alpha)^C \nu (t \hat{\alpha})
\end{align*}
$$

**► Example 20.** Now, given a syntactic signature $\Omega : \mathrm{Con}^1$, we get the constructors as an $\Omega$-algebra by $\omega := ([[\Omega]]_{\mathrm{IC}_\Omega})^C \mathrm{id}^1 : [[\Omega]]_A$. If $\Omega$ is the syntactic signature for natural numbers, we get the constructors as in Example 18.

An $a : \mathrm{Tm}^1 \Omega U$ is a sort term for the syntactic signature $\Omega$. If $\Omega$ is the syntactic signature for natural numbers, $a$ can only be $N$ (1 as a de Bruijn index). If $\Omega$ is the syntactic signature for Con-Ty (Example 4), $a$ can be $\mathrm{Con}, \mathrm{Ty} \ \mathrm{empty}, \mathrm{Ty} \ \mathrm{(ext} \ \mathrm{empty} \ \mathrm{(U} \ \mathrm{empty}))$, and so on. In any case, for such an $a$, we obtain $([a]_{\mathrm{IC}_\Omega})^C \mathrm{id}^1 : \mathrm{Tm}^1 \Omega (\mathrm{El} a) = [[a]]_A \omega$. That is, the algebra interpretation of a sort term at the constructors is equal to terms of that sort.

A $t : \mathrm{Tm}^1 \Omega (\mathrm{El} a)$ is a term of a sort type $a$ constructed using the constructors in $\Omega$. For natural numbers, such a $t$ can only be $s$ applied iteratively to $z$. For such a $t$, we obtain $([t]_{\mathrm{IC}_\Omega})^C \mathrm{id}^1 : (t = [[t]]_A \omega)$. That is, a constructor term is equal to its algebra interpretation at the constructors. This is exactly the equation needed at the end of Example 18.

**► Definition 21 (Eliminator signature algebra IE<sub>-</sub>).** Given an $\Omega : \mathrm{Con}^1$, we use the abbreviation $\omega := [[\Omega]]_{\mathrm{IC}_\Omega} \mathrm{id}^1$ as in Example 20. Assuming an $\omega^D : ([[\Omega]]_{\mathrm{ADS}})^D \omega$, we define the signature algebra $\mathrm{IE}_{\omega^D}$. It is equipped with a morphism $\Omega^{-1} : \mathrm{SignMor}(\mathrm{IE}_{\omega^D}) \to \mathrm{I}$. We define $\mathrm{IE}_{\omega^D}$ by listing its components Con, Ty, Sub, and so on, one per row. Each component has two parts denoted by $^1$ and $^E$. The $^1$ part just reuses the corresponding components of $\mathrm{I}$, thus the morphism $\Omega^{-1}$ is defined as the obvious projection. We omit the equality components, as they come from $\mathrm{UIP}$ or are trivial. We also omit the components for terms and substitutions as their $^E$ parts are uninformative equational reasonings.

$$ \Gamma^1 : \mathrm{Con}^1 \qquad \Gamma^E : (\nu : \mathrm{Sub}^1 \Omega \Gamma^1) \to [[\Gamma]]^S ([[\nu]]^A \omega) ([[\nu]]^D \omega^D) $$
6:16 For Finitary Induction-Induction, Induction is Enough

$$
\begin{align*}
A^1 : \text{Ty}^1 \Gamma^1 &\qquad A^E : (\nu : \text{Sub}^1 \Omega \Gamma^1)(t : \text{Tm}^1 \Omega (A^1[\nu])) \rightarrow \\
&\qquad [[A]^S (\Gamma^E \nu) ([[t]]^A \omega) ([[t]]^D \omega^D)] \\
\sigma^1 : \text{Sub}^1 \Gamma^1 \Delta^1 &\qquad \sigma^E : \Delta^E (\sigma^1 \circ \nu) = [[\sigma]^S (\Gamma^E \nu)] \\
t^1 : \text{Tm}^1 \Gamma^1 A^1 &\qquad t^E : A^E \nu (t^1[\nu]) = [[t]^S (\Gamma^E \nu)] \\
(A[\sigma])^1 := A^1[\sigma^1]^1 &\qquad (A[\sigma])^E \nu t := A^E (\sigma^1 \circ \nu) t \\
.^1 := .^1 &\qquad .^E \nu := tt \\
(\Gamma \triangleright A)^1 := \Gamma^1 \triangleright^1 A^1 &\qquad (\Gamma \triangleright A)^E \nu := (\Gamma^E (\pi_1 \nu), A^E (\pi_1 \nu) (\pi_2 \nu)) \\
U^1 := U^1 &\qquad U^E \nu a := \lambda \alpha . [[\alpha]]^c \text{id}^\# ([[\alpha]]^c \text{id}^\# \alpha]^D \omega^D) \\
(\text{El } a)^1 := \text{El}^1 a^1 &\qquad (\text{El } a)^E \nu t := ([[a]^S (\Gamma^E \nu) ([[t]]^A \omega)] [[t]]^c \text{id} \stackrel{\text{id}}{=} [[a]^S (\Gamma^E \nu) t] a^E \stackrel{\text{id}}{=} [[t]]^D \omega^D)) \\
(\Pi a B)^1 := \Pi^1 a^1 B^1 &\qquad (\Pi a B)^E \nu t := \\
&\qquad \lambda \alpha . [[\alpha]]^c \text{id}^\# (B^E (\nu, [[a]]^c \text{id}, [[\nu]]^c \text{id}^\# \alpha) (t \text{ @ } [[a]]^c \text{id}, [[\nu]]^c \text{id}^\# u)) \\
(\hat{\Pi} T B)^1 := \hat{\Pi}^1 T B^1 &\qquad (\hat{\Pi} T B)^E \nu t := \lambda \alpha . (B^E \nu (t \hat{\otimes} \alpha))
\end{align*}
$$

$$
\sigma^1 : \text{Sub}^1 \Gamma^1 \Delta^1 \qquad \sigma^E : \Delta^E (\sigma^1 \circ \nu) = [[\sigma]^S (\Gamma^E \nu)
$$

$$
t^1 : \mathrm{Tm}^1 \Gamma^1 A^1 \qquad t^E : A^E \nu (t^1[\nu]) = [[t]^S (\Gamma^E \nu)
$$

$$
(A[\sigma])^1 := A^1[\sigma^1]^1 \qquad (A[\sigma])^E \nu t := A^E (\sigma^1 \circ \nu) t
$$

$$
.^1 := .^1 \qquad .^E \nu := tt
$$

$$
(\Gamma \triangleright A)^1 := \Gamma^1 \triangleright^1 A^1 \qquad (\Gamma \triangleright A)^E \nu := (\Gamma^E (\pi_1 \nu), A^E (\pi_1 \nu) (\pi_2 \nu))
$$

$$
U^1 := U^1 \qquad U^E \nu a := \lambda \alpha . [[\alpha]]^c \text{id}^\# ([[\alpha]]^c \text{id}^\# \alpha]^D \omega^D)
$$

$$
(\mathrm{El} a)^1 := \mathrm{El}^1 a^1 \qquad (\mathrm{El} a)^E \nu t := ([[a]^S (\Gamma^E \nu) ([[t]]^A \omega)] [[t]]^c \mathrm{id} \stackrel{\mathrm{id}}{=} [[a]^S (\Gamma^E \nu) t] a^E \stackrel{\mathrm{id}}{=} [[t]]^D \omega^D))
$$

$$
(\Pi a B)^1 := \Pi^1 a^1 B^1 \qquad (\Pi a B)^E \nu t :=
$$

$$
\lambda \alpha . [[\alpha]]^c \text{id}^\# (B^E (\nu, [[a]]^c \text{id}, [[\nu]]^c \text{id}^\# \alpha) (t \text{ @ } [[a]]^c \text{id}, [[\nu]]^c \text{id}^\# u))
$$

$$
(\hat{\Pi} T B)^1 := \hat{\Pi}^1 T B^1 \qquad (\hat{\Pi} T B)^E \nu t := \lambda \alpha . (B^E \nu (t \hat{\otimes} \alpha))
$$

► **Example 22.** Given the assumptions $\Omega$, $\omega^D$ of IE, we obtain the eliminator by $[[\Omega]]_{\mathrm{IE}_{\omega^D}}$ id¹ :
$[[\Omega]]^S \omega \omega^D$. The eliminator is a section of the displayed algebra $\omega^D$, that is, a dependent
function together with equalities witnessing that all the operations are preserved. If $\Omega$ is the
syntactic signature for natural numbers, we get the eliminator of Example 18.

For a sort term $a : \mathrm{Tm}^1 \Omega \mathrm{U}$, the interpretation $([[]]_{\mathrm{IE}_{\omega^D}})^E$ id says that $(\lambda \alpha . [[\alpha]]^D \omega^D) = [[a]]^S ([[\Omega]]^E \mathrm{id})$, that is, the function for the sort $a$ in the eliminator section is the displayed algebra interpretation at $\omega^D$ (motives and methods). For natural numbers, this is the same as $(\lambda n . [[n]]^D (N^D, z^D, s^D)) = (\lambda n . \mathrm{elimNat} (N^D, z^D, s^D) n)$).

The interpretation of a constructor term $t : \mathrm{Tm}^1 \Omega (\mathrm{El} a)$ is uninteresting as it provides an
equality between two different equality proofs of the computation $(\beta)$ rule for $t$.

**Theorem 23.** If a model of ETT supports the theory of IIT signatures, then it supports all IITs.

**Proof.** For a signature (*sig*, *sigc*), we define constructors as

$$
\mathrm{con}_{sig} := ([[sig\,I]]_{\mathrm{Ic}_{sig}})^c \mathrm{id}^1 : (\mathrm{sig\,ADS})^A
$$

This typechecks as $[[sig\,I]]_A = [[-]]_A (sig\,I) \stackrel{sigc}{\equiv} sig\,A = (sig\,ADS)^A$. We define the eliminator
by and an

$$
\mathrm{elim}_{sig} \gamma^D := ([[sig\,I]]_{\mathrm{IE}_{\gamma^D}})^E \mathrm{id}^1 : (\mathrm{sig\,ADS})^S \mathrm{con}_{sig} \gamma^D.
$$

This typechecks firstly because the type of $\gamma^D$ matches the type of the parameter of IE:

$$
(sig\,ADS)^D \mathrm{con}_{sig} \stackrel{\mathrm{sigc}}{\equiv} ([[-]]_{ADS} (sig\,I))^D \mathrm{con}_{sig} = ([sig\,I]_{ADS})^D \mathrm{con}_{sig},
$$

and the result also has the correct type:

$$
[[sig\,I]]^S \mathrm{con}_{sig} \gamma^D = ([[-]]_{ADS} (sig\,I))^S \mathrm{con}_{sig} \gamma^D \stackrel{\mathrm{sigc}}{\equiv} (sig\,ADS)^S \mathrm{con}_{sig} \gamma^D.
$$

► **Remark 24.** In the above proof, we crucially relied on the *sigc* property to define the
constructors (and the eliminator). This is why the simple Church encoding of signatures is
not sufficient.
# 4 Constructing the Theory of IIT Signatures

In this section we show that any model of ETT which supports indexed W-types also supports the theory of signatures, and as a consequence of Theorem 23, all IITs. For this, we work in the internal language of a model of ETT supporting indexed W-types [3]. Indexed W-types correspond to the usual notion of (possibly mutual) indexed inductive types. We use Agda-style notation to define such inductive families: we list the sorts and constructors and use pattern matching when eliminating from them. For an encoding of mutual inductive families as indexed W-types, see e.g. [23].

We construct the theory of IIT signatures in the following steps:

1. We view the theory of signatures as a type theory, and we define its untyped syntax as mutual inductive types together with typing judgments given by inductive relations on the untyped syntax. Then the syntax $| : \mathbf{SignAlg}$ is constructed using those untyped terms for which the typing relation holds.

2. We construct $[[\Gamma]] : \mathbf{SignMor} | M$ for arbitrary $M : \mathbf{SignAlg}$, by:

a. defining a relation $\sim$ between the well-typed syntax and a given signature algebra. The idea is that given a syntactic context $\Gamma$ and a semantic context $\Gamma^M$ of the signature algebra $M$, we have $\Gamma \sim \Gamma^M$ if and only if $[[\Gamma]] = \Gamma^M$, and similarly for types, terms, and substitutions;

b. showing that this relation is functional and thus obtaining a morphism.

3. Proving the uniqueness of this morphism by showing that any morphism $f : \mathbf{SignMor} | M$ satisfies the relation. For example, for any syntactic context $\Gamma$ we have $\Gamma \sim f \Gamma$.

The next sections detail each of these steps.

## 4.1 Syntax

The goal is to define the syntactic signature algebra where contexts are pairs of a precontext together with a well-formedness proof, and similarly for types, terms and substitutions.

Crucially, we do not have conversion relations for typed syntax, nor do we need to use quotients when constructing the syntax. This is possible because there are no $\beta$-rules in the theory of signatures. Hence, we consider only normal terms in the untyped syntax, and define weakening and substitution by recursion. Avoiding quotients is important for two reasons. First, it greatly simplifies formalisation. Second, we aim to reduce the theory of signatures only to inductive types, thus making Theorem 57 stronger.

Now we present the definition of the untyped syntax and the associated typing judgments.

### 4.1.1 Untyped Syntax and its Properties

► **Definition 25** (Untyped syntax). *The untyped syntax is defined as the following inductive datatype.*

(1) *Substitution calculus*

Con<sup>P</sup> : Set

Ty<sup>P</sup> : Set

Sub<sup>P</sup> : Set

Tm<sup>P</sup> : Set

.<sup>P</sup> : Con<sup>P</sup>

e<sup>P</sup> : Sub<sup>P</sup>
6:18 For Finitary Induction-Induction, Induction is Enough

$$702 \quad \vdash_P : \mathrm{Con}^P \to \mathrm{Ty}^P \to \mathrm{Con}^P$$

$$703 \quad \vdash_P : \mathrm{Sub}^P \to \mathrm{Tm}^P \to \mathrm{Sub}^P$$

$$704 \quad \mathrm{var}^P : \mathbb{N} \to \mathrm{Tm}^P$$

(2) Universe

$$705 \quad \mathrm{U}^P : \mathrm{Ty}^P$$

$$707 \quad \mathrm{El}^P : \mathrm{Tm}^P \to \mathrm{Ty}^P$$

(3) Inductive parameters

$$709 \quad \Pi^P : \mathrm{Tm}^P \to \mathrm{Ty}^P \to \mathrm{Ty}^P$$

$$710 \quad \vdash_P : \mathrm{Tm}^P \to \mathrm{Tm}^P \to \mathrm{Tm}^P$$

(4) External parameters

$$712 \quad \hat{\Pi}^P : (T : \mathrm{Set}) \to (T \to \mathrm{Ty}^P) \to \mathrm{Ty}^P$$

$$713 \quad \tilde{\Pi}^P : (T : \mathrm{Set}) \to (T \to \mathrm{Tm}^P) \to \mathrm{Tm}^P$$

$$714 \quad \hat{\vdash} : \mathrm{Tm}^P \to (\alpha : T) \to \mathrm{Tm}^P$$

(5) Default value

$$716 \quad \mathrm{err}^P : \mathrm{Tm}^P$$

Variables are modeled as de Bruijn indices, i.e. as natural numbers pointing to a position in the context. We use the additional default constructor errP : TmP in case of error (ill-scoped substitution). The typing judgments will not mention errP. The main interest of errP is that it behaves like a closed term (which the theory of signatures lacks), in the sense that it is invariant under substitution. This makes expected equalities about substitution true even in the ill-typed case, thus reducing the number of hypotheses for the corresponding lemmas (see Lemma 32).

We will define substitutions $\vdash[-]$ of types and terms recursively.

Note that $(\Pi^P A B)[\sigma]$ should be defined as $\Pi^P (A[\sigma]) (B[\mathrm{wk}_0 \sigma, \mathrm{var}^P 0])$, and thus we need to define $\mathrm{wk}_0$, the weakening of substitutions. The basic idea is to increment the de Bruijn indices of all the variables. Actually, this is not so simple because of the $\Pi^P$ type: we want to define $\mathrm{wk}_0$ $(\Pi^P A B)$ as the $\Pi$ type of the weakening of $A$ and $B$, but here, $B$ must be weakened with respect to the second last variable of the context, rather than the last one. For this reason, we need to generalise the weakening as occuring anywhere in the context.

► **Definition 26** (Untyped weakening). We define untyped weakening recursively on terms by the following functions.

$$734 \quad \mathrm{wk}_n : \mathrm{Ty}^P \to \mathrm{Ty}^P$$

$$735 \quad \mathrm{wk}_n : \mathrm{Tm}^P \to \mathrm{Tm}^P$$

$$736 \quad \mathrm{wk}_0 : \mathrm{Sub}^P \to \mathrm{Sub}^P$$

The natural number $n$ specifies at which position of the context the weakening occurs. Here, $\mathrm{wk}_0$ weakens with respect to the last variable.

Later, in Lemma 36, we show that weakening preserves typing. Stating a typing rule for this operation requires weakening at the middle of a context. This is why we define pairs of untyped contexts, which should be thought of as a splitting of a context at some position. We call the second context a telescope over the first one.

► **Definition 27** (Untyped telescopes). An untyped telescope is given simply by a $\mathrm{Con}^P$.
► **Definition 28** (Merging of a context and a telescope).

$$ \neg; \neg : \mathrm{Con}^P \to \mathrm{Con}^P \to \mathrm{Con}^P $$

745

$$ \Gamma; : \quad := \Gamma $$

746

$$ \Gamma; (\Delta \triangleright^P A) := (\Gamma; \Delta) \triangleright^P A $$

747
748

► **Definition 29** (Weakening for telescopes). *Weakening for telescopes is defined pointwise.*

$\|\Gamma\|$ denotes the length of the context $\Gamma$.

749

$$ \mathrm{wk}_0 : \mathrm{Con}^P \to \mathrm{Con}^P $$

751

$$ \mathrm{wk}_0 .^P \quad := .^P $$

752

$$ \mathrm{wk}_0 (\Delta \triangleright^P A) := \mathrm{wk}_0 \Delta \triangleright^P \mathrm{wk}_{\|\Delta\|} A $$

753
754

This will be used to give typing rules for telescopes in Definition 35.

755

► **Definition 30** (Untyped unary substitution). *We define single substitution by recursion on the presyntax:*

756

757

$$ -[- := -] : \mathrm{Ty}^P \to \mathbb{N} \to \mathrm{Tm}^P \to \mathrm{Ty}^P $$

758

$$ -[- := -] : \mathrm{Tm}^P \to \mathbb{N} \to \mathrm{Tm}^P \to \mathrm{Tm}^P $$

759
760

This is enough to state the typing judgments: indeed, the typing rule for application involves only a unary substitution.

761

762

However, to construct the syntax as a signature algebra, we need to define parallel substitutions:

763

764

► **Definition 31** (Untyped substitution calculus).

$$ -[-] : \mathrm{Ty}^P \to \mathrm{Sub}^P \to \mathrm{Ty}^P $$

765

$$ -[-] : \mathrm{Tm}^P \to \mathrm{Sub}^P \to \mathrm{Tm}^P $$

766

$$ - \circ - : \mathrm{Sub}^P \to \mathrm{Sub}^P \to \mathrm{Sub}^P $$

767
768

These can be defined either by iterating unary substitutions, or by recursion on untyped syntax: the two ways yield provably equal definitions. In the following, we assume that they are defined by recursion. We also make use of the following definition:

769

770

771

$$ \mathrm{keep} : \mathrm{Sub}^P \to \mathrm{Sub}^P $$

772

$$ := \lambda\sigma.(\mathrm{wk}_0\sigma, .^P \mathrm{var}^P 0) $$

773
774

The idea is that if $\sigma$ is a substitution from $\Gamma$ to $\Delta$, then $\mathrm{keep}\sigma$ is a substitution between contexts $\Gamma \triangleright A[\sigma]$ and $\Delta \triangleright A$ for any type $A$ where the last term is just a de Bruijn index 0. This occurs when defining $(\Pi^P A B)[\sigma]$ as $\Pi^P (A[\sigma]) (B[\mathrm{keep}\sigma])$.

775

776

777

We define the identity substitution on a context $\Gamma$ as follows, where $\mathrm{keep}^{\|\Gamma\|}$ is keep iterated $\|\Gamma\|$ times:

778

779

$$ \mathrm{id}^P : \mathrm{Con}^P \to \mathrm{Sub}^P $$

780

$$ := \lambda\Gamma.\mathrm{keep}^{\|\Gamma\|} \epsilon^P $$

781
782

► **Lemma 32** (Exchange laws for weakening and substitution). *Below, $Z$ denotes either a term or a type and $\mathrm{keep}^n$ denotes the $n$ times iteration of $\mathrm{keep}$.*

783

784

$$ \mathrm{wk}-\mathrm{wk} : \mathrm{wk}_{n+p+1}(\mathrm{wk}_n Z) = \mathrm{wk}_n(\mathrm{wk}_{n+p} Z) $$

785
6:20 For Finitary Induction-Induction, Induction is Enough

$$
786 \quad \mathrm{wk}_n[n] \quad : (\mathrm{wk}_n Z)[n := z] = Z
$$

$$
787 \quad \mathrm{wk}_+[] \quad : (\mathrm{wk}_{n+p+1} Z)[n := \mathrm{wk}_p u] = \mathrm{wk}_{n+p} (Z[n := u])
$$

$$
788 \quad \mathrm{wk}[+] \quad : (\mathrm{wk}_n Z)[n + p + 1 := u] = \mathrm{wk}_n (Z[n + p := u])
$$

$$
789 \quad [[+]] \quad : Z[n := u][n + p := z] = Z[n + p + 1 := z][n := (u[p := z])]
$$

$$
790 \quad [\mathrm{keep}^n - \mathrm{wk}_0] \quad : Z[\mathrm{keep}^n (\mathrm{wk}_0 \sigma)] = \mathrm{wk}_n(Z[\mathrm{keep}^n \sigma])
$$

$$
791 \quad \mathrm{wk}_n[\mathrm{keep}^n-,] \quad : (\mathrm{wk}_n Z)[\mathrm{keep}^n (\sigma, {}^p u)] = Z[\mathrm{keep}^n \sigma]
$$

$$
792 \quad [:=][\mathrm{keep}] \quad : Z[n := u][\mathrm{keep}^n \sigma] = Z[\mathrm{keep}^{n+1} \sigma][n := u[\sigma]]
$$

794 Proof. By induction on the untyped syntax.

<figure><img src="image_4.png" /></figure>

795 ► **Corollary 33.** *As particular cases for* $n=0$, *we get*

$$
796 \quad \circ \mathrm{wk}_0 : \sigma \circ (\mathrm{wk}_0 \tau) = \mathrm{wk}_0 (\sigma \circ \tau)
$$

$$
797 \quad \mathrm{wk}_0 \circ, : \mathrm{wk}_0 \sigma \circ (\tau, {}^p t) = \sigma \circ \tau
$$

$$
798 \quad [\mathrm{wk}_0] \quad : t[\mathrm{wk}_0 \sigma] = \mathrm{wk}_0(t[\sigma])
$$

$$
799 \quad \mathrm{wk}_0[, ] \quad : (\mathrm{wk}_0 Z)[\sigma, {}^p u] = Z[\sigma]
$$

$$
800 \quad [0 :=] : Z[0 := u][\sigma] = Z[\mathrm{keep} \sigma][0 := u[\sigma]]
$$

801

► **Lemma 34** (Composition functor law and associativity).

$$
802 \quad [] : Z[\sigma][\tau] = Z[\sigma \circ \tau]
$$

803

$$
804 \quad \mathrm{ass} : (\sigma \circ \delta) \circ \tau = \sigma \circ (\delta \circ \tau)
$$

805 We defer laws for identity substitutions after the definition of the typing judgments, as
806 the proofs require that some inputs are well-typed.

807 4.1.2 Typing Relations and Their Properties

808 ► **Definition 35 (Typing relations).** The typing relations are defined as the following inductive
type indexed over the untyped syntax:

810 (1) *Substitution calculus*

$$
811 \quad \vdash : \mathrm{Con}^P \to \mathrm{Set}
$$

$$
812 \quad \vdash - : \mathrm{Con}^P \to \mathrm{Ty}^P \to \mathrm{Set}
$$

$$
813 \quad \vdash - \in \mathbb{N} : \mathrm{Con}^P \to \mathbb{N} \to \mathrm{Ty}^P \to \mathrm{Set}
$$

$$
814 \quad \vdash - \in - : \mathrm{Con}^P \to \mathrm{Tm}^P \to \mathrm{Ty}^P \to \mathrm{Set}
$$

$$
815 \quad \vdash - \Rightarrow - : \mathrm{Con}^P \to \mathrm{Sub}^P \to \mathrm{Con}^P \to \mathrm{Set}
$$

$$
816 \quad .^w : .^p \vdash
$$

$$
817 \quad \epsilon^w : \Gamma \vdash \epsilon^P \Rightarrow .^P
$$

$$
818 \quad \vdash^w - : (\Gamma \vdash) \to (\Gamma \vdash A) \to \Gamma \vdash^P A \vdash
$$

$$
819 \quad ,^w : (\Delta \vdash) \to (\Gamma \vdash \sigma \Rightarrow \Delta) \to (\Delta \vdash A) \to (\Gamma \vdash t \in A[\sigma]) \to \Gamma \vdash \sigma, {}^p t \Rightarrow \Delta \vdash^P A
$$

$$
820 \quad \mathrm{var}^w : (\Gamma \vdash n \in \mathbb{N} A) \to \Gamma \vdash \mathrm{var}^p n \in A
$$

$$
821 \quad 0^w : (\Gamma \vdash) \to (\Gamma \vdash A) \to \Gamma \vdash^P A \vdash 0 \in \mathbb{N} \ w k^P A
$$

$$
822 \quad S^w : (\Gamma \vdash) \to (\Gamma \vdash A) \to (\Gamma \vdash n \in \mathbb{N} A) \to (\Gamma \vdash B) \to \Gamma \vdash^P B \vdash S n \in \mathbb{N} w k^P A
$$

823

(2) *Universe*
$$U^w : (\Gamma \vdash) \rightarrow \Gamma \vdash U^P$$

$$E^l w : (\Gamma \vdash) \rightarrow (\Gamma \vdash a \in U^P) \rightarrow \Gamma \vdash E^l P a$$

(3) Inductive parameters

$$\Pi^w : (\Gamma \vdash) \rightarrow (\Gamma \vdash a \in U^P) \rightarrow (\Gamma \triangleright^P E^l P a \vdash B) \rightarrow \Gamma \vdash \Pi^P a B$$

$$\begin{align*}
\mathit{app}^w : (\Gamma \vdash) & \rightarrow (\Gamma \vdash a \in U^P) \rightarrow (\Gamma \triangleright^P E^l P a \vdash B) \\
& \rightarrow (\Gamma \vdash t \in \Pi^P a B) \rightarrow (\Gamma \vdash u \in E^l P a) \rightarrow \Gamma \vdash t \hat{\otimes}^P u \in B[0 := u]
\end{align*}$$

(4) External parameters

$$\hat{\Pi}^w : (T : \mathit{Set}) \rightarrow (A : T \rightarrow \mathit{Ty}^P) \rightarrow (\Gamma \vdash) \rightarrow ((t : T) \rightarrow \Gamma \vdash A t) \rightarrow \Gamma \vdash \hat{\Pi}^P T A$$

$$\begin{align*}
\mathit{app}^w : (T : \mathit{Set}) & \rightarrow (A : T \rightarrow \mathit{Ty}^P) \rightarrow (\Gamma \vdash) \rightarrow ((t : T) \rightarrow \Gamma \vdash A t) \\
& \rightarrow (\Gamma \vdash t \in \hat{\Pi}^P T A) \rightarrow (u : T) \rightarrow \Gamma \vdash t \hat{\otimes} u \in A u
\end{align*}$$

There is possibility of redundancy in the arguments of the constructors. Here, we are “paranoid” (nomenclature from [9]), so that we get more inductive hypotheses when performing recursion.

► Lemma 36 (Weakening preserves typing).

$$w k_0^w : (\Gamma \vdash A) \rightarrow (\Gamma; \Delta \vdash) \rightarrow \Gamma \triangleright^P A; w k_0 \Delta \vdash$$

$$w k^w : (\Gamma \vdash A) \rightarrow (\Gamma; \Delta \vdash B) \rightarrow \Gamma \triangleright^P A; w k_0 \Delta \vdash w k_{\parallel \Delta \parallel} B$$

$$w k^w : (\Gamma \vdash A) \rightarrow (\Gamma; \Delta \vdash t \in B) \rightarrow \Gamma \triangleright^P A; w k_0 \Delta \vdash w k_{\parallel \Delta \parallel} t \in w k_{\parallel \Delta \parallel} B$$

$$w k_0^w : (\Gamma \vdash A) \rightarrow (\Gamma \vdash \sigma \Rightarrow \Delta) \rightarrow \Gamma \triangleright^P A \vdash w k_0 \sigma \Rightarrow \Delta$$

**Proof.** By mutual induction on the typing relations.

<figure><img src="image_5.png" /></figure>

We show that judgments are stable under substitution.

► Lemma 37 (Substitution preserves typing).

$$[w^w] : (\Gamma \vdash) \rightarrow (\Delta \vdash A) \rightarrow (\Gamma \vdash \sigma \Rightarrow \Delta) \rightarrow \Gamma \vdash A[\sigma]$$

$$[w^w] : (\Gamma \vdash) \rightarrow (\Delta \vdash t \in A) \rightarrow (\Gamma \vdash \sigma \Rightarrow \Delta) \rightarrow \Gamma \vdash t[\sigma] \in A[\sigma]$$

$$[w^w] : (\Delta \vdash x \in_N A) \rightarrow (\Gamma \vdash \sigma \Rightarrow \Delta) \rightarrow \Gamma \vdash x[\sigma] \in A[\sigma]$$

$$\circ w : (\Gamma \vdash) \rightarrow (\Gamma \vdash \sigma \Rightarrow \Delta) \rightarrow (\Delta \vdash \tau \Rightarrow E) \rightarrow \Gamma \vdash \tau \circ \sigma \Rightarrow E$$

**Proof.** By mutual induction on the typing relations.

<figure><img src="image_6.png" /></figure>

We show the category and functor laws involving identity substitution for well-formed types, terms and substitutions.

► Lemma 38 (Identity laws).

$$[\mathit{id}^P] : (\Gamma \vdash A) \rightarrow A[\mathit{id}^P \Gamma] = A$$

$$[\mathit{id}^P] : (\Gamma \vdash x \in_N A) \rightarrow x[\mathit{id}^P \Gamma] = Vx$$

$$[\mathit{id}^P] : (\Gamma \vdash t \in A) \rightarrow t[\mathit{id}^P \Gamma] = t$$

$$\mathit{id}^P : (\Gamma \vdash \sigma \Rightarrow \Delta) \rightarrow \sigma \circ \mathit{id}^P \Gamma = \sigma$$

$$\mathit{id}^l : (\Gamma \vdash \sigma \Rightarrow \Delta) \rightarrow \mathit{id}^l \Delta \circ \sigma = \sigma$$

Finally, we show that the identity substitution itself is well-typed:
6:22 For Finitary Induction-Induction, Induction is Enough

► Lemma 39 (Typing for the identity substitution).

$$
\begin{array}{l}
\text{id}^w : (\Gamma \vdash) \rightarrow \Gamma \vdash \text{id}^p \Gamma \Rightarrow \Gamma \\
\text{id}^w : (\Gamma \vdash) \rightarrow \Gamma \vdash \text{id}^p \Gamma \Rightarrow \Gamma
\end{array}
$$

862
863
► **Definition 40 (Proposition).** A type is a proposition, or proof-irrelevant, if it has at most one inhabitant.

$$
864 \qquad \text{is-prop } T := (a : T) \to (a' : T) \to a = a'
$$

► Lemma 41 (Proof irrelevance of typing relations).

865
Con<sup>wp</sup> : is-prop (Γ ⊢)

866
Ty<sup>wp</sup> : is-prop (Γ ⊢ A)

867
Var<sup>wp</sup> : is-prop (Γ ⊢ x ∈<sub>N</sub> A)

868
Tm<sup>wp</sup> : is-prop (Γ ⊢ t ∈ A)

869
Sub<sup>wp</sup> : is-prop (Γ ⊢ σ ⇒ Δ)

870

► Lemma 42 (Unicity of typing).

871
Tm<sup>w</sup>=Ty : (Γ ⊢ t ∈ A) → (Γ ⊢ t ∈ B) → A = B

872
873
Var<sup>w</sup>=Ty : (Γ ⊢ x ∈<sub>N</sub> A) → (Γ ⊢ x ∈<sub>N</sub> B) → A = B

874
875
876
877
Let us consider for instance the application constructor app<sup>w</sup>: for a codomain type B it yields an overall type C = B[0 := u] for an application. Even if C is known a priori, there may be another B for which B[0 := u] = C, possibly leading to many proofs that t @<sup>p</sup> u has type C. Unicity of typing solves this issue, as B is then uniquely determined by the type Π<sup>p</sup> AB of t.

878

4.1.3 The Syntax as a Signature Algebra

879
880
► **Definition 43 (Syntax for the theory of signatures).** We define the syntax as an element of SignAlg by pairs of untyped syntax and typing relations:

881
Con<sup>l</sup> ::= Σ<sub>Γ</sub> Γ

882
Ty<sup>l</sup>(Γ, Γ<sup>w</sup>) := Σ<sub>A</sub> Γ ⊢ A

883
Tm<sup>l</sup>(Γ, Γ<sup>w</sup>)(A, A<sup>w</sup>) := Σ<sub>t</sub> Γ ⊢ t ∈ A

884
Sub<sup>l</sup>(Γ, Γ<sup>w</sup>)(Δ, Δ<sup>w</sup>) := Σ<sub>σ</sub> Γ ⊢ σ ⇒ Δ

885

886
887
888
The other fields are given straightforwardly. Regarding the equations, it is enough to prove them only for the untyped syntactic part: as we argued in Lemma 41, the proofs of typing judgments are automatically equal.

889
890
891
892
893
894
► Remark 44. Up until Definition 43, UIP is not used. Function extensionality on the other hand is necessary because the untyped metatheoretic Π takes a metatheoretic function as an argument. An example induction step that uses function extensionality is in Lemma 38, in particular in the case (ΠT A)[id] = ΠT A. Indeed, the left hand side of this equation is equal to ΠT (λt.(At)[id]) by definition, whereas the induction hypothesis states that (t : T) → (At)[id] = At.

895
896
897
898
## 4.2 Relating the Syntax to a Signature Algebra

It remains to show that the constructed syntax l is the initial signature algebra. To achieve this, we first define a relation between the syntax and any signature algebra, then show that the relation is functional, which lets us extract a signature morphism from the relation.

This approach is an alternative presentation of Streicher's method for interpreting preterms in an arbitrary model of type theory [30]. Streicher first defines a family of partial maps from the presyntax to a model, then shows that the maps are total on well-formed input. We have found that our approach is significantly easier to formalise. To see why, note that the right notion of partial map in type theory, which does not presume decidable definedness, is fairly heavyweight:

$$ \text{PartialMap } A B := A \to ((P : \text{Set}) \times \text{is-prop } P \times (P \to B)) $$

In the above definition, we notice an opportunity for converting a fibered definition of a type family into an indexed one; if we drop the propositionality for P for the time being, we may equivalently return a family indexed over B, which is exactly just a relation $A \to B \to \text{Set}$. Then, in our approach, we recover uniqueness of P through the functionality requirement on the $A \to B \to \text{Set}$ relation, and totality by already assuming well-formedness of A. In type theory, using indexed families instead of display maps is a common convenience, since the former are natively supported, while the latter require carrying around auxiliary propositional equalities.

### 4.2.1 The Functional Relation

Given an $M : \text{SignAlg}$, we define the functional relation satisfied by the $[[\text{−}]] : \text{SignMor} l M$ by recursion on the typing judgments. If $\Gamma$ is a context in l and $\Gamma^M$ is a semantic context (i.e. a context in the signature algebra $M$), we want to define a type $\Gamma \sim \Gamma^M$ equivalent to $[[\Gamma]] = \Gamma^M$. Of course, at this stage, $[[\text{−}]]$ is not available yet since the point of defining this relation is to construct $[[\text{−}]]$ in the end.

For a type $A$ in a context $\Gamma$, we want to define a relation $A \sim A^M$ that is equivalent to $[[A]] = A^M$. For this equality to make sense, the semantic type $A^M$ must live in the semantic context $[[\Gamma]]$. But again, $[[\text{−}]]$ is not yet available at this stage. Exploiting the expected equivalence between $\Gamma \sim \Gamma^M$ and $[[\Gamma]] = \Gamma^M$, we may consider defining $A \sim A^M$ under the hypotheses that $A^M$ lies in a semantics context $\Gamma^M$ which is related to $\Gamma$. Then, the type of the relation for types is

$$ (\Gamma : \text{Con}^1) \to (A : \text{Ty}^1 \Gamma) \to (\Gamma^M : \text{Con}^M) \to (\Gamma \sim \Gamma^M) \to (A^M : \text{Ty}^M \Gamma^M) \to \text{Set} $$

Note that the relation on contexts must be defined mutually with the relation on types (see for example the case of context extension), but here, the relation on contexts appears as the type of an argument of the relation on types. We want to avoid using such recursive-recursive definitions as they are not allowed by the elimination principles of indexed inductive types, so we instead just remove the hypothesis $\Gamma \sim \Gamma^M$ from the list of arguments. We proceed similarly for terms and substitutions. Actually, this removal is not without harm. For example, consider relating the empty substitution $\Gamma \vdash \epsilon^P \Rightarrow .^P$ to a semantic substitution $\sigma^M : \text{Sub}^M \Gamma^M \Delta^M$. We would like to assert that $\sigma^M$ equals the empty semantic substitution $\epsilon^M$, but this is not possible because typechecking requires that $\Delta^M$ is the empty semantic context. This is precisely what was ensured by the hypothesis $\Gamma^1 \sim \Delta^M$ we removed. Our way out here is to state that $\sigma^M$ is related to the empty substitution if the target semantic context $\Delta^M$ is empty, and, acknowledging this equality, if $\sigma^M$ is the empty substitution.
6:24 For Finitary Induction-Induction, Induction is Enough

Let us mention another possible solution for avoiding recursion-recursion: defining $A \sim A^M$ so that it is equivalent to $(e : [[\Gamma]] = \Gamma^M) \times ([[A]]_{=e\#} A^M)$. In comparison, our approach yields a more concise definition of the relation. For example, in the case of the universe, this would lead to the definition $U^w \Gamma^w \sim A^M := (\Gamma^w \sim \Gamma^M) \times (A^M = U^M)$, instead of our definition $U^w \Gamma^w \sim A^M := (A^M = U^M)$.

**► Definition 45 (Relation $\sim$).** We define the relation by recursion on the typing judgments. In the following, we abbreviate $A^w \sim_{\Gamma^M} A^M$ by $A^w \sim A^M$ when $\Gamma^M$ can be inferred, and similarly for terms and substitutions.

(1) *Substitution calculus*

$$ \sim - \qquad : \Gamma \vdash \rightarrow \mathrm{Con}^M \rightarrow \mathrm{Set} $$

$$ \sim_{\Gamma^M} - \qquad : \Gamma \vdash A \rightarrow \mathrm{Ty}^M \Gamma^M \rightarrow \mathrm{Set} $$

$$ \sim_{\Gamma^M \vdash A^M} - \qquad : \Gamma \vdash t \in A \rightarrow \mathrm{Tm}^M \Gamma^M A^M \rightarrow \mathrm{Set} $$

$$ \sim_{\Gamma^M \vdash A^M} - \qquad : \Gamma \vdash x \in A \rightarrow \mathrm{Tm}^M \Gamma^M A^M \rightarrow \mathrm{Set} $$

$$ \sim_{\Gamma^M \Rightarrow \Delta^M} - \qquad : \Gamma \vdash \sigma \Rightarrow \Delta \rightarrow \mathrm{Sub}^M \Gamma^M \Delta^M \rightarrow \mathrm{Set} $$

$$ \sim w \sim \Gamma^M \qquad := \Gamma^M = w $$

$$ \sim_{\Gamma^M \Rightarrow E^M} \delta^M \qquad := (e_E : E^M = w) \times (\delta^M =_{e_E \#} \epsilon^M) $$

$$ (\Gamma^w \triangleright^w A^w) \sim \Delta^M \qquad := \sum_{\Gamma^M} (\Gamma^w \sim \Gamma^M) \times \sum_{A^M} (A^w \sim A^M) \times (\Delta^M = \Gamma^M \triangleright^M A^M) $$

$$ (,^w \Delta^w \sigma^w A^w t^w) \sim_{\Gamma^M \Rightarrow E^M} \delta^M \qquad := \sum_{\Delta^M} (\Delta^w \sim \Delta^M) \times \sum_{\sigma^M} (\sigma^w \sim \sigma^M) \times \sum_{A^M} (A^w \sim A^M) \times \sum_{t^M} (t^w \sim t^M) \times (e_E : E^M = \Delta^M \triangleright^M A^M) \times (\delta =_{e_E \#} \sigma^M, t^M) $$

$$ \mathrm{var}^w x^w \sim t^M \qquad := x^w \sim t^M $$

$$ 0^w \Gamma^w A^w \sim_{\Delta^M \vdash B^M} t^M \qquad := \sum_{\Gamma^M} (\Gamma^w \sim \Gamma^M) \times \sum_{A^M} (A^w \sim A^M) \times (e_\Delta : \Delta^M = \Gamma^M \triangleright^M A^M) \times (e_B : B^M =_{e_\Delta \#} \mathrm{wk}^M A^M) \times (t^M =_{e_\Delta, e_B \#} \mathrm{vz}^M) $$

$$ S^w \Gamma^w A^w n^w B^w \sim_{\Delta^M \vdash C^M} t^M \qquad := \sum_{\Gamma^M} (\Gamma^w \sim \Gamma^M) \times \sum_{A^M} (A^w \sim A^M) \times \sum_{B^M} (B^w \sim B^M) \times \sum_{n^M} (n^w \sim n^M) \times (e_\Delta : \Delta^M = \Gamma^M \triangleright^M B^M) \times (e_C : C^M =_{e_\Delta \#} \mathrm{wk}^M A^M) \times (t^M =_{e_\Delta, e_C \#} \mathrm{vs}^M n^M) $$

(2) *Universe*

$$ U^w \Gamma^w A^w \sim A^M \qquad := A^M = U^M $$
$$973 \qquad \mathrm{El}^w \Gamma^w a^w \sim A^M \qquad := \sum_{a^M} (a^w \sim a^M) \times (A^M = \mathrm{El}^M a^M)$$

(3) Inductive parameters

$$974 \qquad \Pi^w \Gamma^w a^w B^w \sim C^M \qquad := \sum_{a^M} (a^w \sim a^M) \times \sum_{B^M} (B^w \sim B^M) \\ \qquad \times (C^M = \Pi^M a^M B^M)$$

$$975 \qquad \mathrm{app}^w \Gamma^w a^w B^w t^w u^w \sim_{\Gamma^M \vdash C^M} x^M := \sum_{a^M} (a^w \sim a^M) \times \sum_{B^M} (B^w \sim B^M) \times \\ 976 \qquad \qquad \qquad \sum_{t^M} (t^w \sim t^M) \times \sum_{u^M} (u^w \sim u^M) \times \\ 977 \qquad \qquad \qquad \qquad (e_C : C^M = B^M [0 := u^M]^M) \times \\ 978 \qquad \qquad \qquad \qquad (x^M =_{e_C \#} t^M {}^@M u^M)$$

(4) Metatheoretic parameters

$$981 \qquad \hat{\Pi}^w T A \Gamma^w A^w \sim B^M \qquad := \sum_{A^M} ((t:T) \rightarrow A^w \sim A^M t) \times (B^M = \hat{\Pi}^M T A^M)$$

$$982 \qquad \mathrm{a\hat{p}}^w T A \Gamma^w A^w t^w u \sim_{\Gamma^M \vdash B^M} x^M := \sum_{A^M} ((t:T) \rightarrow A^w \sim A^M t) \times \sum_{t^M} (t^w \sim t^M) \times \\ 983 \qquad \qquad \qquad (e_B : B^M = \hat{\Pi}^M T A^M) \times (x^M =_{e_B \#} t^M {}^@M u)$$

### 4.2.2 Right Uniqueness

Next, we prove that this relation is right unique. Then, we show that the relation is stable under weakening and substitution. The last step consists of showing left-totality, i.e. giving a related semantic counterpart to any well-typed context, type or term. Everything is proved by induction on the typing judgments.

► **Lemma 46 (Right uniqueness).** *The relation is right unique in the following sense:*

$$992 \qquad \Sigma \sim^p : (\Gamma^w : \Gamma \vdash) \qquad \rightarrow \mathrm{is-prop} \left( \sum_{\Gamma^M} \Gamma^w \sim \Gamma^M \right)$$

$$993 \qquad \Sigma \sim^p : (A^w : \Gamma \vdash A) \qquad \rightarrow \mathrm{is-prop} \left( \sum_{A^M} A^w \sim A^M \right)$$

$$994 \qquad \Sigma \sim^p : (t^w : \Gamma \vdash t \in A) \qquad \rightarrow \mathrm{is-prop} \left( \sum_{t^M} t^w \sim t^M \right)$$

$$995 \qquad \Sigma \sim^p : (x^w : \Gamma \vdash x \in_N A) \qquad \rightarrow \mathrm{is-prop} \left( \sum_{x^M} x^w \sim x^M \right)$$

$$996 \qquad \Sigma \sim^p : (\sigma^w : \Gamma \vdash \sigma \Rightarrow \Delta) \qquad \rightarrow \mathrm{is-prop} \left( \sum_{\sigma^M} \sigma^w \sim \sigma^M \right)$$

► **Remark 47.** We mentioned that in order to avoid a recursive-recursive definition, we removed some hypotheses in the list of arguments of the relation. Such hypotheses are sometimes missed, for example in the case of the empty substitution or in the case of variables, requiring us to state additional equalities. Because of this, we need UIP to show that $\sum_{\Gamma^M} \Gamma \sim \Gamma^M$ and $\sum_{A^M} A \sim A^M$ are propositions. One may think that the use of UIP could be avoided by using the alternative verbose definition that we suggested before, expecting that $\sum_{\Gamma^M} \sum_{A^M} A \sim A^M$, rather than $\sum_{A^M} A \sim A^M$, is a proposition. However, this is not obvious. For example, we were not able to define $\mathrm{El}^w \Gamma^w a^w \sim A^M$ in this fashion.
6:26 For Finitary Induction-Induction, Induction is Enough

In related work, Hugunin investigated constructing IITs without UIP [19] in cubical type theory, and demonstrated that well-formedness predicates used in syntactic algebras can subtly break in that setting. Also, while Hugunin does not use UIP, he only shows the simple version of dependent elimination for the constructed IITs. Hence, the question whether IITs are reducible to inductive types in a UIP-free setting remains open.

4.2.3 Stability under Weakening and Substitution

Stability of the relation under weakening must be proved before stability under substitution. Indeed, in the proof of stability under substitution, the Π case requires to show that Π(A[σ]) (B[keep σ]) is related to Π<sup>M</sup>(A<sup>M</sup>[σ]<sup>M</sup>) (B<sup>M</sup>[keep<sup>M</sup> σ]<sup>M</sup>). We would like to apply the induction hypothesis, so we need to show that keep σ = wk<sub>0</sub> σ ,<sup>P</sup> var<sup>P</sup> 0 is related to keep<sup>M</sup> σ<sup>M</sup>, knowing that σ is related to σ<sup>M</sup>. As keep σ = wk<sub>0</sub> σ ,<sup>P</sup> var<sup>P</sup> 0, we are left with showing that wk<sub>0</sub> σ = σ ◦ wk (where wk = wk<sub>0</sub> id) relates to its semantic counterpart.

To achieve that, we show that wk<sub>0</sub> preserves the relation, for types and terms. This requires to generalise a bit and show that wk<sub>n</sub> preserves the relation, as wk<sub>0</sub> (ΠA B) = Π(wk<sub>0</sub> A) (wk<sub>1</sub> B). But remember that wk<sub>n</sub> performs a weakening in the middle of a context, so we first define the semantic counterpart of this:

$$
\begin{align*}
\Sigma \mathrm{wk}_0 \Rightarrow^M : (\Gamma^w : \Gamma \vdash) &\to (\Gamma^w \sim \Gamma^M) \to \\
&\to (\Delta^w : \Gamma; \Delta \vdash) \to (\Delta^w \sim \Delta^M) \to \\
&\to (A^M : \mathrm{Ty}^M \Gamma^M) \to (\Delta'^M : \mathrm{Con}^M) \times (\mathrm{Sub}^M \Delta'^M \Delta^M)
\end{align*}
$$

Here, Δ'M should be thought of as the context ΔM where the weakening has happened in the middle of the context, by inserting the type A'M after the prefix ΓM. Indeed, we expect that ΓM is a prefix of ΔM, as ΓM relates to Γ and ΔM to Γ; Δ. The substitution from the weakened context to the original one must be computed at the same time otherwise the induction hypothesis is not strong enough. Then, we separate the two components under the same (implicit) hypotheses:

$$
\begin{align*}
\mathit{wk}_0^M A^M \Delta^M & : \mathit{Con}^M \\
\mathit{wk} \Rightarrow^M A^M \Delta^M & : \mathit{Sub}^M (\mathit{wk}_0^M A^M \Delta^M) \Delta^M
\end{align*}
$$

Note that if recursion-recursion is available in the metatheory, wk<sub>0</sub><sup>M</sup> and wk<sup>⇒M</sup> can be
defined directly without introducing this intermediate Σwk<sub>0</sub> ⇒<sup>M</sup>.

► **Lemma 48** (Weakening preserves typing). *The following statements are all under the hypotheses* (Γ<sup>w</sup> : Γ ⊢), (Γ<sup>w</sup> ∼ Γ<sup>M</sup>), (Δ<sup>w</sup> : Γ; Δ ⊢), (Δ<sup>w</sup> ∼ Δ<sup>M</sup>), (A<sup>w</sup> : Γ ⊢ A), and (A<sup>w</sup> ∼ A<sup>M</sup>).

$$
\begin{align*}
\text{wk}_0 \sim & : \text{wk}_0^w A^w \Delta^w \sim \text{wk}_0^M A^M \Delta^M \\
\text{wk} \sim & : (T^w : \Gamma; \Delta \vdash T) \rightarrow (T^w \sim T^M) \rightarrow \text{wk}^w A^w T^w \sim T^M [\text{wk}_0 \Rightarrow^M A^M \Delta^M]^M \\
\text{wk} \sim & : (t^w : \Gamma; \Delta \vdash t \in T) \rightarrow (t^w \sim t^M) \rightarrow \text{wk}^w A^w t^w \sim t^M [\text{wk}_0 \Rightarrow^M A^M \Delta^M]^M \\
\text{wk} \sim & : (x^w : \Gamma; \Delta \vdash t \in_N T) \rightarrow (x^w \sim x^M) \rightarrow \text{wk}^w A^w x^w \sim x^M [\text{wk}_0 \Rightarrow^M A^M \Delta^M]^M
\end{align*}
$$

Proof. By mutual induction on the typing judgments.

<figure><img src="image_7.png" /></figure>

► Lemma 49 (Weakening of substitution preserves - ∼ -).

$$
\begin{align*}
\text{wk}_0 \sim & : (\Gamma^w : \Gamma \vdash) \to (\Gamma^w \sim \Gamma^M) \to (A^w : \Gamma \vdash A) \to (A^w \sim A^M) \to \\
& \qquad (\sigma^w : \Gamma \vdash \sigma \Rightarrow \Delta) \to (\sigma^w \sim \sigma^M) \to (\text{wk}_0^w A^w \sigma^w \sim \sigma^M \circ_M \text{wk}^M)
\end{align*}
$$
**Proof.** By induction on the typing judgments.

Next, we want to prove that given any well-typed substitution $\sigma : \text{Sub} \Gamma \Delta$ and semantic contexts $\Gamma^M$ and $\Delta^M$, related to $\Gamma$ and $\Delta$, respectively, there is a semantic substitution related to $\sigma$. In the extension case $\Gamma \vdash \sigma, \Gamma^P \Rightarrow \Delta \triangleright \Gamma^P A$, the induction hypothesis provides $\sigma^M, \Delta^M, A^M$ related to their syntactic counterpart. However, the premises of the induction hypothesis for getting a relevant $t^M$ require showing that the type $A^M[\sigma^M]^M$ is related to the syntactic type $A[\sigma]$.

**Lemma 50 (Preservation of the relation by substitution for variables).**

$$ \begin{align*} \llbracket \sigma^w : \Gamma \vdash \sigma \Rightarrow \Delta \rrbracket \to (\sigma^w \sim \sigma^M) \to (x^w : \Delta \vdash x \in_N A) \to (x^w \sim x^M) \to \\ \llbracket x^w \sigma^w \sim x^M[\sigma^M]^M \rrbracket \end{align*} $$

**Proof.** Induction on typing.

**Lemma 51 (Preservation of the relation by substitution for types and terms).** We assume $(\sigma^w : \Gamma \vdash \sigma \Rightarrow \Delta)$, $(\sigma^w \sim \sigma^M)$, $(\Gamma^w : \Gamma \vdash)$, $(\Gamma^w \sim \Gamma^M)$, $(\Delta^w : \Delta \vdash)$, and $(\Delta^w \sim \Delta^M)$:

$$ \llbracket \sigma^w : \Delta \vdash A \rrbracket \to (A^w \sim A^M) \to \llbracket \Gamma^w \sigma^w \sim A^M[\sigma^M]^M \rrbracket $$

$$ \llbracket t^w : \Delta \vdash t \in A \rrbracket \to (t^w \sim t^M) \to \llbracket \Gamma^w t^w \sigma^w \sim t^M[\sigma^M]^M \rrbracket $$

**Proof.** Mutual induction on typing.

**Lemma 52 (The relation is preserved by composition and identity).** We have the same hypotheses as in the previous lemma.

$$ \begin{align*} \circ \sim & : (E^w : E \vdash) \to (E^w \sim E^M) \to (\delta^w : \Delta \vdash \delta \Rightarrow E) \to (\delta^w \sim \delta^M) \to \\ & \circ^w \Gamma^w \delta^w \sigma^w \sim \delta^M \circ^M \sigma^M \end{align*} $$

$$ \text{id} \sim : (\Gamma^w : \Gamma \vdash) \to (\Gamma^w \sim \Gamma^M) \to \text{id}^w \Gamma^w \sim \text{id}_{\Gamma^M} $$

### 4.2.4 Left-Totality and the Recursor

Before defining the cursor $\llbracket - \rrbracket$, we show left totality of the relation: that is, the image of a syntactic context is a unique semantic context which is related to it, and similarly for types and terms.

**Lemma 53 (Left totality of $\sim \sim$).**

$$ \Sigma \text{Con} \sim : (\Gamma^w : \Gamma \vdash) \to \sum_{\Gamma^M} \Gamma^w \sim \Gamma^M $$

$$ \Sigma \text{Ty} \sim : (\Gamma^w : \Gamma \vdash) \to (\Gamma^w \sim \Gamma^M) \to (A^w : \Gamma \vdash A) \to (A^M : \text{Ty}^M \Gamma^M) \times (A^w \sim A^M) $$

$$ \begin{align*} \Sigma \text{Tm} \sim : (\Gamma^w : \Gamma \vdash) \to (\Gamma^w \sim \Gamma^M) \to (A^w : \Gamma \vdash A) \to (A^w \sim A^M) \to \\ (t^w : \Gamma \vdash t \in A) \to (t^M : \text{Tm}^M \Gamma^M A^M) \times (t^w \sim t^M) \end{align*} $$

$$ \begin{align*} \Sigma \text{Var} \sim : (\Gamma^w : \Gamma \vdash) \to (\Gamma^w \sim \Gamma^M) \to (A^w : \Gamma \vdash A) \to (A^w \sim A^M) \to \\ (x^w : \Gamma \vdash x \in_N A) \to (x^M : \text{Tm}^M \Gamma^M A^M) \times (x^w \sim x^M) \end{align*} $$

$$ \begin{align*} \Sigma \text{Sub} \sim : (\Gamma^w : \Gamma \vdash) \to (\Gamma^w \sim \Gamma^M) \to (\Delta^w : \Delta \vdash) \to (\Delta^w \sim \Delta^M) \to \\ (\sigma^w : \Gamma \vdash \sigma \Rightarrow \Delta) \to (\sigma^M : \text{Sub}^M \Gamma^M \Delta^M) \times (\sigma^w \sim \sigma^M) \end{align*} $$
6:28 For Finitary Induction-Induction, Induction is Enough

1085
1086

**Proof.** By induction on well-formedness judgments. The right uniqueness of the relation is used in this induction. ◀

1087
1088

► **Lemma 54** (Existence of the recursor). *For any $M$: SignAlg there is a $[\llcorner - \rrcorner]$ : SignMor $| M$ where $|$ is given in Definition 43.*

1089
1090

**Proof.** Using the first projections in the construction of the left-totality construction and right uniqueness. ◀

1091

4.3 Uniqueness

1092
1093
1094

It remains to show that the morphism constructed in Lemma 54 is unique. We exploit right uniqueness of the relation: it is enough to show that any such morphism maps a syntactic context to a related semantic context, and similarly for types and terms.

1095
1096

► **Lemma 55.** *We assume an arbitrary signature morphism $f$ from $|\rightarrow$ to $M$. This induces the following maps:*

1097

$\mathrm{Con}^f : (\Gamma \vdash) \rightarrow \mathrm{Con}^M$

1098

$\mathrm{Ty}^f : (\Gamma^w : \Gamma \vdash) \rightarrow (\Gamma \vdash A) \rightarrow \mathrm{Ty}^M (\mathrm{Con}^f \Gamma^w)$

1099

$\mathrm{Tm}^f : (\Gamma^w : \Gamma \vdash) \rightarrow (A^w : \Gamma \vdash A) \rightarrow (\Gamma \vdash t \in A) \rightarrow \mathrm{Tm}^M (\mathrm{Con}^f \Gamma^w) (\mathrm{Ty}^f \Gamma^w A^w)$

1100

$\mathrm{Var}^f : (\Gamma^w : \Gamma \vdash) \rightarrow (A^w : \Gamma \vdash A) \rightarrow (\Gamma \vdash x \in_N A) \rightarrow \mathrm{Tm}^M (\mathrm{Con}^f \Gamma^w) (\mathrm{Ty}^f \Gamma^w A^w)$

1101
1102

$\mathrm{Sub}^f : (\Gamma^w : \Gamma \vdash) \rightarrow (\Delta^w : \Delta \vdash) \rightarrow (\Gamma \vdash \sigma \Rightarrow \Delta) \rightarrow \mathrm{Sub}^M (\mathrm{Con}^f \Gamma^w) (\mathrm{Con}^f \Delta^w)$

1103

*The images of the above maps are related by $- \sim -$:*

1104

$\sim \mathrm{Con}^f : (\Gamma^w : \Gamma \vdash) \rightarrow \Gamma^w \sim \mathrm{Con}^f \Gamma^w$

1105

$\sim \mathrm{Ty}^f : (\Gamma^w : \Gamma \vdash) \rightarrow (A^w : \Gamma \vdash A) \rightarrow \Gamma^w \sim \mathrm{Ty}^f \Gamma^w A^w$

1106

$\sim \mathrm{Tm}^f : (\Gamma^w : \Gamma \vdash) \rightarrow (A^w : \Gamma \vdash A) \rightarrow (t^w : \Gamma \vdash t \in A) \rightarrow \Gamma^w \sim \mathrm{Tm}^f \Gamma^w A^w t^w$

1107

$\sim \mathrm{Var}^f : (\Gamma^w : \Gamma \vdash) \rightarrow (A^w : \Gamma \vdash A) \rightarrow (x^w : \Gamma \vdash x \in_N A) \rightarrow \Gamma^w \sim \mathrm{Var}^f \Gamma^w A^w x^w$

1108
1109

$\sim \mathrm{Sub}^f : (\Gamma^w : \Gamma \vdash) \rightarrow (\Delta^w : \Delta \vdash) \rightarrow (\sigma^w : \Gamma \vdash \sigma \Rightarrow \Delta) \rightarrow \Gamma^w \sim \mathrm{Sub}^f \Gamma^w \Delta^w \sigma^w$

1110

**Proof.** By induction on typing relations. ◀

1111
1112

► **Corollary 56** (Uniqueness of the recursor). *By right uniqueness of $- \sim -$, there is only one morphism $\mathrm{SignMor}|M$ for any $M$.*

1113
1114

► **Theorem 57.** *If a model of ETT supports indexed W-types, it supports the theory of IIT signatures.*

1115
1116

**Proof.** We define the syntax $|\rightarrow$ by Definition 43 which only used indexed W-types, the recursor by Lemma 54 and we prove its uniqueness property by Corollary 56. ◀

1117

► **Corollary 58.** *If a model of ETT supports indexed W-types, it supports all IITs.*

1118

**Proof.** Combining Theorem 57 and Theorem 23. ◀
# 5 Further Work

The current work only concerns finitary IITs. An extension would be to also allow infinitely branching inductive types such as W-types. This would first require giving semantics for infinitary IITs and adapting the term model construction. These would be straightforward following [24]. However, it seems to be more difficult to construct the syntax of infinitary IIT signatures without using quotients. The reason is that such syntax would not be strictly restricted to neutral terms: the term model construction for infinitary IITs requires λ-abstraction and βη-rules for infinitary Π types. A definition of normal preterms and typing judgments on them may still be possible, but it appears to be much more complicated than before (the current authors have attempted this without conclusive success).

As mentioned in Section 4.2.2, it also remains an open problem whether IITs are reducible to inductive types in a UIP-free setting. To show this, we would need to construct the syntax of signatures without UIP, and also reproduce the semantics and term model construction for IITs without UIP.

# References

1. Benedikt Ahrens, Ralph Matthes, and Anders Mörtberg. From signatures to monads in unimath. *Journal of Automated Reasoning*, 63(2):285–318, Aug 2019. doi:10.1007/s10817-018-9474-4.

2. Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, and Fredrik Nordvall Forsberg. Quotient inductive-inductive types. In Christel Baier and Ugo Dal Lago, editors, *Foundations of Software Science and Computation Structures*, pages 293–310, Cham, 2018. Springer International Publishing.

3. Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride, and Peter Morris. Indexed containers. *J. Funct. Program.*, 25, 2015. URL: http://dx.doi.org/10.1017/S095679681500009X, doi:10.1017/S095679681500009X.

4. Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. In Rastislav Bodik and Rupak Majumdar, editors, *Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016*, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 18–29. ACM, 2016. URL: http://doi.acm.org/10.1145/2837614.2837638, doi:10.1145/2837614.2837638.

5. Thorsten Altenkirch, Ambrus Kaposi, András Kovács, and Jakob von Raumer. Constructing inductive-inductive types via type erasure. In Marc Bezem, editor, *25th International Conference on Types for Proofs and Programs, TYPES 2019*. Centre for Advanced Study at the Norwegian Academy of Science and Letters, 2019.

6. Thorsten Altenkirch, Nuo Li, and Ondřej Rypáček. Some constructions on Ω-groupoids. In *Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice*, LFMTP '14, pages 4:1–4:8, New York, NY, USA, 2014. ACM. URL: http://doi.acm.org/10.1145/2631172.2631176, doi:10.1145/2631172.2631176.

7. Robert Atkey, Neil Ghani, and Patricia Johann. A relationally parametric model of dependent type theory. In *Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, POPL '14, page 503–515, New York, NY, USA, 2014. Association for Computing Machinery. doi:10.1145/2535838.2535852.

8. Steve Awodey, Jonas Frey, and Sam Speight. Impredicative encodings of (higher) inductive types. In Anuj Dawar and Erich Grädel, editors, *Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018*, Oxford, UK, July 09-12, 2018, pages 76–85. ACM, 2018. doi:10.1145/3209108.3209130.

9. Andrej Bauer, Philipp G. Haselwarter, and Théo Winterhalter. A modular formalization of type theory in Coq. In Ambrus Kaposi, editor, *23rd International Conference on Types for Proofs and Programs, TYPES 2017*. Eötvös Loránd University, 2017.
6:30 For Finitary Induction-Induction, Induction is Enough

1167 10 Guillaume Brunerie. A formalization of the initiality conjecture in agda. Slides of a talk at the Homotopy Type Theory 2019 Conference, Carnegie Mellon University, Pittsburgh, Pennsylvania, August 2019. URL: https://guillaumebrunerie.github.io/pdf/initiality.pdf.

1171 11 Paolo Capriotti. Notions of type formers. In Ambrus Kaposi, editor, *23rd International Conference on Types for Proofs and Programs, TYPES 2017*. Eötvös Loránd University, 2017.

1172 12 John Cartmell. Generalised algebraic theories and contextual categories. *Annals of Pure and Applied Logic*, 32:209–243, 1986.

1175 13 James Chapman. Type theory should eat itself. *Electronic Notes in Theoretical Computer Science*, 228:21–36, January 2009. URL: http://dx.doi.org/10.1016/j.entcs.2008.12.114, doi:10.1016/j.entcs.2008.12.114.

1178 14 Jesper Cockx and Andreas Abel. Sprinkles of extensionality for your vanilla type theory. In Silvia Ghilezan and Ivetić Jelena, editors, *22nd International Conference on Types for Proofs and Programs, TYPES 2016*. University of Novi Sad, 2016.

1181 15 Nils Anders Danielsson. A formalisation of a dependently typed language as an inductive-recursive family. In Thorsten Altenkirch and Conor McBride, editors, *TYPES*, volume 4502 of *Lecture Notes in Computer Science*, pages 93–109. Springer, 2006.

1184 16 Peter Dybjer. Internal type theory. In *Lecture Notes in Computer Science*, pages 120–134. Springer, 1996.

1186 17 Peter Dybjer and Anton Setzer. A finite axiomatization of inductive-recursive definitions. In *Typed Lambda Calculi and Applications*, volume 1581 of *Lecture Notes in Computer Science*, pages 129–146. Springer, 1999.

1189 18 Martin Hofmann. Syntax and semantics of dependent types. In *Semantics and Logics of Computation*, pages 79–130. Cambridge University Press, 1997.

1191 19 Jasper Hugunin. Constructing inductive-inductive types in cubical type theory. In Mikołaj Bojańczyk and Alex Simpson, editors, *Foundations of Software Science and Computation Structures*, pages 295–312, Cham, 2019. Springer International Publishing.

1194 20 Ambrus Kaposi. Re: separate definition of constructors? Email to the Agda mailing list, May 2019. URL: https://lists.chalmers.se/pipermail/agda/2019/011176.html.

1196 21 Ambrus Kaposi, András Kovács, and Thorsten Altenkirch. Constructing quotient inductive-inductive types. *Proc. ACM Program. Lang.*, 3(POPL):2:1–2:24, January 2019. doi:10.1145/3290315.

1199 22 Ambrus Kaposi, András Kovács, and Ambroise Lafont. Closed inductive-inductive types are reducible to indexed inductive types. In Marc Bezem, editor, *25th International Conference on Types for Proofs and Programs, TYPES 2019*. Centre for Advanced Study at the Norwegian Academy of Science and Letters, 2019.

1203 23 Ambrus Kaposi and Jakob von Raumer. A syntax for mutual inductive families. In *5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)*, 2020. To appear.

1206 24 András Kovács and Ambrus Kaposi. Large and infinitary quotient inductive-inductive types. In *35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020, Saarbrücken, Germany, July 8-11, 2020*, 2020. To appear.

1209 25 Lorenzo Malatesta, Thorsten Altenkirch, Neil Ghani, Peter Hancock, and Conor McBride. Small induction recursion, indexed containers and dependent polynomials are equivalent, 2013. TLCA 2013.

1212 26 Fredrik Nordvall Forsberg. *Inductive-inductive definitions*. PhD thesis, Swansea University, 2013.

1214 27 Fredrik Nordvall Forsberg and Anton Setzer. Inductive-inductive definitions. In Anuj Dawar and Helmut Veith, editors, *CSL 2010*, volume 6247 of *Lecture Notes in Computer Science*, pages 454–468. Springer, Heidelberg, 2010.

1217 28 Ulf Norell. *Towards a practical programming language based on dependent type theory*. PhD thesis, Chalmers University of Technology, 2007.
1219

29 The Univalent Foundations Program. Homotopy type theory: Univalent foundations of mathematics. Technical report, Institute for Advanced Study, 2013.

1220

1221

30 Thomas Streicher. *Semantics of Type Theory: Correctness, Completeness, and Independence Results*. Birkhauser Boston Inc., Cambridge, MA, USA, 1991.

1222