1111/1111.0123.md

PROOF-IRRELEVANT MODEL OF CC WITH PREDICATIVE INDUCTION AND JUDGMENTAL EQUALITY

GYESIK LEE^a AND BENJAMIN WERNER^b

^a Hankyong National University, Anseong-si, Kyonggi-do, Korea
e-mail address: gslee@hknuc.ac.kr

^b INRIA Saclay and LIX, Ecole Polytechnique, 91128 Palaiseau Cedex, France
e-mail address: Benjamin.Werner@inria.fr

---

ABSTRACT. We present a set-theoretic, proof-irrelevant model for Calculus of Constructions (CC) with predicative induction and judgmental equality in Zermelo-Fraenkel set theory with an axiom for countably many inaccessible cardinals. We use Aczel’s trace encoding which is universally defined for any function type, regardless of being impredicative. Direct and concrete interpretations of simultaneous induction and mutually recursive functions are also provided by extending Dybjer’s interpretations on the basis of Aczel’s rule sets. Our model can be regarded as a higher-order generalization of the truth-table methods. We provide a relatively simple consistency proof of type theory, which can be used as the basis for a theorem prover.

1. INTRODUCTION

Informal motivation. The types-as-sets interpretation of type theory in a sufficiently strong classical axiomatic set theory, such as the Zermelo-Fraenkel (ZF) set theory, has been regarded as the most straightforward approach to demonstrating the consistency of type theory (cf. [Aczel(1998)] and [Coquand(1990)]). It can be construed as a higher-order generalization of the truth-table methods. Such a model captures the intuitive meaning of the constructs: the product, $\lambda$ -abstraction, and application correspond to the ordinary set-theoretic product, function, and application, respectively.

A straightforward model of type theory is very useful for establishing the consistency of type theory, and it can be used to determine the proof-theoretic strength of type theory (cf. [Aczel(1998), Dybjer(1991), Dybjer(2000), Werner(1997)]). However, a higher-order generalization of the trivial Boolean model is not so simple (cf. [Miquel and Werner(2003)]). The main cause of this problem, as identified by [Reynolds(1984)], is the fact that type systems

---

1998 ACM Subject Classification: F.4.1, F.3.1.

Key words and phrases: Calculus of Constructions, judgmental equality, proof-irrelevance, consistency.

^a Corresponding author: For Gyesik Lee, this work was partly supported by Mid-career Researcher Program through NRF funded by the MEST (2010-0022061).containing Girard-Reynolds' second-order calculus cannot have the usual set-theoretic interpretation of types. The only way to provide a set-theoretic meaning for an impredicative proposition type is to identify all the proof terms of that proposition type: Proposition types are interpreted either by the empty set or a singleton with a canonical element. Thus, proof-irrelevant models are necessary for interpreting reasonable higher-order type systems.

Set-theoretic models of type theory can be understood in a straightforward manner. [Werner(2008)] showed that they can be used as the basis of proof assistants in programming with dependent types. This is because they provide a mechanism to distinguish between computational and logical parts. Werner's system is a proof-irrelevant version of Luo's Extended Calculus of Constructions (ECC; [Luo(1989)]), and the set-theoretic model is an extension of that of Calculus of Constructions (CC) defined by [Miquel and Werner(2003)].

Luo's ECC is a Martin-Löf-style extension of CC, with strong sum types and a fully cumulative type hierarchy. At the lowest level, there is an impredicative type $\mathbf{Prop}$ of propositions. This is followed by a hierarchy of predicative type universes $\mathbf{Type}_i$ , $i = 0, 1, 2, \dots$ :

• • $\mathbf{Prop}$ is of type $\mathbf{Type}_0$ ;
• • $\mathbf{Type}i$ is of type $\mathbf{Type}{i+1}$ ;
• • $\mathbf{Prop} \prec \mathbf{Type}_0 \prec \mathbf{Type}_1 \prec \dots$ .

Werner's system, however, does not include the subtyping rule $\mathbf{Prop} \prec \mathbf{Type}_0$ , which could complicate the model construction, as identified by [Miquel and Werner(2003)]. Their model constructions cannot be extended to ECC. We will explain this in detail in Remark 3.1.

In this paper, we investigate the inclusion of $\mathbf{Prop} \prec \mathbf{Type}_0$ , and we show that type theory with judgmental equality, à la [Martin-Löf(1984)], can have a simple proof-irrelevant model. We expect our results to play a key role in the theoretical justification of proof systems based on Martin-Löf-style type theory.

Overview of the work. Martin-Löf type theory and Logical Framework include typing rules for the equality of objects and types:

$$\mathrm{\Gamma }⊢M=N:A\text{and}\frac{\mathrm{\Gamma }⊢M:A\mathrm{\Gamma }⊢A=B}{\mathrm{\Gamma }⊢M:B}(conv)\backslash Gamma\; \backslash vdash\; M\; =\; N\; :\; A\; \backslash quad\; \backslash text\{and\}\; \backslash quad\; \backslash frac\{\backslash Gamma\; \backslash vdash\; M\; :\; A\; \backslash quad\; \backslash Gamma\; \backslash vdash\; A\; =\; B\}\{\backslash Gamma\; \backslash vdash\; M\; :\; B\}\; \backslash quad\; (conv)$$

In particular, Barendregt's PTS-style $\beta$ -conversion side condition turns into an explicit judgment. Two objects are not just equal; they are equal with respect to a type (cf. [Nordström et al.(1990) Nordström, Petersson, and Smith, Goguen(1994), Aczel(1998)]).

The type system considered in our study is CC with predicative induction and judgmental equality. It is a type system with the following features: dependent types, impredicative type ( $\mathbf{Prop}$ ) of propositions, a cumulative hierarchy of predicative universes ( $\mathbf{Type}_i$ ), predicative inductions, and judgmental equality.

The main difficulty in the construction of a set-theoretic model of our system stems from the impredicativity of $\mathbf{Prop}$ and the subtyping property $\mathbf{Prop} \prec \mathbf{Type}_0$ . Without subtyping, one could use the solution provided by [Miquel and Werner(2003)] and [Werner(2008)], whereby proof-terms are syntactically distinguished from other function terms. Thus, the problem lies in the case distinction between the impredicative type $\mathbf{Prop}$ and the predicative types $\mathbf{Type}_i$ , whereas the subsumption eliminates the difference. An interpretation function $f : {0, 1} \rightarrow \mathcal{V}$ is required, where $\mathcal{V}$ is a set universe, that is different from the identity function. See Section 3 for further details.For a set-theoretic interpretation of the cumulative type universes and predicative inductions, it is sufficient to assume countably many (strongly) inaccessible cardinals. [Werner(1997)] showed that ZF with an axiom guaranteeing the existence of infinitely many inaccessible cardinals is a good candidate. However, it is not clear whether the inaccessible cardinal axiom is necessary for our construction. The required feature of an inaccessible cardinal $\kappa$ is the closure property of the universe $\mathcal{V}_\kappa$ under the powerset operation. This is a necessary condition for the interpretation of inductive types. Following [Dybjer(1991)], we use Aczel's rule sets to obtain a direct and concrete interpretation of induction and recursion rules.

The remainder of this paper is organized as follows. In Section 2, we provide a formal presentation of CC with predicative induction and judgmental equality. Examples are presented to enable the reader to understand the syntax and typing rules. This section can be regarded as an introduction to the base theory of the proof assistant Coq. Indeed, the syntax we have provided is as close to Coq syntax as that used in practice, except for the judgmental equality and the restriction on predicative inductions.¹

The difficulties in providing set-theoretic interpretations of impredicative or polymorphic types, subtypes, etc., are discussed in Section 3. We use the computational information about the domains saved in the interpretation of $a : A$ to avoid these difficulties. This means that for the construction of set-theoretic models, type systems with judgmental equality are more explicit than systems without it. Using some typical examples, we explain the construction of a set-theoretic interpretation of inductive types and recursive functions.

Finally, in Section 4, we prove the soundness of our interpretation. The proof itself is relatively simple, and it can also be used to verify the consistency of our system. This is because some types such as $\Pi(\alpha : \mathbf{Prop}).\alpha$ will be interpreted as the empty set; hence, they cannot be inhabited in the type system.

In Section 5, we summarize the main results, and we discuss related work for future investigation.

2. FORMAL PRESENTATION OF CC WITH JUDGMENTAL EQUALITY

First, we provide the full presentation of the system, i.e., Coquand's CC with judgmental equality and predicative induction over infinitely many cumulative universes.

2.1. Syntax. We assume an infinite set of countably many variables, and we let $x, x_i, X, X_i, \dots$ vary over the variables. We also use special constants $\mathbf{Prop}$ and $\mathbf{Type}_i$ , $i \in \mathbb{N}$ . They are called sorts. Sorts are usually denoted by $s, s_i$ , etc.²

---

¹We remark that many impredicative inductive types can be coded by impredicative definitions (cf. [Girard et al.(1989)Girard, Taylor, and Lafont, Coquand(1990), Werner(1997)]).

²In this paper, we do not consider the sort $\mathbf{Set}$ . Indeed, when (the impredicative or predicative sort) $\mathbf{Set}$ is placed at the lowest level in the hierarchy of sorts, as in the case of the current development of Coq, there is no way to provide a universal set-theoretic interpretation of both $\mathbf{Set}$ and $\mathbf{Prop}$ , as identified by [Reynolds(1984)]. Note, however, that $\mathbf{Type}_0$ in our system plays the role of the predicative $\mathbf{Set}$ .Definition 2.1 (Terms and contexts). The syntax of the objects is given as follows.

Here, $[]$ denotes the empty sequence.

Definition 2.2 (Atomic terms). Atomic terms are either variables, sorts, or terms of the form $\mathbf{Ind}_n{\Delta_I := \Delta_C} \cdot x$ .

Definition 2.3 (Domain of contexts). The domain of a context is defined as follows:

Remark 2.4.

(1) Vector notations are used instead of some sequences of expressions:

• $\backslash vec\{t\}\; :=\; t\_1,\; \backslash dots,\; t\_n$ • $\backslash Pi\; \backslash vec\{x\}\; :\; \backslash vec\{A\}.t\; :=\; \backslash Pi\; x\_1\; :\; A\_1.\; \backslash dots\; \backslash Pi\; x\_n\; :\; A\_n.\; t$ • $\backslash frac\{\}\{x/k\; :\; A\; :=\; t\}\; :=\; x\_0/k\_0\; :\; A\_0\; :=\; t\_0,\; \backslash dots,\; x\_n/k\_n\; :\; A\_n\; :=\; t\_n$

• $f\; \backslash vec\{t\}\; :=\; f\; t\_1\; \backslash dots\; t\_n$ • $\backslash lambda\; \backslash vec\{x\}\; :\; \backslash vec\{A\}.t\; :=\; \backslash lambda\; x\_1\; :\; A\_1.\; \backslash dots\; \backslash lambda\; x\_n\; :\; A\_n.\; t$

(2) Note that we use two subscript styles. One is of the form $t_1, \dots, t_n$ , and the other is of the form $t_0, \dots, t_n$ , where $n$ is a natural number. The latter style will be used only in the definition of mutually recursive functions, i.e., in combination with fix.

(3) Given a sequence $\vec{\ell}$ , let $lh(\vec{\ell})$ denote its length.

(4) In the examples presented below, character strings are used instead of single character variables in order to emphasize the correspondence with real Coq-expressions.

(5) Given a declaration $\Delta$ and a variable $x$ , let $\Delta(x) = A$ when $A$ is the only term such that $x : A$ occurs in $\Delta$ .

(6) There are standard definitions of the sets of free variables in a context or a term, and of the substitution $t[x \setminus u]$ , where $t, u$ are terms and $x$ a variable. Formal definitions are given in Appendix A.

(7) Given a sequence $\delta = x_1 : t_1, \dots, x_n : t_n$ and a term $t$ , let $t{\delta} := t[x_1 \setminus t_1] \dots [x_n \setminus t_n]$ denote consecutive substitution. On the other hand, the simultaneous substitution of terms $t_1, \dots, t_n$ for $x_1, \dots, x_n$ , respectively, in $t$ is denoted by $t[\delta] := t[x_1 \setminus t_1, \dots, x_n \setminus t_n]$ .

To enable the reader to understand the intended meaning of terms and contexts, we explain some notations with examples. The examples will also be used in Section 3 to explain our model.

Remark 2.5. The expression $\mathbf{Ind}_n{\Delta_I := \Delta_C}$ denotes a (mutually) inductive type, and the subscript $n$ denotes the number of parameters. $\Delta_I$ and $\Delta_C$ are two declarations containing inductive types and their constructors, respectively. The Parameters are binders shared by all the constructors of the definition, and they are used to construct polymorphic types. Theparameters differ from other non-parametric binders in that the conclusion of each type of constructor invokes the inductive type with the same parameter values as its specification. We refer to Lemma 3.8 and Lemma 3.9, which show the difference between parameters and non-parametric binders.

The mutual definition of trees and forests can be represented, for instance, by $\mathcal{D}_{TF} = \mathbf{Ind}_1{\Delta_I := \Delta_C}$ , where

The subscript 1 implies that $(A : \text{Type})$ is a parameter.

Remark 2.6. If $\mathcal{D} = \mathbf{Ind}_n{\Delta_I := \Delta_C}$ and $x \in \text{dom}(\Delta_I, \Delta_C)$ , then $\mathcal{D} \cdot x$ corresponds to the names of defined inductive types or their constructors.

The type for natural numbers and its two constructors can be represented by $\mathcal{D}_N \cdot \text{nat}$ , $\mathcal{D}_N \cdot 0$ , and $\mathcal{D}_N \cdot \text{S}$ , respectively, where $\mathcal{D}_N = \mathbf{Ind}_0{\Delta_I := \Delta_C}$ , $\Delta_I = \text{nat} : \text{Type}_0$ , and $\Delta_C = 0 : \text{nat}, \text{S} : \text{nat} \rightarrow \text{nat}$ .

In the examples presented below, however, we use character strings for better readability. Thus, for example, nat, 0, and S are used instead of $\mathcal{D}_N \cdot \text{nat}$ , $\mathcal{D}_N \cdot 0$ , and $\mathcal{D}_N \cdot \text{S}$ , respectively.

Remark 2.7 (case and fix). The term case( $e, Q, \vec{h}$ ) corresponds to the following Coq-expression

$$\text{match }e\text{ as }y\text{ in }I\vec{u}\text{ return }Q\vec{u}y\text{ with }\cdots \mid C_i\vec{p}\vec{v}\Rightarrow h_i\mid \dots \text{ end}\backslash text\{match\; \}\; e\; \backslash text\{\; as\; \}\; y\; \backslash text\{\; in\; \}\; I\; \backslash vec\{u\}\; \backslash text\{\; return\; \}\; Q\; \backslash vec\{u\}\; y\; \backslash text\{\; with\; \}\; \backslash dots\; \backslash mid\; C\_i\; \backslash vec\{p\}\; \backslash vec\{v\}\; \backslash Rightarrow\; h\_i\; \backslash mid\; \backslash dots\; \backslash text\{\; end\}$$

where

• • the term $e$ is of an inductive type $I \vec{p} \vec{u}$ for some terms $\vec{p}, \vec{u}$ ,
• • $lh(\vec{p}) = lh(\vec{u})$ ,
• • $Q = \lambda \vec{u} : \vec{U}. \lambda y : I \vec{p} \vec{u}. Q'$ for some terms $\vec{U}, Q'$ ,
• • the term $y$ is a fresh variable bound in $Q \vec{u} y$ ,
• • each $C_i$ is a constructor of type $\Pi \vec{p} : \vec{P}. \Pi \vec{v} : \vec{V}_i. I \vec{p} \vec{w}_i$ for some terms $\vec{P}, \vec{V}_i, \vec{w}_i$ , and
• • each $h_i = \lambda \vec{v} : \vec{V}_i. h'_i$ for some term $h'_i$ .

The term $\mathbf{fix} f_i {f/k : A := t}$ denotes the $(i + 1)$ th function defined by a mutual recursion. The number $k_i$ denotes the position of the inductive binder on which recursion is performed for $f_i$ . It corresponds to Coq's struct annotation used for the “guarded” condition in the termination check (cf. [Giménez(1995)]).

(1) The addition function plus can be defined as follows:

$$\text{plus}=\mathbf{f}\mathbf{i}\mathbf{x}f\{f\mathrm{/}1:\mathrm{\Pi }(m,n:\text{nat})\mathrm{.}\text{nat}:=\lambda (m,n:\text{nat})\mathrm{.}\text{case}(n,Q,h_0,h_1)\},\backslash text\{plus\}\; =\; \backslash mathbf\{fix\}\; f\; \backslash \{f/1\; :\; \backslash Pi(m,\; n\; :\; \backslash text\{nat\}).\; \backslash text\{nat\}\; :=\; \backslash lambda(m,\; n\; :\; \backslash text\{nat\}).\; \backslash text\{case\}(n,\; Q,\; h\_0,\; h\_1)\backslash \},$$

where $Q = \lambda(\ell : \text{nat}). \text{nat}$ , $h_0 = m$ , and $h_1 = \lambda(p : \text{nat}). \text{S}(f m p)$ .(2) The functions for measuring the size of trees and forests can be represented by $\text{Tsize} = \text{fix } g_0 {R}$ and $\text{Fsize} = \text{fix } g_1 {R}$ , where $R = \overrightarrow{g/k : B := t, k_0 = k_1 = 1}$ , and

2.2. Typing rules. The typing judgment $\Gamma \vdash M : A$ or $\Gamma \vdash M = N : A$ is defined simultaneously with the property $\mathcal{WF}(\Gamma)$ of a well-formed valid context and the property $\Gamma \vdash M \prec N$ of cumulativity of types in Figures 1 ~ 4. We provide short explanations of some rules. For a more detailed explanation, refer to [Bertot and Castéran(2004)], [Letouzey(2004)], or [Paulin-Mohring(1996)].

Typing rules for basic terms and valid contexts (Figure 1). Typing rules for standard constructions of $\lambda$ - and $\Pi$ -terms are given.

(wf): Well-formed contexts contain well-typed terms, and they can be extended by well-typed inductive types, as in rule (ind-wf) of Figure 2.

( $\Pi$ ) and ( $\Pi\text{-eq}$ ): $\mathcal{P}(s_1, s_2, s_3)$ implies that

• • $s_2 = s_3 = \text{Prop}$ , or
• • $s_1 \in \text{Type}_i$ , $s_2 = \text{Type}_j$ and $s_3 = \text{Type}_k$ where $k \geq \max{i, j}$ .

Typing rules for inductive types and recursive functions (Figure 2). Typing rules for (mutually) inductive types, case distinctions, and (mutually) recursive functions are given.

(ind-wf): The positivity condition is crucial for defining an inductive type. A term $A$ is an arity ending in sort $s$ , $\text{Arity}(A, s)$ , if it is convertible to $s$ or a product $\Pi x : A. B$ , where $B$ is an arity ending in sort $s$ . $A$ is called an arity, $\text{Arity}(A)$ , if $A$ is an arity ending in sort $s$ for some sort $s$ .

A term $M$ satisfies the positivity condition for a variable $x$ when $M = \Pi \vec{y} : \vec{A}. x \vec{u}$ for some terms $\vec{A}, \vec{u}$ and the variable $x$ occurs strictly positively in $\vec{A}$ . A variable $x$ occurs strictly positively in $M$ when

• • $x$ does not occur in $M$ , or
• • $M \equiv \Pi \vec{y} : \vec{A}. (x \vec{B})$ and $x$ does not occur in $\vec{A}, \vec{B}$ .

Now, $\mathcal{I}_n(\Delta_I, \Delta_C)$ represents the following conditions:

• • All the names contained in the domains of $\Delta_I$ and $\Delta_C$ must be mutually distinct and new.

  $\backslash mathcal\{WF\}(\backslash emptyset)$	$\backslash frac\{\backslash Gamma\; \backslash vdash\; A\; :\; s\; \backslash quad\; x\; \backslash notin\; \backslash text\{dom\}(\backslash Gamma)\}\{\backslash mathcal\{WF\}(\backslash Gamma,\; (x\; :\; A))\}$	$\backslash frac\{\backslash Gamma\; \backslash vdash\; t\; :\; A\; \backslash quad\; x\; \backslash notin\; \backslash text\{dom\}(\backslash Gamma)\}\{\backslash mathcal\{WF\}(\backslash Gamma,\; (x\; :=\; t\; :\; A))\}$	(wf)
  	$\backslash frac\{\backslash mathcal\{WF\}(\backslash Gamma)\}\{\backslash Gamma\; \backslash vdash\; \backslash text\{Prop\}\; :\; \backslash text\{Type\}\_i\}$		(ax)
  	$\backslash frac\{\backslash mathcal\{WF\}(\backslash Gamma)\; \backslash quad\; (x\; :\; A)\; \backslash in\; \backslash Gamma\; \backslash quad\; \backslash text\{or\}\; \backslash quad\; (x\; :=\; t\; :\; A)\; \backslash in\; \backslash Gamma\}\{\backslash Gamma\; \backslash vdash\; x\; :\; A\}$		(var)
  	$\backslash frac\{\backslash Gamma,\; (x\; :=\; t\; :\; A)\; \backslash vdash\; u\; :\; U\}\{\backslash Gamma\; \backslash vdash\; \backslash text\{let\; \}\; x\; :=\; t\; \backslash text\{\; in\; \}\; u\; :\; U[x\; \backslash setminus\; t]\}$		(let)
  	$\backslash frac\{\backslash Gamma\; \backslash vdash\; t\; =\; t\text{'}\; :\; A\; \backslash quad\; \backslash Gamma,\; (x\; :=\; t\; :\; A)\; \backslash vdash\; u\; =\; u\text{'}\; :\; U\}\{\backslash Gamma\; \backslash vdash\; (\backslash text\{let\; \}\; x\; :=\; t\; \backslash text\{\; in\; \}\; u)\; =\; (\backslash text\{let\; \}\; x\; :=\; t\text{'}\; \backslash text\{\; in\; \}\; u\text{'})\; :\; U[x\; \backslash setminus\; t]\}$		(let-eq)
  	$\backslash frac\{\backslash Gamma\; \backslash vdash\; A\; :\; s\_1\; \backslash quad\; \backslash Gamma,\; x\; :\; A\; \backslash vdash\; B\; :\; s\_2\; \backslash quad\; \backslash mathcal\{P\}(s\_1,\; s\_2,\; s\_3)\}\{\backslash Gamma\; \backslash vdash\; \backslash Pi\; x\; :\; A.\; B\; :\; s\_3\}$		($\backslash Pi$)
  	$\backslash frac\{\backslash Gamma\; \backslash vdash\; A\; =\; A\text{'}\; :\; s\_1\; \backslash quad\; \backslash Gamma,\; x\; :\; A\; \backslash vdash\; B\; =\; B\text{'}\; :\; s\_2\; \backslash quad\; \backslash mathcal\{P\}(s\_1,\; s\_2,\; s\_3)\}\{\backslash Gamma\; \backslash vdash\; \backslash Pi\; x\; :\; A.\; B\; =\; \backslash Pi\; x\; :\; A\text{'}.\; B\text{'}\; :\; s\_3\}$		($\backslash Pi$-eq)
  	$\backslash frac\{\backslash Gamma,\; x\; :\; A\; \backslash vdash\; M\; :\; B\; \backslash quad\; \backslash Gamma\; \backslash vdash\; \backslash Pi\; x\; :\; A.\; B\; :\; s\}\{\backslash Gamma\; \backslash vdash\; \backslash lambda\; x\; :\; A.\; M\; :\; \backslash Pi\; x\; :\; A.\; B\}$		($\backslash lambda$)
  	$\backslash frac\{\backslash Gamma\; \backslash vdash\; A\; =\; A\text{'}\; :\; s\; \backslash quad\; \backslash Gamma,\; x\; :\; A\; \backslash vdash\; M\; =\; M\text{'}\; :\; B\; \backslash quad\; \backslash Gamma\; \backslash vdash\; \backslash Pi\; x\; :\; A.\; B\; :\; s\text{'}\}\{\backslash Gamma\; \backslash vdash\; \backslash lambda\; x\; :\; A.\; M\; =\; \backslash lambda\; x\; :\; A\text{'}.\; M\text{'}\; :\; \backslash Pi\; x\; :\; A.\; B\}$		($\backslash lambda$-eq)
  	$\backslash frac\{\backslash Gamma\; \backslash vdash\; M\; :\; \backslash Pi\; x\; :\; A.\; B\; \backslash quad\; \backslash Gamma\; \backslash vdash\; N\; :\; A\}\{\backslash Gamma\; \backslash vdash\; MN\; :\; B[x\; \backslash setminus\; N]\}$		(app)
  	$\backslash frac\{\backslash Gamma\; \backslash vdash\; M\; =\; M\text{'}\; :\; \backslash Pi\; x\; :\; A.\; B\; \backslash quad\; \backslash Gamma\; \backslash vdash\; N\; =\; N\text{'}\; :\; A\}\{\backslash Gamma\; \backslash vdash\; MN\; =\; M\text{'}N\text{'}\; :\; B[x\; \backslash setminus\; N]\}$		(app-eq)

Figure 1: Basic terms and valid contexts

• • All the types of $\Delta_I$ and $\Delta_C$ start with the same $n$ products, say, $\vec{p} : \vec{P}$ .
• • Any occurrence of some $d \in \text{dom}(\Delta_I)$ in $\Delta_C$ is of the form $(d \vec{p} \vec{u})$ , which is not applicable any more.
• • For all $d : A \in \Delta_I$ , $A$ is an arity ending in sort $s_d$ such that $s_d \neq \text{Prop}$ . Thus, we do not use inductive definitions of type $\text{Prop}$ . Some propositions defined inductively can be constructed using an impredicative coding. See [Girard et al.(1989)Girard, Taylor, and Lafont, Coquand(1990)], and [Werner(1997)] for further details.
• • For all $c : T \in \Delta_C$ , $T$ is the type of a constructor for an inductive type $d \in \text{dom}(\Delta_I)$ , i.e., $T$ is of the form $\Pi \vec{p} : \vec{P}. \Pi \vec{z} : \vec{Z}. (d \vec{p} \vec{u})$ . In this case, the sort $s_c$ in the third premise of the rule must be $s_d$ .
• • $T$ satisfies the positivity condition for all $x \in \text{dom}(\Delta_I)$ .

Notation. We use $\Gamma \vdash \text{Ind}_n{\Delta_I := \Delta_C}$ when all the premises of (ind-wf) are satisfied.

$$\backslash frac\{\backslash begin\{array\}\{c\}\; \backslash mathcal\{I\}\_n(\backslash Delta\_I,\; \backslash Delta\_C)\; \backslash \backslash \; \backslash Gamma\; \backslash vdash\; A\; :\; s\_d\; \backslash quad\; \backslash text\{for\; all\; \}\; (d\; :\; A)\; \backslash in\; \backslash Delta\_I\; \backslash \backslash \; \backslash Gamma,\; \backslash Delta\_I\; \backslash vdash\; T\; :\; s\_c\; \backslash quad\; \backslash text\{for\; all\; \}\; (c\; :\; T)\; \backslash in\; \backslash Delta\_C\; \backslash end\{array\}\}\{\backslash mathcal\{WF\}(\backslash Gamma,\; \backslash mathbf\{Ind\}\_n\backslash \{\backslash Delta\_I\; :=\; \backslash Delta\_C\backslash \})\}\; \backslash quad\; (ind-wf)$$

$$\backslash frac\{\backslash mathcal\{WF\}(\backslash Gamma)\; \backslash quad\; \backslash mathcal\{D\}\; =\; \backslash mathbf\{Ind\}\_n\backslash \{\backslash Delta\_I\; :=\; \backslash Delta\_C\backslash \}\; \backslash in\; \backslash Gamma\; \backslash quad\; d\; \backslash in\; \backslash text\{dom\}(\backslash Delta\_I)\}\{\backslash Gamma\; \backslash vdash\; \backslash mathcal\{D\}\; \backslash cdot\; d\; :\; \backslash Delta\_I(d)[.\backslash setminus\; \backslash mathcal\{D\}]\}\; \backslash quad\; (ind-type)$$

$$\backslash frac\{\backslash mathcal\{WF\}(\backslash Gamma)\; \backslash quad\; \backslash mathcal\{D\}\; =\; \backslash mathbf\{Ind\}\_n\backslash \{\backslash Delta\_I\; :=\; \backslash Delta\_C\backslash \}\; \backslash in\; \backslash Gamma\; \backslash quad\; c\; \backslash in\; \backslash text\{dom\}(\backslash Delta\_C)\}\{\backslash Gamma\; \backslash vdash\; \backslash mathcal\{D\}\; \backslash cdot\; c\; :\; \backslash Delta\_C(c)[.\backslash setminus\; \backslash mathcal\{D\}]\}\; \backslash quad\; (ind-const)$$

$$\backslash frac\{\backslash begin\{array\}\{c\}\; \backslash mathbf\{Ind\}\_n\backslash \{\backslash Delta\_I\; :=\; \backslash Delta\_C\backslash \}\; \backslash in\; \backslash Gamma\; \backslash quad\; (d\_i\; :\; \backslash Pi\; \backslash vec\{p\}\; :\; \backslash vec\{P\}.\; A)\; \backslash in\; \backslash Delta\_I\; \backslash quad\; lh(\backslash vec\{p\})\; =\; n\; \backslash \backslash \; \backslash Gamma\; \backslash vdash\; Q\; :\; B\; \backslash quad\; \backslash mathcal\{C\}(d\_i\; \backslash vec\{p\}\; :\; A;\; B)\; \backslash quad\; \backslash Gamma\; \backslash vdash\; e\; :\; d\_i\; \backslash vec\{p\}\; \backslash vec\{u\}\; \backslash \backslash \; \backslash Gamma\; \backslash vdash\; h\_k\; :\; \backslash Pi\; \backslash vec\{v\}\; :\; \backslash vec\{V\}\_k.\; Q\; \backslash vec\{w\}\_k\; (c\_k\; \backslash vec\{p\}\; \backslash vec\{v\})\; \backslash text\{\; for\; all\; \}\; (c\_k\; :\; \backslash Pi\; \backslash vec\{p\}\; :\; \backslash vec\{P\}.\; \backslash Pi\; \backslash vec\{v\}\; :\; \backslash vec\{V\}\_k.\; d\_i\; \backslash vec\{p\}\; \backslash vec\{w\}\_k)\; \backslash in\; \backslash Delta\_C\; \backslash end\{array\}\}\{\backslash Gamma\; \backslash vdash\; \backslash mathbf\{case\}(e,\; Q,\; (h\_k)\_k)\; :\; Q\; \backslash vec\{u\}\; e\}\; \backslash quad\; (case)$$

$$\backslash frac\{\backslash begin\{array\}\{c\}\; \backslash mathbf\{Ind\}\_n\backslash \{\backslash Delta\_I\; :=\; \backslash Delta\_C\backslash \}\; \backslash in\; \backslash Gamma\; \backslash quad\; (d\_i\; :\; \backslash Pi\; \backslash vec\{p\}\; :\; \backslash vec\{P\}.\; A)\; \backslash in\; \backslash Delta\_I\; \backslash quad\; lh(\backslash vec\{p\})\; =\; n\; \backslash \backslash \; \backslash Gamma\; \backslash vdash\; Q\; =\; Q\text{'}\; :\; B\; \backslash quad\; \backslash mathcal\{C\}(d\_i\; \backslash vec\{p\}\; :\; A;\; B)\; \backslash quad\; \backslash Gamma\; \backslash vdash\; e\; =\; e\text{'}\; :\; d\_i\; \backslash vec\{p\}\; \backslash vec\{u\}\; \backslash \backslash \; \backslash Gamma\; \backslash vdash\; h\_k\; =\; h\text{'}\_k\; :\; \backslash Pi\; \backslash vec\{v\}\; :\; \backslash vec\{V\}\_k.\; Q\; \backslash vec\{w\}\_k\; (c\_k\; \backslash vec\{p\}\; \backslash vec\{v\})\; \backslash text\{\; for\; all\; \}\; (c\_k\; :\; \backslash Pi\; \backslash vec\{p\}\; :\; \backslash vec\{P\}.\; \backslash Pi\; \backslash vec\{v\}\; :\; \backslash vec\{V\}\_k.\; d\_i\; \backslash vec\{p\}\; \backslash vec\{w\}\_k)\; \backslash in\; \backslash Delta\_C\; \backslash end\{array\}\}\{\backslash Gamma\; \backslash vdash\; \backslash mathbf\{case\}(e,\; Q,\; (h\_k)\_k)\; =\; \backslash mathbf\{case\}(e\text{'},\; Q\text{'},\; (h\text{'}\_k)\_k)\; :\; Q\; \backslash vec\{u\}\; e\}\; \backslash quad\; (case-eq)$$

$$\backslash frac\{\backslash mathcal\{F\}(\backslash vec\{f\},\; \backslash vec\{A\},\; \backslash vec\{k\},\; \backslash vec\{t\})\; \backslash quad\; n\; =\; lh(\backslash vec\{k\})\; \backslash quad\; (\backslash Gamma\; \backslash vdash\; A\_i\; :\; s\_i)\_\{\backslash forall\; i\; \backslash leq\; n\}\; \backslash quad\; (\backslash Gamma,\; \backslash vec\{f\}\; :\; \backslash vec\{A\}\; \backslash vdash\; t\_i\; :\; A\_i)\_\{\backslash forall\; i\; \backslash leq\; n\}\; \backslash quad\; j\; \backslash leq\; n\}\{\backslash Gamma\; \backslash vdash\; \backslash mathbf\{fix\}\; f\_j\; \backslash \{\; \backslash vec\{f\}\; /\; k\; :\; A\; :=\; \backslash vec\{t\}\; \backslash \}\; :\; A\_j\}\; \backslash quad\; (fix)$$

$$\backslash frac\{\backslash begin\{array\}\{c\}\; \backslash mathcal\{F\}(\backslash vec\{f\},\; \backslash vec\{A\},\; \backslash vec\{k\},\; \backslash vec\{t\})\; \backslash quad\; \backslash mathcal\{F\}(\backslash vec\{f\},\; \backslash vec\{A\}\text{'},\; \backslash vec\{k\},\; \backslash vec\{t\}\text{'})\; \backslash quad\; n\; =\; lh(\backslash vec\{k\})\; \backslash \backslash \; (\backslash Gamma\; \backslash vdash\; A\_i\; =\; A\text{'}\_i\; :\; s\_i)\_\{\backslash forall\; i\; \backslash leq\; n\}\; \backslash quad\; (\backslash Gamma,\; \backslash vec\{f\}\; :\; \backslash vec\{A\}\; \backslash vdash\; t\_i\; =\; t\text{'}\_i\; :\; A\_i)\_\{\backslash forall\; i\; \backslash leq\; n\}\; \backslash quad\; j\; \backslash leq\; n\; \backslash end\{array\}\}\{\backslash Gamma\; \backslash vdash\; \backslash mathbf\{fix\}\; f\_j\; \backslash \{\; \backslash vec\{f\}\; /\; k\; :\; A\; :=\; \backslash vec\{t\}\; \backslash \}\; =\; \backslash mathbf\{fix\}\; f\_j\; \backslash \{\; \backslash vec\{f\}\; /\; k\; :\; A\text{'}\; :=\; \backslash vec\{t\}\text{'}\; \backslash \}\; :\; A\_j\}\; \backslash quad\; (fix-eq)$$

Figure 2: Inductive types and recursive functions

(ind-type) and (ind-const): Given $\mathcal{D} = \mathbf{Ind}_n{\Delta_I := \Delta_C}$ and a term $A$ , $A[.\setminus \mathcal{D}]$ implies that every occurrence of $z \in \text{dom}(\Delta_I, \Delta_C)$ in $A$ is replaced with $\mathcal{D} \cdot z$ .

(case) and (case-eq): $d_i$ and $c_k$ denote $\mathbf{Ind}_n{\Delta_I := \Delta_C} \cdot d_i$ and $\mathbf{Ind}_n{\Delta_I := \Delta_C} \cdot c_k$ , respectively. Furthermore, $lh(\vec{u}) = lh(\vec{w}_k)$ .

For an inductive type $d$ and an arity $B$ , the relation $\mathcal{C}(d \vec{q} : A; B)$ is defined as follows:

• • $\mathcal{C}(d \vec{q} : \mathbf{Prop}; d \vec{q} \rightarrow \mathbf{Prop})$ ;
• • $\mathcal{C}(d \vec{q} : \mathbf{Prop}; d \vec{q} \rightarrow \mathbf{Type}_j)$ iff $d$ is an inductive type that is empty or has only one constructor³ such that all the non-parametric arguments are of sort $\mathbf{Prop}$ ;
• • $\mathcal{C}(d \vec{q} : \mathbf{Type}_j; d \vec{q} \rightarrow s)$ for any sort $s$ ;
• • $\mathcal{C}(d \vec{q} : (\Pi u : U. A); (\Pi u : U. B))$ iff $\mathcal{C}(d \vec{q} u : A; B)$ .

³This reflects the fact that no pattern matching is allowed on proof-terms, which would otherwise result in a paradox, as shown by [Coquand(1990)].

$$\backslash frac\{\backslash Gamma\; \backslash vdash\; M\; :\; A\}\{\backslash Gamma\; \backslash vdash\; M\; =\; M\; :\; A\}$$	$$\backslash frac\{\backslash Gamma\; \backslash vdash\; M\; =\; N\; :\; A\}\{\backslash Gamma\; \backslash vdash\; N\; =\; M\; :\; A\}$$	$(ref)(sym)$
$$\backslash frac\{\backslash Gamma\; \backslash vdash\; M\; =\; N\; :\; A\; \backslash quad\; \backslash Gamma\; \backslash vdash\; N\; =\; P\; :\; A\}\{\backslash Gamma\; \backslash vdash\; M\; =\; P\; :\; A\}$$		$(trans)$
$$\backslash frac\{\backslash Gamma\; \backslash vdash\; M\; :\; A\; \backslash quad\; \backslash Gamma\; \backslash vdash\; A\; =\; B\; :\; s\}\{\backslash Gamma\; \backslash vdash\; M\; :\; B\}$$	$$\backslash frac\{\backslash Gamma\; \backslash vdash\; M\; =\; N\; :\; A\; \backslash quad\; \backslash Gamma\; \backslash vdash\; A\; =\; B\; :\; s\}\{\backslash Gamma\; \backslash vdash\; M\; =\; N\; :\; B\}$$	$(conv)(conv-eq)$
$$\backslash frac\{\backslash Gamma,\; x\; :\; A\; \backslash vdash\; M\; :\; B\; \backslash quad\; \backslash Gamma\; \backslash vdash\; \backslash Pi\; x\; :\; A.\; B\; :\; s\; \backslash quad\; \backslash Gamma\; \backslash vdash\; N\; :\; A\}\{\backslash Gamma\; \backslash vdash\; (\backslash lambda\; x\; :\; A.\; M)N\; =\; M[x\; \backslash setminus\; N]\; :\; B[x\; \backslash setminus\; N]\}$$		$(\backslash beta)$
$$\backslash frac\{\backslash mathcal\{WF\}(\backslash Gamma)\; \backslash quad\; (x\; :=\; t\; :\; A)\; \backslash in\; \backslash Gamma\}\{\backslash Gamma\; \backslash vdash\; x\; =\; t\; :\; A\}$$		$(\backslash delta)$
$$\backslash frac\{\backslash Gamma\; \backslash vdash\; t\; :\; A\; \backslash quad\; \backslash Gamma,\; (x\; :=\; t\; :\; A)\; \backslash vdash\; u\; :\; U\}\{\backslash Gamma\; \backslash vdash\; (\backslash mathbf\{let\}\; \backslash \; x\; :=\; t\; \backslash \; \backslash mathbf\{in\}\; \backslash \; u)\; =\; u[x\; \backslash setminus\; t]\; :\; U[x\; \backslash setminus\; t]\}$$		$(\backslash zeta)$
		$(\backslash iota)$
$$\backslash frac\{\}\{\backslash Gamma\; \backslash vdash\; \backslash mathbf\{case\}(c\_j\; \backslash vec\{p\}\; \backslash vec\{a\},\; Q,\; (h\_k)\_k)\; =\; h\_j\; \backslash vec\{a\}\; :\; Q\; \backslash vec\{u\}(c\_j\; \backslash vec\{p\}\; \backslash vec\{a\})\}$$		$(\backslash iota)$
$$\backslash begin\{aligned\}\; (\backslash Gamma\; \backslash vdash\; A\_i\; :\; s\_i)\_\{\backslash forall\; i\; \backslash leq\; n\}\; \backslash quad\; (\backslash Gamma,\; \backslash vec\{f\}\; :\; \backslash vec\{A\}\; \backslash vdash\; t\_i\; :\; A\_i)\_\{\backslash forall\; i\; \backslash leq\; n\}\; \backslash quad\; \backslash mathcal\{F\}(\backslash vec\{f\},\; \backslash vec\{A\},\; \backslash vec\{k\},\; \backslash vec\{t\})\; \backslash quad\; j\; \backslash leq\; n\; \backslash \backslash \; R\; \backslash equiv\; f/k\; :\; A\; :=\; \backslash vec\{t\}\; \backslash quad\; A\_j\; \backslash equiv\; \backslash Pi\; \backslash vec\{x\}\_j\; :\; \backslash vec\{B\}\_j.\; A\text{'}\_j\; \backslash quad\; \backslash Gamma\; \backslash vdash\; \backslash vec\{a\}\; :\; \backslash vec\{B\}\_j\; \backslash quad\; lh(\backslash vec\{B\}\_j)\; =\; k\_j\; +\; 1\; \backslash end\{aligned\}$$		$(\backslash iota)$
$$\backslash frac\{\}\{\backslash Gamma\; \backslash vdash\; (\backslash mathbf\{fix\}\; \backslash \; f\_j\; \backslash \{R\backslash \})\; \backslash vec\{a\}\; =\; (t\_j[f\_i\; \backslash setminus\; (\backslash mathbf\{fix\}\; \backslash \; f\_i\; \backslash \{R\backslash \})]\; \backslash vec\{a\})\; :\; A\text{'}\_j\backslash \{\backslash vec\{x\}\; :\; \backslash vec\{a\}\backslash \}\}$$		$(\backslash iota)$
$\backslash vdash\; \backslash mathbf\{Prop\}\; \backslash prec\; \backslash mathbf\{Type\}\_0$	$\backslash vdash\; \backslash mathbf\{Type\}\_j\; \backslash prec\; \backslash mathbf\{Type\}\_\{j+1\}$	$(inc)$
$$\backslash frac\{\backslash Gamma\; \backslash vdash\; M\; \backslash prec\; N\; \backslash quad\; \backslash Gamma\; \backslash vdash\; N\; \backslash prec\; P\}\{\backslash Gamma\; \backslash vdash\; M\; \backslash prec\; P\}$$		$(trans-inc)$
$$\backslash frac\{\backslash Gamma\; \backslash vdash\; A\; \backslash prec\; B\; \backslash quad\; \backslash Gamma\; \backslash vdash\; C\; :\; s\; \backslash quad\; x\; \backslash notin\; \backslash text\{dom\}(\backslash Gamma)\}\{\backslash Gamma,\; x\; :\; C\; \backslash vdash\; A\; \backslash prec\; B\}$$		$(weak-inc)$
$$\backslash frac\{\backslash Gamma\; \backslash vdash\; A\_1\; =\; B\_1\; :\; s\; \backslash quad\; \backslash Gamma,\; x\; :\; A\_1\; \backslash vdash\; A\_2\; \backslash prec\; B\_2\}\{\backslash Gamma\; \backslash vdash\; \backslash Pi\; x\; :\; A\_1.\; A\_2\; \backslash prec\; \backslash Pi\; x\; :\; B\_1.\; B\_2\}$$		$(\backslash Pi-inc)$
$$\backslash frac\{\backslash Gamma\; \backslash vdash\; M\; =\; N\; :\; s\; \backslash quad\; \backslash Gamma\; \backslash vdash\; M\; \backslash prec\; P\}\{\backslash Gamma\; \backslash vdash\; N\; \backslash prec\; P\}$$	$$\backslash frac\{\backslash Gamma\; \backslash vdash\; M\; =\; N\; :\; s\; \backslash quad\; \backslash Gamma\; \backslash vdash\; P\; \backslash prec\; M\}\{\backslash Gamma\; \backslash vdash\; P\; \backslash prec\; N\}$$	$(eq-inc)$
$$\backslash frac\{\backslash Gamma\; \backslash vdash\; M\; :\; A\; \backslash quad\; \backslash Gamma\; \backslash vdash\; A\; \backslash prec\; B\}\{\backslash Gamma\; \backslash vdash\; M\; :\; B\}$$	$$\backslash frac\{\backslash Gamma\; \backslash vdash\; M\; =\; N\; :\; A\; \backslash quad\; \backslash Gamma\; \backslash vdash\; A\; \backslash prec\; B\}\{\backslash Gamma\; \backslash vdash\; M\; =\; N\; :\; B\}$$	$(cum)(cum-eq)$

Figure 3: Judgmental equality and cumulative type universesThis means that an object of the inductive type $d$ can be eliminated for proving a property $P$ of type $B$ . Let $\mathcal{C}(d\vec{q}; B)$ denote $\mathcal{C}(d\vec{q} : A; B)$ , where $A$ is the type of $d\vec{q}$ .

(fix) and (fix-eq): $\mathcal{F}(\vec{f}, \vec{A}, \vec{k}, \vec{t})$ represents the following conditions:

• • $lh(\vec{f}) = lh(\vec{A}) = lh(\vec{k}) = lh(\vec{t})$ ,
• • for each $t_i \in \vec{t}$ , there is an inductive type $\mathcal{D} \cdot d$ , where $\mathcal{D} = \mathbf{Ind}_n{\Delta_I := \Delta_C}$ , and a term $T_i$ such that
  • – $t_i = \lambda \vec{y} : \vec{Y}. \lambda z : (\mathcal{D} \cdot d) \vec{u}. t'_i$ , where $lh(\vec{Y}) = k_i$ , and
  • – there is a constrained derivation with respect to $z$ and $\Delta_I, \Delta_C$ such that

$${\mathrm{\Gamma }}^{ϵ},(\vec{y}:\vec{Y}{)}^{ϵ},z:{=}^z(\mathcal{D}\cdot d)\vec{u},(\vec{f}:\vec{A}{)}_{\vec{k}}^{\le z}⊢t_i^{\mathrm{\prime }}{:}^{ϵ}{T}_i^{ϵ}\backslash Gamma^\backslash epsilon,\; (\backslash vec\{y\}\; :\; \backslash vec\{Y\})^\backslash epsilon,\; z\; :=^z\; (\backslash mathcal\{D\}\; \backslash cdot\; d)\; \backslash vec\{u\},\; (\backslash vec\{f\}\; :\; \backslash vec\{A\})\_\{\backslash vec\{k\}\}^\{\backslash leq\; z\}\; \backslash vdash\; t\text{'}\_i\; :^\backslash epsilon\; T\_i^\backslash epsilon$$

where $(\vec{f} : \vec{A})_{\vec{k}}^{\leq z}$ is the context composed of

$$f_j{:}^{ϵ}\mathrm{\Pi }(\vec{u}:{\vec{B}}_j{)}^{ϵ}\mathrm{.}\mathrm{\Pi }v:{=}^z{X}_j\mathrm{.}{P}_j^{ϵ}f\_j\; :^\backslash epsilon\; \backslash Pi(\backslash vec\{u\}\; :\; \backslash vec\{B\}\_j)^\backslash epsilon.\; \backslash Pi\; v\; :=^z\; X\_j.\; P\_j^\backslash epsilon$$

if $f_j : \Pi(\vec{u} : \vec{B}_j). \Pi v : X_j. P_j$ is from $\vec{f} : \vec{A}$ and $lh(B_j) = k_j$ .

The condition for constrained derivation ensures that the constructed terms are normalizing terms. A formal definition is given in Appendix B. Informally, it means that $t_i$ can only contain decreasing recursive calls: if $f_j$ appears in $t_i$ , then it must have at least $k_j + 1$ arguments, and its $(k_j + 1)$ th argument must be structurally smaller than the initial inductive argument $z$ (Thus, any subterm of an inductive term obtained by going through at least one constructor is structurally smaller than the initial term.).

Judgmental equality and type universes (Figure 3). The rules in Figure 3 stipulate that the judgmental equality based on reductions is an equivalence relation. De Bruijn's telescope notation is very useful: $\Gamma \vdash \vec{t} : \vec{A}$ with $lh(t) = n$ implies that

• • $\Gamma, x_1 : A_1, \dots, x_{j-1} : A_{j-1} \vdash A_j : s_j$ for all $j \in {1, \dots, n}$ , and
• • $\Gamma \vdash t_j : A_j[x_1 \setminus t_1] \cdots [x_{j-1} \setminus t_{j-1}]$ for all $j \in {1, \dots, n}$ .

3. SET-THEORETIC MODEL CONSTRUCTION

3.1. Background. We must resolve a dilemma related to the construction of a set-theoretic model of CC and its extensions. In a proof-irrelevant model, each type expression should have an obvious set-theoretic interpretation; however, it is well known that impredicative or polymorphic types, such as Prop, can only have a trivial set-theoretic interpretation, as shown by [Reynolds(1984)]. Hence, it is necessary to assign a singleton or the empty set to each term of type Prop.

In constructing a set-theoretic model of Coquand's CC, [Miquel and Werner(2003)] provided the following solution. Under the assumption of the existence of a urelement • that does not belong to the standard universe of set theory, the sort Prop is associated with${\emptyset, {\bullet}}$ . Furthermore, the application and $\lambda$ -abstraction terms are interpreted by app and lam, respectively, which are defined as follows:

Remark 3.1. This construction does not correctly model the cumulative relation between Prop and $\text{Type}_i$ , as demonstrated in the following example; [Werner(2008)] showed that it can be easily extended to the cumulative type universes when the subtyping relation between Prop and $\text{Type}_i$ does not exist

Consider $I = \lambda(A : \text{Type}_0). A \rightarrow A$ . Then, its type of set-theoretic interpretation is not deterministic. Suppose that $P$ is a true proposition. Then, $\llbracket I P \rrbracket$ depends on the type we have assigned to $P$ , that is, Prop or $\text{Type}_0$ . In the former case, $\llbracket I P \rrbracket = {\bullet}$ since $P \rightarrow P$ is a tautology, whereas in the latter case, $\llbracket I P \rrbracket = \llbracket I \rrbracket(\llbracket P \rrbracket) = {f \mid f : {\bullet} \rightarrow {\bullet}} \neq {\bullet}$ since $\llbracket P \rrbracket = {\bullet}$ .

Another solution was provided by [Aczel(1998)]. He used the trace encoding of functions in order to provide an adequate interpretation of the impredicative type Prop of propositions and its relationship with $\text{Type}_i$ . For this reason, we adopt Aczel's solution.

Definition 3.2 (Trace encoding of set-theoretic functions). Let $u, x, f$ denote sets. Then,

Note that for any function $f$ and any $x \in \text{dom}(f)$ , we have

$$\mathbf{a}\mathbf{p}\mathbf{p}(\mathbf{l}\mathbf{a}\mathbf{m}(f),x)=\{y\mid (x,y)\in \mathbf{l}\mathbf{a}\mathbf{m}(f)\}=\{y\mid y\in f(x)\}=f(x)\mathrm{.}\backslash mathbf\{app\}(\backslash mathbf\{lam\}(f),\; x)\; =\; \backslash \{y\; \backslash mid\; (x,\; y)\; \backslash in\; \backslash mathbf\{lam\}(f)\backslash \}\; =\; \backslash \{y\; \backslash mid\; y\; \backslash in\; f(x)\backslash \}\; =\; f(x).$$

Notations.

1. (1) In the remainder of this paper, $\downarrow$ is used if something is well defined, and $\uparrow$ is used otherwise.
2. (2) Given sets $A, B(x)$ , $x \in A$ , let $\prod_{x \in A} B(x)$ denote the set of all functions $f$ such that $\text{dom}(f) = A$ and $f(x) \in B(x)$ for all $x \in A$ .
3. (3) Given a function $f \in \prod_{x_1 \in A_1} \cdots \prod_{x_n \in A_n(x_1, \dots, x_{n-1})} B(x_1, \dots, x_n)$ , we use the notation $\vec{\mathbf{lam}}_n(f)$ (resp. and $\vec{\mathbf{app}}(f, \vec{x})$ ) for the $n$ -times application of lam (resp. app):

We suppress the subscript $n$ when the number of times we want to apply lam or app is obvious from the context. Note that $\vec{\mathbf{lam}}_0(f) = f$ and $\vec{\mathbf{app}}_0(f, \text{nil}) = f$ .

Lemma 3.3 ([Aczel(1998)]). Given a set $A$ , assume $B(x) \subseteq 1$ for all $x \in A$ .

1. (1) ${\mathbf{lam}(f) \mid f \in \prod_{x \in A} B(x)} \subseteq 1$ .
2. (2) ${\mathbf{lam}(f) \mid f \in \prod_{x \in A} B(x)} = 1$ iff $\forall x \in A (B(x) = 1)$ .Proof. Let $f \in \prod_{x \in A} B(x)$ , i.e.,

Then, we have

This also implies that ${\mathbf{lam}(f) \mid f \in \prod_{x \in A} B(x)} = 1$ iff $\forall x \in A (B(x) = 1)$ . $\square$

Remark 3.4. A useful feature of trace encoding is that $\mathbf{app}(u, a)$ and $\mathbf{lam}(f)$ are always defined for any sets $u, a, f$ , including the empty set. This, however, implies that we sometimes lose the information of the domain of a given function $f$ , i.e., we cannot trace back to $\text{dom}(f)$ starting from $\mathbf{lam}(f)$ . We will see that the use of judgmental equality enables us to avoid such a loss when only well-typed terms are involved.

3.2. Inductive types and rule sets. Here, we follow the approaches of [Aczel(1998)] and [Dybjer(1991)] for the construction of a set-theoretic interpretation of inductive types. We are particularly interested in rule sets.

We are going to work on the basis of ZF set theory with an axiom guaranteeing the existence of countably many (strongly) inaccessible cardinals. Note that such an axiom is independent of ZFC. [Werner(1997)] showed that such an axiom is sufficient for a set-theoretic interpretation of the cumulative type universes and predicatively inductive types. However, it is not clear whether this axiom is necessary for our construction. Indeed, the required feature of an inaccessible cardinal $\kappa$ is the closure property of the universe $\mathcal{V}_\kappa$ under the powerset operation. This is a necessary condition for the interpretation of inductive types.

Henceforth, assume that there are countably many (strongly) inaccessible cardinals. Let $\kappa_0 = \omega$ and $\kappa_1, \kappa_2, \dots$ enumerate these inaccessible cardinals. We associate each sort $\text{Type}_i$ with its $\text{rank}(\text{Type}_i) := \kappa_i$ . If $(\mathcal{V}\alpha){\alpha \in \text{Ord}}$ denotes the (standard) universe of sets defined as follows, then $\mathcal{V}_\kappa$ is a model of ZF:

$${\mathcal{V}}_0:=\mathrm{\varnothing }\text{and}{\mathcal{V}}_{\alpha }:=\bigcup _{\beta \in \alpha }\mathcal{P}({\mathcal{V}}_{\beta })\text{if }\alpha >0\backslash mathcal\{V\}\_0\; :=\; \backslash emptyset\; \backslash quad\; \backslash text\{and\}\; \backslash quad\; \backslash mathcal\{V\}\_\backslash alpha\; :=\; \backslash bigcup\_\{\backslash beta\; \backslash in\; \backslash alpha\}\; \backslash mathcal\{P\}(\backslash mathcal\{V\}\_\backslash beta)\; \backslash quad\; \backslash text\{if\; \}\; \backslash alpha\; >\; 0$$

$\text{Ord}$ denotes the class of all ordinals, $\lambda$ denotes a limit ordinal, and $\mathcal{P}$ denotes the power set operator. In particular, if $\kappa$ is an inaccessible cardinal, $A \in \mathcal{V}_\kappa$ , and for every $a \in A$ , $B_a \in \mathcal{V}\kappa$ , then, $\prod{a \in A} B_a \in \mathcal{V}\kappa$ . Let $\text{rank}(\text{Prop}) := -1$ and $\mathcal{V}{-1} = {0, 1}$ for convenience. Refer to [Drake(1974)] for further details about inaccessible cardinals.

A rule on a base set $U$ is a pair of sets $\langle u, v \rangle$ , often written as $\frac{u}{v}$ , such that $u \subseteq U$ and $v \in U$ . A set of rules on $U$ is called a rule set on $U$ . Given a rule set $\Phi$ on $U$ , a set $w \subseteq U$ is $\Phi$ -closed if for any $\frac{u}{v} \in \Phi$ , $v \in w$ whenever $u \subseteq w$ . Note that there is the least $\Phi$ -closed set

$$\mathcal{I}(\mathrm{\Phi }):=\bigcap \{w\subseteq U\mid w\mathrm{\Phi }\text{-closed}\}\mathrm{.}\backslash mathcal\{I\}(\backslash Phi)\; :=\; \backslash bigcap\; \backslash \{w\; \backslash subseteq\; U\; \backslash mid\; w\; \backslash text\{\; \}\; \backslash Phi\backslash text\{-closed\}\backslash \}.$$

In fact, it is well known that each rule set $\Phi$ on $U$ generates a monotone operator on $\mathcal{P}(U)$

$${\mathrm{\Gamma }}_{\mathrm{\Phi }}(X):=\{v\in U\mid \text{there exists some }u\subseteq X\text{ such that }\frac{u}{v}\in \mathrm{\Phi }\}\backslash Gamma\_\backslash Phi(X)\; :=\; \backslash \{v\; \backslash in\; U\; \backslash mid\; \backslash text\{there\; exists\; some\; \}\; u\; \backslash subseteq\; X\; \backslash text\{\; such\; that\; \}\; \backslash frac\{u\}\{v\}\; \backslash in\; \backslash Phi\backslash \}$$such that $\mathcal{I}(\Phi)$ is the least fixed point of $\Gamma_\Phi$ . Assuming that $\Phi$ is a rule set on $I \times U$ , $\Phi$ defines a family $\mathcal{IF}(\Phi)$ of sets in $U$ over $I$ as

$$\mathcal{I}\mathcal{F}(\mathrm{\Phi })(i):=\{u\in U\mid ⟨i,u⟩\in \mathcal{I}(\mathrm{\Phi })\}\backslash mathcal\{IF\}(\backslash Phi)(i)\; :=\; \backslash \{u\; \backslash in\; U\; \backslash mid\; \backslash langle\; i,\; u\; \backslash rangle\; \backslash in\; \backslash mathcal\{I\}(\backslash Phi)\backslash \}$$

for each $i \in I$ .

A rule set is deterministic provided that it contains at most one rule with a given conclusion. The rule sets defined below by an inductive definition are deterministic. This makes it possible to interpret functions defined by structural recursion on a certain inductive type as set-theoretic functions. The interpretations are defined on the corresponding set-theoretic inductively defined set, which is the fixpoint of a monotone operator. Refer to [Aczel(1977)] and [Moschovakis(1974), Moschovakis(1980)] for further details about rule sets, monotone operators, and fixpoints.

Below, we describe the interpretations of inductive and recursive types with some examples. Given a well-defined (mutually) inductive type $\mathbf{Ind}_n{\Delta_I := \Delta_C}$ , where

$${\mathrm{\Delta }}_I=x_0:A_1,\dots ,x_{\mathrm{\ell }}:A_{\mathrm{\ell }}\text{and}{A}_i=\mathrm{\Pi }\vec{p}:\vec{P}\mathrm{.}\mathrm{\Pi }{\vec{a}}_i:{\vec{B}}_i\mathrm{.}{s}_i,\backslash Delta\_I\; =\; x\_0\; :\; A\_1,\; \backslash dots,\; x\_\backslash ell\; :\; A\_\backslash ell\; \backslash quad\; \backslash text\{and\}\; \backslash quad\; A\_i\; =\; \backslash Pi\; \backslash vec\{p\}\; :\; \backslash vec\{P\}.\; \backslash Pi\; \backslash vec\{a\}\_i\; :\; \backslash vec\{B\}\_i.\; s\_i,$$

let $\text{rank}(x_i) := \text{rank}(s_i)$ .

Notations.

1. (1) With each context $\Gamma$ , we associate a set $\llbracket \Gamma \rrbracket$ of $\Gamma$ -valuations of the form $\langle \alpha_1, \dots, \alpha_n \rangle$ , where $n$ is the length of $\Gamma$ and $\langle, \dots, \rangle$ denotes a sequence of a finite length. Given a sequence $L = \langle \alpha_1, \dots, \alpha_n \rangle$ and a natural number $i < n$ , we set $(L)i = \alpha{i+1}$ . If $\alpha_{i+1}$ itself is a sequence of length $m$ , then we write $(L){i,j}$ for $(\alpha{i+1})_j$ if $j < m$ , etc.
2. (2) $\alpha, \beta, \alpha_i, \beta_i$ vary over single values while $\gamma, \delta, \gamma_i, \delta_i$ vary over valuations. nil denotes the empty sequence. Given two valuations $\gamma$ and $\delta$ , the notation $\gamma, \delta$ denotes their concatenation. If $\delta = \langle \alpha \rangle$ , then we write $\gamma, \alpha$ instead of $\gamma, \langle \alpha \rangle$ .
3. (3) With each pair $(\Gamma, t)$ formed by a context $\Gamma$ and a term $t$ , we associate a function $\llbracket \Gamma \vdash t \rrbracket$ that is partially defined on $\Gamma$ -valuations: $\llbracket \Gamma \vdash t \rrbracket_\gamma$ denotes $\llbracket \Gamma \vdash t \rrbracket(\gamma)$ when $\gamma \in \llbracket \Gamma \rrbracket$ .
4. (4) In the following, we write $\llbracket t \rrbracket$ for $\llbracket \Gamma \vdash t \rrbracket_\gamma$ if $\Gamma$ and $\gamma \in \llbracket \Gamma \rrbracket$ are fixed in the context. Similarly, we use the notation $\vec{u} \in \llbracket \vec{A} \rrbracket$ for $u_1 \in \llbracket \Gamma \vdash A_1 \rrbracket_\gamma, \dots, u_n \in \llbracket \Gamma, x_1 : A_1, \dots, x_{n-1} : A_{n-1} \vdash A_n \rrbracket_{\gamma, u_1 \dots u_{n-1}}$ for some context $\Gamma$ and $\Gamma$ -valuation $\gamma \in \llbracket \Gamma \rrbracket$ .

3.3. Interpretation of inductive types. Here, we claim the existence of the interpretations of inductive types that satisfy the soundness of the rules (ind-wf), (ind-type), and (ind-const) when the conditions in the typing rules are fulfilled. The formal definition is given in Appendix C. Refer to [Dybjer(1991)], whose idea is generalized in this paper.

Lemma 3.5. Suppose $\Gamma \vdash \mathcal{D}$ , where $\mathcal{D} = \mathbf{Ind}_n{\Delta_I := \Delta_C}$ . Let $\gamma \in \llbracket \Gamma \rrbracket$ be given. As mentioned before, we suppress $\Gamma$ and $\gamma$ for better readability. Further suppose that

$${\mathrm{\Delta }}_I:=d_0:A_0,\dots ,d_{\mathrm{\ell }}:A_{\mathrm{\ell }},{\mathrm{\Delta }}_C:=c_1:T_1,\dots ,c_m:T_m,\backslash Delta\_I\; :=\; d\_0\; :\; A\_0,\; \backslash dots,\; d\_\backslash ell\; :\; A\_\backslash ell,\; \backslash quad\; \backslash Delta\_C\; :=\; c\_1\; :\; T\_1,\; \backslash dots,\; c\_m\; :\; T\_m,$$

$$A_i:=\mathrm{\Pi }\vec{p}:\vec{P}\mathrm{.}\mathrm{\Pi }{\vec{b}}_i:{\vec{B}}_i\mathrm{.}{s}_i,T_k:=\mathrm{\Pi }\vec{p}:\vec{P}\mathrm{.}\mathrm{\Pi }{\vec{z}}_k:{\vec{Z}}_k\mathrm{.}{d}_{i_k}\vec{p}{\vec{t}}_k\mathrm{.}A\_i\; :=\; \backslash Pi\; \backslash vec\{p\}\; :\; \backslash vec\{P\}.\; \backslash Pi\; \backslash vec\{b\}\_i\; :\; \backslash vec\{B\}\_i.\; s\_i,\; \backslash quad\; T\_k\; :=\; \backslash Pi\; \backslash vec\{p\}\; :\; \backslash vec\{P\}.\; \backslash Pi\; \backslash vec\{z\}\_k\; :\; \backslash vec\{Z\}\_k.\; d\_\{i\_k\}\; \backslash vec\{p\}\; \backslash vec\{t\}\_k.$$

Then, there is some rule set $\Phi$ such that the following interpretation of $\mathcal{D} \cdot d_i$ and $\mathcal{D} \cdot c_k$ satisfies the soundness of the rules (ind-type) and (ind-const):

• • $\llbracket \mathcal{D} \cdot d_i \rrbracket := \mathbf{lam}(f_i)$ where $f_i(\vec{p}, \vec{b}_i) := \mathcal{IF}(\Phi)(i, \vec{p}, \vec{b}_i)$ for $\vec{p}, \vec{b}_i : \llbracket \vec{P}, \vec{B}_i \rrbracket$ ,
• • $\llbracket \mathcal{D} \cdot c_k \rrbracket := \mathbf{lam}(g_k)$ where $g_k(\vec{p}, \vec{z}_k) := \langle k, \vec{z}_k \rangle$ for $\vec{p}, \vec{z}_k : \llbracket \vec{P}, \vec{Z}_k \rrbracket$ .Remark 3.6. The positivity condition is crucial for showing that the construction of the rule set $\Phi$ in Appendix C is well defined.

The elements of our rule sets $\Phi$ are of the form $\frac{u}{\langle i, \vec{p}, \vec{t}, \langle j, \vec{v} \rangle \rangle}$ , where $i$ denotes the $i$ th inductive type $d_i$ , $\vec{p}$ denote the parameters, $\vec{t}$ denote the non-parametric arguments of $d_i$ , $j$ denotes the $j$ th constructor of $d_i$ , and $\vec{v}$ denote the non-parametric arguments of the $j$ th constructor. Note that $\vec{p}, \vec{t}, \vec{v}$ could be empty.

Example 3.7 (Natural numbers). Let $\mathcal{D}_N$ be the inductive type for natural numbers, as in Remark 2.6. Then,

$${\mathrm{\Phi }}_{\text{nat}}=\left\{\frac{\mathrm{\varnothing }}{⟨0,⟨1⟩⟩}\right\}\cup \{\frac{\{v\}}{⟨0,⟨2,v⟩⟩}\mid v\in {\mathcal{V}}_{{\kappa }_0}\},\backslash Phi\_\{\backslash text\{nat\}\}\; =\; \backslash left\backslash \{\; \backslash frac\{\backslash emptyset\}\{\backslash langle\; 0,\; \backslash langle\; 1\; \backslash rangle\; \backslash rangle\}\; \backslash right\backslash \}\; \backslash cup\; \backslash left\backslash \{\; \backslash frac\{\backslash \{v\backslash \}\}\{\backslash langle\; 0,\; \backslash langle\; 2,\; v\; \backslash rangle\; \backslash rangle\}\; \backslash mid\; v\; \backslash in\; \backslash mathcal\{V\}\_\{\backslash kappa\_0\}\; \backslash right\backslash \},$$

$\llbracket \text{nat} \rrbracket = \mathcal{IF}(\Phi_{\text{nat}})(0)$ , $\llbracket 0 \rrbracket = \langle 1 \rangle$ , and $\text{app}(\llbracket \text{S} \rrbracket, n) = \langle 2, n \rangle$ for any $n \in \llbracket \text{nat} \rrbracket$ .

Example 3.8 (Inductive families). The following Coq-expression shows a typical use of inductive families.

Inductive toto : Type -> Type :=
| Y1 : forall x : Type, toto x
| Y2 : forall x : Type, toto nat -> toto x -> toto x.

The inductive type toto can be represented by $\mathcal{D}_{\text{toto}} = \text{Ind}_0{\Delta_I := \Delta_C}$ , where

Then,

$${\mathrm{\Phi }}_{\text{toto}}=\{\frac{\mathrm{\varnothing }}{⟨0,x,⟨1,x⟩⟩}\mid x\in {\mathcal{V}}_{{\kappa }_1}\}\cup \{\frac{\{⟨0,\mathrm{⟦}\text{nat}\mathrm{⟧},v_1⟩,⟨0,x,v_2⟩\}}{⟨0,x,⟨2,x,v_1,v_2⟩⟩}\mid x,v_1,v_2\in {\mathcal{V}}_{{\kappa }_1}\},\backslash Phi\_\{\backslash text\{toto\}\}\; =\; \backslash left\backslash \{\; \backslash frac\{\backslash emptyset\}\{\backslash langle\; 0,\; x,\; \backslash langle\; 1,\; x\; \backslash rangle\; \backslash rangle\}\; \backslash mid\; x\; \backslash in\; \backslash mathcal\{V\}\_\{\backslash kappa\_1\}\; \backslash right\backslash \}\; \backslash cup\; \backslash left\backslash \{\; \backslash frac\{\backslash \{\backslash langle\; 0,\; \backslash llbracket\; \backslash text\{nat\}\; \backslash rrbracket,\; v\_1\; \backslash rangle,\; \backslash langle\; 0,\; x,\; v\_2\; \backslash rangle\backslash \}\}\{\backslash langle\; 0,\; x,\; \backslash langle\; 2,\; x,\; v\_1,\; v\_2\; \backslash rangle\; \backslash rangle\}\; \backslash mid\; x,\; v\_1,\; v\_2\; \backslash in\; \backslash mathcal\{V\}\_\{\backslash kappa\_1\}\; \backslash right\backslash \},$$

$\text{app}(\llbracket \text{toto} \rrbracket, x) = \mathcal{IF}(\Phi_{\text{toto}})(0, x)$ , $\text{app}(\llbracket Y_1 \rrbracket, x) = \langle 1, x \rangle$ , and $\text{app}(\llbracket Y_2 \rrbracket, x, a, b) = \langle 2, x, a, b \rangle$ , where $x \in \mathcal{V}_{\kappa_1}$ , $a \in \text{app}(\llbracket \text{toto} \rrbracket, \llbracket \text{nat} \rrbracket)$ , and $b \in \text{app}(\llbracket \text{toto} \rrbracket, x)$ .

Example 3.9 (Inductive types with parameters). The following Coq-expression shows a typical use of parametric inductive types.

Inductive titi (x : Type) : Type :=
| Z1 : titi x
| Z2 : titi nat -> titi x -> titi x.

The inductive type titi can be represented by $\mathcal{D}_{\text{titi}} = \text{Ind}_1{\Delta_I := \Delta_C}$ , where

Then,

$${\mathrm{\Phi }}_{\text{titi}}=\{\frac{\mathrm{\varnothing }}{⟨0,x,⟨1⟩⟩}\mid x\in {\mathcal{V}}_{{\kappa }_1}\}\cup \{\frac{\{⟨0,\mathrm{⟦}\text{nat}\mathrm{⟧},v_1⟩,⟨0,x,v_2⟩\}}{⟨0,x,⟨2,v_1,v_2⟩⟩}\mid x\in {\mathcal{V}}_{{\kappa }_1},v_1,v_2\in {\mathcal{V}}_{{\kappa }_0}\},\backslash Phi\_\{\backslash text\{titi\}\}\; =\; \backslash left\backslash \{\; \backslash frac\{\backslash emptyset\}\{\backslash langle\; 0,\; x,\; \backslash langle\; 1\; \backslash rangle\; \backslash rangle\}\; \backslash mid\; x\; \backslash in\; \backslash mathcal\{V\}\_\{\backslash kappa\_1\}\; \backslash right\backslash \}\; \backslash cup\; \backslash left\backslash \{\; \backslash frac\{\backslash \{\backslash langle\; 0,\; \backslash llbracket\; \backslash text\{nat\}\; \backslash rrbracket,\; v\_1\; \backslash rangle,\; \backslash langle\; 0,\; x,\; v\_2\; \backslash rangle\backslash \}\}\{\backslash langle\; 0,\; x,\; \backslash langle\; 2,\; v\_1,\; v\_2\; \backslash rangle\; \backslash rangle\}\; \backslash mid\; x\; \backslash in\; \backslash mathcal\{V\}\_\{\backslash kappa\_1\},\; v\_1,\; v\_2\; \backslash in\; \backslash mathcal\{V\}\_\{\backslash kappa\_0\}\; \backslash right\backslash \},$$

$\text{app}(\llbracket \text{titi} \rrbracket, x) = \mathcal{IF}(\Phi_{\text{titi}})(0, x)$ , $\text{app}(\llbracket Z_1 \rrbracket, x) := \langle 1 \rangle$ , and $\text{app}(\llbracket Z_2 \rrbracket, x, a, b) := \langle 2, a, b \rangle$ , where $x \in \mathcal{V}_{\kappa_1}$ , $a \in \text{app}(\llbracket \text{titi} \rrbracket, \llbracket \text{nat} \rrbracket)$ , and $b \in \text{app}(\llbracket \text{titi} \rrbracket, x)$ .Remark 3.10. Note that in Coq, toto cannot have Type -> Set as its type, unlike titit. This difference is also reflected in their interpretations.

Example 3.11 (Mutually inductive types with parameters). Two inductive types tree and forest defined by $\mathcal{D}_{TF}$ in Remark 2.5 can be interpreted by means of the following rule set:

3.4. Interpretation of well-founded structured recursion. A set defined by a (mutual) induction generates a canonical well-founded relation on the set, i.e., the relation defined according to the inductive construction of the elements, the so-called structurally-smaller-than-relation. This is the basis for the discipline of structural recursion, which stipulates that recursive calls consume structurally smaller data.

Here, we claim the existence of the interpretations of recursive types that satisfy the soundness of the rules (fix), (fix-eq), and (ι). A formal definition is given in Appendix D. Refer to [Dybjer(1991)], whose study provides the basic idea.

Lemma 3.12. Suppose $\Gamma \vdash \mathbf{fix} f_\ell {R} : A_j$ , where

$$\begin{array}{c}{\displaystyle R=\overrightarrow{f\mathrm{/}k:A:=t},A_i\equiv \mathrm{\Pi }{\vec{x}}_i:{\vec{B}}_i\mathrm{.}{A}_i^{\mathrm{\prime }},lh({\vec{B}}_i)=k_i+1,\mathrm{\ell }\le n,}\\ {\displaystyle (\mathrm{\Gamma }⊢A_i:s_i{)}_{\mathrm{\forall }i\le n},(\mathrm{\Gamma },\vec{f}:\vec{A}⊢t_i:A_i{)}_{\mathrm{\forall }i\le n},\mathcal{F}(\vec{f},\vec{A},\vec{k},\vec{t})\mathrm{.}}\end{array}\backslash begin\{aligned\}\; R\; =\; \backslash overrightarrow\{f/k\; :\; A\; :=\; t\},\; \backslash quad\; A\_i\; \backslash equiv\; \backslash Pi\; \backslash vec\{x\}\_i\; :\; \backslash vec\{B\}\_i.\; A\text{'}\_i,\; \backslash quad\; lh(\backslash vec\{B\}\_i)\; =\; k\_i\; +\; 1,\; \backslash quad\; \backslash ell\; \backslash leq\; n,\; \backslash \backslash \; (\backslash Gamma\; \backslash vdash\; A\_i\; :\; s\_i)\_\{\backslash forall\; i\; \backslash leq\; n\},\; \backslash quad\; (\backslash Gamma,\; \backslash vec\{f\}\; :\; \backslash vec\{A\}\; \backslash vdash\; t\_i\; :\; A\_i)\_\{\backslash forall\; i\; \backslash leq\; n\},\; \backslash quad\; \backslash mathcal\{F\}(\backslash vec\{f\},\; \backslash vec\{A\},\; \backslash vec\{k\},\; \backslash vec\{t\}).\; \backslash end\{aligned\}$$

Let $\gamma \in \llbracket \Gamma \rrbracket$ be given. We suppress $\Gamma$ and $\gamma$ for better readability. Then, there is a rule set $\Psi$ such that the following interpretation of $\mathbf{fix} f_\ell {R}$ satisfies the soundness of the rules (fix), (fix-eq), and (ι):

• • $\llbracket \mathbf{fix} f_\ell {R} \rrbracket = \mathbf{lam}(h)$ , where $h(a_1, \dots, a_{k_\ell}, \langle k, \vec{z}k \rangle) = \mathcal{IF}(\Psi)(a_1, \dots, a{k_\ell}, \langle k, \vec{z}_k \rangle)$ for $\vec{a}, \langle k, \vec{z}_k \rangle \in \llbracket \vec{B}_\ell \rrbracket$ .

Remark 3.13. The condition for constrained derivation is essential. Indeed, constrained derivation corresponds to guarded recursion defined by [Giménez(1995)]; hence, it guarantees that the construction of the rule set $\Psi$ in Appendix D is well defined.

The elements of our rule sets $\Psi$ are of the form $\frac{u}{\langle \vec{x}, \langle k, \vec{y} \rangle, b \rangle}$ , where $k$ denotes the $k$ th constructor of the inductive type $d$ on which the recursion is performed, $\vec{y}$ denote the non-parametric arguments of $d$ , $\vec{x}$ denotes the list of rest arguments of the constructor, and $b$ is the result of the function. Note that $\vec{x}, \vec{y}$ could be empty.

Example 3.14 (Primitive recursion). The Coq-expression stated below is a general form of primitive recursion.

Fixpoint PRec (A:Type) (g:A) (h:nat -> A -> A) (n:nat) {struct n} : A :=
  match n with
  | 0 => g
  | S p => h p (PRec A g h p)
end.
```The corresponding term is  $\text{PRec} := \mathbf{fix} \ f_0 \{f_0/3 : B := t\}$ , where



$P = \lambda(\ell : \text{nat}). A$ ,  $h_1 = g$ , and  $h_2 = \lambda(p : \text{nat}). h p (f_0 A g h p)$ .  $\llbracket \text{PRec} \rrbracket$  is characterized by the following rule set  $\Psi_{\text{PRec}} :=$

\left\{ \frac{\emptyset}{\langle A, g, h, \langle 1 \rangle, g \rangle} \mid A \in \mathcal{V}_{\kappa_i}, g \in A, h \in \llbracket \text{nat} \rightarrow A \rightarrow A \rrbracket} \right\} \cup \left\{ \frac{\{\langle A, g, h, p, v \rangle\}}{\langle A, g, h, \langle 2, p \rangle, \mathbf{app}(h, p, v) \rangle} \mid A \in \mathcal{V}_{\kappa_i}, g \in A, h \in \llbracket \text{nat} \rightarrow A \rightarrow A \rrbracket, p \in \llbracket \text{nat} \rrbracket, v \in A \right\}.

Given a type  $A$ ,  $\llbracket \text{PRec } A \rrbracket$  denotes the primitive recursor with values from  $A$ . For instance,

$$\mathbf{a}\mathbf{p}\mathbf{p}(\mathrm{⟦}\text{plus}\mathrm{⟧},m,n)=\mathcal{I}\mathcal{F}(\text{Prec})(\mathrm{⟦}\text{nat}\mathrm{⟧},m,\mathrm{⟦}h\mathrm{⟧},n)\backslash mathbf\{app\}(\backslash llbracket\; \backslash text\{plus\}\; \backslash rrbracket,\; m,\; n)\; =\; \backslash mathcal\{IF\}(\backslash text\{Prec\})(\backslash llbracket\; \backslash text\{nat\}\; \backslash rrbracket,\; m,\; \backslash llbracket\; h\; \backslash rrbracket,\; n)$$

where  $h = \lambda(p : \text{nat}). \lambda(\ell : \text{nat}). \mathbf{S} \ell$  and  $m, n \in \llbracket \text{nat} \rrbracket$ .

**Example 3.15** (Mutually recursive functions). The interpretations of  $\text{Tsize}$  and  $\text{Fsize}$  from Remark 2.7 are characterized by the following rule set  $\Psi_{\text{size}} :=$

$$\{\frac{\{⟨A,f,v^{\mathrm{\prime }}⟩\}}{⟨A,⟨1,a,f⟩,\mathrm{⟦}\mathbf{S}{v}^{\mathrm{\prime }}\mathrm{⟧}}\mid A\in {\mathcal{V}}_{{\kappa }_0},f\in \mathbf{a}\mathbf{p}\mathbf{p}(\mathrm{⟦}\text{forest}\mathrm{⟧},A),v^{\mathrm{\prime }}\in \mathrm{⟦}\text{nat}\mathrm{⟧},a\in A\}\cup \{\frac{\mathrm{\varnothing }}{⟨A,⟨2⟩,\mathrm{⟦}\mathbf{0}\mathrm{⟧}}\mid A\in {\mathcal{V}}_{{\kappa }_0}\}\cup \{\frac{\{⟨A,t,v_1^{\mathrm{\prime }}⟩,⟨A,f^{\mathrm{\prime }},v_2^{\mathrm{\prime }}⟩\}}{⟨A,⟨3,t,f^{\mathrm{\prime }}⟩,\mathbf{a}\mathbf{p}\mathbf{p}(\mathrm{⟦}\text{plus}\mathrm{⟧},v_1^{\mathrm{\prime }},v_2^{\mathrm{\prime }})⟩}\mid A\in {\mathcal{V}}_{{\kappa }_0},t\in \mathbf{a}\mathbf{p}\mathbf{p}(\mathrm{⟦}\text{tree}\mathrm{⟧},A),f^{\mathrm{\prime }}\in \mathbf{a}\mathbf{p}\mathbf{p}(\mathrm{⟦}\text{forest}\mathrm{⟧},A),v_1^{\mathrm{\prime }},v_2^{\mathrm{\prime }}\in \mathrm{⟦}\text{nat}\mathrm{⟧}\}\mathrm{.}\backslash left\backslash \{\; \backslash frac\{\backslash \{\backslash langle\; A,\; f,\; v\text{'}\; \backslash rangle\backslash \}\}\{\backslash langle\; A,\; \backslash langle\; 1,\; a,\; f\; \backslash rangle,\; \backslash llbracket\; \backslash mathbf\{S\}\; v\text{'}\; \backslash rrbracket\}\; \backslash mid\; A\; \backslash in\; \backslash mathcal\{V\}\_\{\backslash kappa\_0\},\; f\; \backslash in\; \backslash mathbf\{app\}(\backslash llbracket\; \backslash text\{forest\}\; \backslash rrbracket,\; A),\; v\text{'}\; \backslash in\; \backslash llbracket\; \backslash text\{nat\}\; \backslash rrbracket,\; a\; \backslash in\; A\; \backslash right\backslash \}\; \backslash cup\; \backslash left\backslash \{\; \backslash frac\{\backslash emptyset\}\{\backslash langle\; A,\; \backslash langle\; 2\; \backslash rangle,\; \backslash llbracket\; \backslash mathbf\{0\}\; \backslash rrbracket\}\; \backslash mid\; A\; \backslash in\; \backslash mathcal\{V\}\_\{\backslash kappa\_0\}\; \backslash right\backslash \}\; \backslash cup\; \backslash left\backslash \{\; \backslash frac\{\backslash \{\backslash langle\; A,\; t,\; v\text{'}\_1\; \backslash rangle,\; \backslash langle\; A,\; f\text{'},\; v\text{'}\_2\; \backslash rangle\backslash \}\}\{\backslash langle\; A,\; \backslash langle\; 3,\; t,\; f\text{'}\; \backslash rangle,\; \backslash mathbf\{app\}(\backslash llbracket\; \backslash text\{plus\}\; \backslash rrbracket,\; v\text{'}\_1,\; v\text{'}\_2)\; \backslash rangle\}\; \backslash mid\; A\; \backslash in\; \backslash mathcal\{V\}\_\{\backslash kappa\_0\},\; t\; \backslash in\; \backslash mathbf\{app\}(\backslash llbracket\; \backslash text\{tree\}\; \backslash rrbracket,\; A),\; \backslash right.\; \backslash \backslash \; \backslash left.\; f\text{'}\; \backslash in\; \backslash mathbf\{app\}(\backslash llbracket\; \backslash text\{forest\}\; \backslash rrbracket,\; A),\; v\text{'}\_1,\; v\text{'}\_2\; \backslash in\; \backslash llbracket\; \backslash text\{nat\}\; \backslash rrbracket\; \backslash right\backslash \}.$$

#### 4. SET-THEORETIC MODEL AND SOUNDNESS

Since the denotations  $\llbracket \Gamma \rrbracket$  and  $\llbracket \Gamma \vdash t \rrbracket$  will be defined by mutual induction on the size of their arguments, we need a size function  $|\cdot|$  that guarantees the termination. In particular, the following properties should be satisfied:

- •  $|\Gamma| < |\Gamma \vdash A| < |\Gamma, x : A|$ ,
- •  $|\Gamma \vdash t|, |\Gamma \vdash A| < |\Gamma, x := t : A|$ ,
- •  $|\Delta_I(d)|, |\Delta_C(c)| < |\mathbf{Ind}_n\{\Delta_I := \Delta_C\} \cdot x|$  for all  $x \in \text{dom}(\Delta_I, \Delta_C)$ ,  $d \in \text{dom}(\Delta_I)$ , and  $c \in \text{dom}(\Delta_C)$ ,
- •  $|A_i|, |t_j| < |f/k : A := t|$  for all  $A_i \in \vec{A}$  and  $t_j \in \vec{t}$ .

An adequate size function can be defined by a simple extension of the one defined by [Miquel and Werner(2003)]:

- • The size  $|t|$  of a term  $t$  is (recursively) defined as the sum of the sizes of its immediate subterms plus 1.- – The immediate subterms of  $\mathbf{Ind}_n\{\Delta_I := \Delta_C\} \cdot x$  are  $\Delta_I(d)$  and  $\Delta_C(c)$ , where  $d \in \text{dom}(\Delta_I)$  and  $c \in \text{dom}(\Delta_C)$ .
- – The immediate subterms of  $\mathbf{fix} f_j \{f/k : A := t\}$  are  $\vec{A}, \vec{t}$ .
- • The size of a context  $\Gamma$  is defined as follows:
  - –  $|\llbracket \cdot \rrbracket| = 1/2$ ,
  - –  $|\Gamma, (x : t)| = |\Gamma| + |t|$ ,
  - –  $|\Gamma, (x := t : A)| = |\Gamma| + |t| + |A|$ ,
  - –  $|\Gamma, \mathbf{Ind}_n\{\Delta_I := \Delta_C\}| = |\Gamma| + 1$ .
- •  $|\Gamma \vdash t| = |\Gamma| + |t| - \frac{1}{2}$ .

**Remark 4.1.** As mentioned in Remark 3.6 and Remark 3.13, the positivity condition and the condition for constrained derivation play a crucial role for establishing the soundness proof of Theorem 4.4.

**Definition 4.2.** The set-theoretic interpretations of  $\llbracket \Gamma \rrbracket$  and  $\llbracket \gamma \vdash t \rrbracket$  are defined by a mutual induction on the size of their arguments.

(1) For each context  $\Gamma$ , the set  $\llbracket \Gamma \rrbracket$  is defined as follows:



(2) The interpretation  $\llbracket \Gamma \vdash t \rrbracket$  of a term  $t$  in a context  $\Gamma$  is a partial function defined on  $\llbracket \Gamma \rrbracket$ : Given  $\gamma \in \llbracket \Gamma \rrbracket$ ,





(\*) If  $x \in \text{dom}(\Gamma)$ , then the occurrence should be unique.

(†)  $A$  could be any term with the given property since the interpretation, when defined, is independent of it.

The following lemma is crucial for the soundness proof.**Lemma 4.3** (Substitutivity). *Let  $\Gamma$  be a context and let  $u, A$  be terms such that  $\llbracket \Gamma \vdash u \rrbracket_\gamma \in \llbracket \Gamma \vdash A \rrbracket_\gamma$  for some  $\gamma \in \llbracket \Gamma \rrbracket$  (assuming that both of them are defined), and write  $\alpha = \llbracket \Gamma \vdash u \rrbracket_\gamma$ .*

- (1) *Suppose  $(\gamma, \alpha), \delta \in \llbracket \Gamma, x : A, \Delta \rrbracket$ . Then,  $\gamma, \delta \in \llbracket \Gamma, \Delta[x \setminus u] \rrbracket$ .*
- (2) *Suppose  $(\gamma, \alpha), \delta \in \llbracket \Gamma, x : A, \Delta \rrbracket$  and  $\llbracket \Gamma, x : A, \Delta \vdash t \rrbracket_{(\gamma, \alpha), \delta} \downarrow$ . Then,*
  - •  $\llbracket \Gamma, \Delta[x \setminus u] \vdash t[x \setminus u] \rrbracket_{\gamma, \delta} \downarrow$ .
  - •  $\llbracket \Gamma, \Delta[x \setminus u] \vdash t[x \setminus u] \rrbracket_{\gamma, \delta} = \llbracket \Gamma, x : A, \Delta \vdash t \rrbracket_{(\gamma, \alpha), \delta} = \llbracket \Gamma, x := u : A, \Delta \vdash t \rrbracket_{(\gamma, \alpha), \delta}$ .

*Proof.* The assertions are proved for each  $\Delta$  and  $t$  by a mutual induction on the size of their arguments. In particular, given  $\Delta$ , the first assertion is proved before the second one for all  $t$ . In the case of  $\Delta = []$ , the claims are obvious. Assume that  $\Delta = \Delta_0, y : B$  and  $\delta = \delta_0, \beta$ . The other cases can be considered similarly.

- (1)  $(\gamma, \alpha), \delta_0, \beta \in \llbracket \Gamma, x : A, \Delta_0, y : B \rrbracket$ . Then, using the I.H. of the second claim, we have

$$\beta \in \mathrm{⟦}\mathrm{\Gamma },x:A,{\mathrm{\Delta }}_0⊢B{\mathrm{⟧}}_{\gamma ,\alpha ,{\delta }_0}=\mathrm{⟦}\mathrm{\Gamma },{\mathrm{\Delta }}_0[x\setminus u]⊢B[x\setminus u]{\mathrm{⟧}}_{\gamma ,{\delta }_0}\mathrm{.}\backslash beta\; \backslash in\; \backslash llbracket\; \backslash Gamma,\; x\; :\; A,\; \backslash Delta\_0\; \backslash vdash\; B\; \backslash rrbracket\_\{\backslash gamma,\; \backslash alpha,\; \backslash delta\_0\}\; =\; \backslash llbracket\; \backslash Gamma,\; \backslash Delta\_0[x\; \backslash setminus\; u]\; \backslash vdash\; B[x\; \backslash setminus\; u]\; \backslash rrbracket\_\{\backslash gamma,\; \backslash delta\_0\}.$$

That is,  $\gamma, \delta_0, \beta \in \llbracket \Gamma, \Delta_0[x \setminus u], y : B[x \setminus u] \rrbracket$ .

- (2) We proceed by induction on  $t$ . If  $t = x$ , the claim follows because  $\llbracket \Gamma \vdash u \rrbracket_\gamma \downarrow$  implies that  $\llbracket \Gamma, \Delta[x \setminus u] \vdash u \rrbracket_{\gamma, \delta} \downarrow$  and  $\llbracket \Gamma, \Delta[x \setminus u] \vdash u \rrbracket_{\gamma, \delta} = \llbracket \Gamma \vdash u \rrbracket_\gamma$ . This is because the interpretation of  $u$  does not depend on  $\text{dom}(\Delta)$ . Other cases can be easily shown by using induction hypotheses.

□

**Theorem 4.4** (Soundness). *Our type system is sound with respect to the set-theoretic interpretation defined in Definition 4.2 in the following sense:*

- (1) *If  $\mathcal{WF}(\Gamma)$ , then  $\llbracket \Gamma \rrbracket$  is defined.*
- (2) *If  $\Gamma \vdash M : A$ , then  $\llbracket \Gamma \rrbracket$  is defined, and for any  $\gamma \in \llbracket \Gamma \rrbracket$ , it holds that  $\llbracket \Gamma \vdash M \rrbracket_\gamma$  and  $\llbracket \Gamma \vdash A \rrbracket_\gamma$  are defined, and that*

$$\mathrm{⟦}\mathrm{\Gamma }⊢M{\mathrm{⟧}}_{\gamma }\in \mathrm{⟦}\mathrm{\Gamma }⊢A{\mathrm{⟧}}_{\gamma }\mathrm{.}\backslash llbracket\; \backslash Gamma\; \backslash vdash\; M\; \backslash rrbracket\_\backslash gamma\; \backslash in\; \backslash llbracket\; \backslash Gamma\; \backslash vdash\; A\; \backslash rrbracket\_\backslash gamma.$$

- (3) *If  $\Gamma \vdash M = N : A$ , then  $\llbracket \Gamma \rrbracket$  is defined, and for any  $\gamma \in \llbracket \Gamma \rrbracket$ , it holds that  $\llbracket \Gamma \vdash M \rrbracket_\gamma$ ,  $\llbracket \Gamma \vdash N \rrbracket_\gamma$ , and  $\llbracket \Gamma \vdash A \rrbracket_\gamma$  are defined, and that*

$$\mathrm{⟦}\mathrm{\Gamma }⊢M{\mathrm{⟧}}_{\gamma }=\mathrm{⟦}\mathrm{\Gamma }⊢N{\mathrm{⟧}}_{\gamma }\in \mathrm{⟦}\mathrm{\Gamma }⊢A{\mathrm{⟧}}_{\gamma }\mathrm{.}\backslash llbracket\; \backslash Gamma\; \backslash vdash\; M\; \backslash rrbracket\_\backslash gamma\; =\; \backslash llbracket\; \backslash Gamma\; \backslash vdash\; N\; \backslash rrbracket\_\backslash gamma\; \backslash in\; \backslash llbracket\; \backslash Gamma\; \backslash vdash\; A\; \backslash rrbracket\_\backslash gamma.$$

- (4) *If  $\Gamma \vdash M \prec N$ , then  $\llbracket \Gamma \rrbracket$  is defined, and for any  $\gamma \in \llbracket \Gamma \rrbracket$ , it holds that  $\llbracket \Gamma \vdash M \rrbracket_\gamma$  and  $\llbracket \Gamma \vdash N \rrbracket_\gamma$  are defined, and that*

$$\mathrm{⟦}\mathrm{\Gamma }⊢M{\mathrm{⟧}}_{\gamma }\subseteq \mathrm{⟦}\mathrm{\Gamma }⊢N{\mathrm{⟧}}_{\gamma }\mathrm{.}\backslash llbracket\; \backslash Gamma\; \backslash vdash\; M\; \backslash rrbracket\_\backslash gamma\; \backslash subseteq\; \backslash llbracket\; \backslash Gamma\; \backslash vdash\; N\; \backslash rrbracket\_\backslash gamma.$$

*Proof.* We proceed by a simultaneous induction over the typing derivation. The cases  $(wf)$ ,  $(ax)$ ,  $(var)$ ,  $(weak)$ , and  $(weak-eq)$  are obvious.

(II) Suppose

$$\frac{\mathrm{\Gamma }⊢A:s_1\mathrm{\Gamma },x:A⊢B:s_2}{\mathrm{\Gamma }⊢\mathrm{\Pi }x:A\mathrm{.}B:s_3}\mathrm{.}\backslash frac\{\backslash Gamma\; \backslash vdash\; A\; :\; s\_1\; \backslash quad\; \backslash Gamma,\; x\; :\; A\; \backslash vdash\; B\; :\; s\_2\}\{\backslash Gamma\; \backslash vdash\; \backslash Pi\; x\; :\; A.\; B\; :\; s\_3\}.$$

By I.H., it holds that  $\llbracket \Gamma \vdash A \rrbracket_\gamma \in \llbracket \Gamma \vdash s_1 \rrbracket_\gamma$  and  $\llbracket \Gamma, x : A \vdash B \rrbracket_{\gamma, \alpha} \in \llbracket \Gamma, x : A \vdash s_2 \rrbracket_{\gamma, \alpha}$  for all  $\alpha \in \llbracket \Gamma \vdash A \rrbracket_\gamma$ . Now, we need to show that

$$\mathrm{⟦}\mathrm{\Gamma }⊢\mathrm{\Pi }x:A\mathrm{.}B{\mathrm{⟧}}_{\gamma }\in \mathrm{⟦}\mathrm{\Gamma }⊢s_3{\mathrm{⟧}}_{\gamma }\mathrm{.}\backslash llbracket\; \backslash Gamma\; \backslash vdash\; \backslash Pi\; x\; :\; A.\; B\; \backslash rrbracket\_\backslash gamma\; \backslash in\; \backslash llbracket\; \backslash Gamma\; \backslash vdash\; s\_3\; \backslash rrbracket\_\backslash gamma.$$If  $s_2 = s_3 = \mathbf{Prop}$ , then Lemma 3.3 implies the claim. Assume  $s_1 = \mathbf{Type}_i, s_2 = \mathbf{Type}_j, s_3 = \mathbf{Type}_k$ , and  $i, j \leq k$ . Then,  $\llbracket \Gamma \vdash s_3 \rrbracket = \mathcal{V}_{\kappa_k}$ , where  $\kappa_k$  is the  $k$ th inaccessible cardinal; hence,  $\mathcal{V}_{\kappa_k}$  is closed under the power set operation.

The cases  $(\Pi\text{-eq})$ ,  $(\lambda)$ , and  $(\lambda\text{-eq})$  are obvious.

$(app)$  Suppose

$$\frac{\mathrm{\Gamma }⊢M:\mathrm{\Pi }x:A\mathrm{.}B\mathrm{\Gamma }⊢N:A}{\mathrm{\Gamma }⊢MN:B[x\setminus N]}\mathrm{.}\backslash frac\{\backslash Gamma\; \backslash vdash\; M\; :\; \backslash Pi\; x\; :\; A.\; B\; \backslash quad\; \backslash Gamma\; \backslash vdash\; N\; :\; A\}\{\backslash Gamma\; \backslash vdash\; MN\; :\; B[x\; \backslash setminus\; N]\}\; .$$

By induction hypothesis, it holds that  $\llbracket \Gamma \vdash N \rrbracket_\gamma \in \llbracket \Gamma \vdash A \rrbracket_\gamma$  and  $\llbracket \Gamma \vdash M \rrbracket_\gamma = \mathbf{lam}(f)$  for some function  $f$  with  $\text{dom}(f) = \llbracket \Gamma \vdash A \rrbracket_\gamma$  and  $f(\alpha) \in \llbracket \Gamma, x : A \vdash B \rrbracket_{\gamma, \alpha}$  for any  $\alpha \in \llbracket \Gamma \vdash A \rrbracket_\gamma$ . Thus, we have



The cases  $(app\text{-eq})$ ,  $(let)$ , and  $(let\text{-eq})$  are similar.

The soundness of  $(ind\text{-wf})$ ,  $(ind\text{-type})$ , and  $(ind\text{-cons})$  are obvious from the interpretation constructions. The interpretations of inductive types and constructors are possible because of the induction hypotheses. This is the same for  $(fix)$ ,  $(fix\text{-eq})$ ,  $(case)$ , and  $(case\text{-eq})$ .

The cases  $(ref)$ ,  $(sym)$ ,  $(trans)$ ,  $(conv)$ , and  $(conv\text{-eq})$  are obvious.

$(\beta)$  Suppose

$$\frac{\mathrm{\Gamma },x:A⊢M:B\mathrm{\Gamma }⊢A:s_1\mathrm{\Gamma },x:A⊢B:s_2\mathrm{\Gamma }⊢N:A}{\mathrm{\Gamma }⊢(\lambda x:A\mathrm{.}M)N=M[x\setminus N]:B[x\setminus N]}\mathrm{.}\backslash frac\{\backslash Gamma,\; x\; :\; A\; \backslash vdash\; M\; :\; B\; \backslash quad\; \backslash Gamma\; \backslash vdash\; A\; :\; s\_1\; \backslash quad\; \backslash Gamma,\; x\; :\; A\; \backslash vdash\; B\; :\; s\_2\; \backslash quad\; \backslash Gamma\; \backslash vdash\; N\; :\; A\}\{\backslash Gamma\; \backslash vdash\; (\backslash lambda\; x\; :\; A.\; M)N\; =\; M[x\; \backslash setminus\; N]\; :\; B[x\; \backslash setminus\; N]\}\; .$$

It remains to show that  $\llbracket \Gamma \vdash (\lambda x : A : M)N \rrbracket_\gamma = \llbracket M[x \setminus N] \rrbracket_\gamma$ :



by Lemma 4.3 because we know that  $\llbracket \Gamma \vdash N \rrbracket_\gamma \in \llbracket \Gamma \vdash A \rrbracket_\gamma$  by induction hypothesis. The judgmental equality plays a crucial role in this case.

The case  $(\delta)$  is obvious, and the case  $(\zeta)$  follows from Lemma 4.3 and induction hypothesis. The case  $(\iota)$  is obvious by definition. The cumulativity rules are obviously sound. Finally, the soundness of the the constrained typing rules in Figure 4 follows directly from the arguments stated above.  $\square$

**Theorem 4.5** (Consistency). *There is no term  $t$  such that  $\vdash t : \Pi x : *.x$ .*

*Proof.* Note that  $\llbracket \vdash \Pi x : *.x \rrbracket_{\text{nil}} = \emptyset$ .  $\square$## 5. CONCLUSION

We identified some critical issues in constructing a set-theoretic, proof-irrelevant model of CC with cumulative type universes. Our construction reconfirmed that proof-irrelevance is a subtle and difficult subject to tackle when it is combined with the subtyping of the universes, in particular,  $\mathbf{Prop} \prec \mathbf{Type}$ . We showed that the set-theoretic interpretation can be relatively easy when we work with judgmental equality. We believe that our study provides a (relatively) easy way for justifying the correctness of type theory in Martin-Löf-styled, i.e., with simple model and, in particular, no proof of the strong normalization, which is usually very difficult to establish.

Besides the historical importance of Martin-Löf-style type theory and the technical difficulties with external  $\beta$ -reduction, there is another theoretical and practical reason for studying type systems with judgmental equality. In general, the equivalence of two systems with or without judgmental equality remains an open problem. Proving the equivalence of two systems with or without judgmental equality is not a simple task, even though some positive results have been achieved by [Coquand(1991)], [Goguen(1994), Goguen(1999)], [Adams(2006)], and [Siles and Herbelin(2010)]. However, they are not sufficiently general to cover the case with cumulative type universes. Although [Adams(2006)] mentioned that it might be possible to extend his proof to more general systems with unique principal types instead of type uniqueness as in the case of Luo’s ECC [Luo(1990), Luo(1994)] and Coquand’s CIC, it still remains an open question.

A positive consequence of the work of [Adams(2006)] and [Siles and Herbelin(2010)] is that the failed attempt of [Miquel and Werner(2003)], i.e., without using sorted variables, would work if one first considers the system CC with judgmental equality and uses its equivalence to the usual CC. This is indeed the case for the model construction described in this paper, where we restrict the model construction to CC.

## ACKNOWLEDGMENT

We would like to express our sincere gratitude to Hugo Herbelin and Bruno Barras for their insightful discussions and advice. We would also like to thank the anonymous referees whose comments enabled us to improve this paper significantly.

## REFERENCES

- [Aczel(1977)] Peter Aczel. An introduction to inductive definition. In Jon Barwise, editor, *Handbook of Mathematical Logic*, pages 739–782. North-Holland, 1977.
- [Aczel(1998)] Peter Aczel. On relating type theories and set theories. In *Proceedings of Types ’98*, volume 1657 of *Lecture Notes in Comput. Sci.*, pages 1–18. Springer, 1998.
- [Adams(2006)] Robin Adams. Pure type systems with judgemental equality. *J. Funct. Program.*, 16(2): 219–246, 2006.
- [Bertot and Castéran(2004)] Yves Bertot and Pierre Castéran. *Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions*. Springer Verlag, 2004.
- [Coquand(1990)] Thierry Coquand. Metamathematical Investigation on a Calculus of Constructions. In P. Odifreddi, editor, *Logic and Computer Science*, volume 31 of APIC series, pages 91–122. Academic Press, 1990.
- [Coquand(1991)] Thierry Coquand. An algorithm for testing conversion in type theory. In *Logical frameworks*, pages 255–279. Cambridge University Press, 1991.
- [Drake(1974)] Frank R. Drake. *Set Theory: An Introduction to Large Cardinals*, volume 76 of *Studies in logic and the foundations of mathematics*. North Holland, 1974.[Dybjer(1991)] Peter Dybjer. Inductive sets and families in Martin-Löf's type theory and their set-theoretic semantics. In *Logical frameworks (Sophia-Antipolis, 1990)*, pages 280–306. Cambridge Univ. Press, 1991.

[Dybjer(2000)] Peter Dybjer. A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory. *J. Symb. Log.*, 65(2):525–549, 2000.

[Giménez(1995)] Eduardo Giménez. Codifying guarded definitions with recursive schemes. In *Types for proofs and programs (Båstad, 1994)*, volume 996 of *Lecture Notes in Comput. Sci.*, pages 39–59. Springer, 1995.

[Girard et al.(1989)Girard, Taylor, and Lafont] Jean-Yves Girard, Paul Taylor, and Yves Lafont. *Proofs and types*, volume 7 of *Cambridge Tracts in Theoretical Computer Science*. Cambridge University Press, 1989.

[Goguen(1994)] Healfdene Goguen. *A Typed Operational Semantics for Type Theory*. PhD thesis, University of Edinburgh, 1994.

[Goguen(1999)] Healfdene Goguen. Soundness of the Logical Framework for Its Typed Operational Semantics. In *Typed Lambda Calculi and Applications, TLCA'99*, pages 177–197, 1999.

[Letouzey(2004)] Pierre Letouzey. *Programmation fonctionnelle certifiée – L'extraction de programmes dans l'assistant Coq*. PhD thesis, Université Paris-Sud, July 2004.

[Luo(1989)] Zhaohui Luo. Ecc, an extended calculus of constructions. In *LICS*, pages 386–395. IEEE Computer Society, 1989.

[Luo(1990)] Zhaohui Luo. *An Extended Calculus of Constructions*. PhD thesis, University of Edinburgh, November 1990.

[Luo(1994)] Zhaohui Luo. *Computation and reasoning: a type theory for computer science*, volume 11 of *International Series of Monographs on Computer Science*. Oxford University Press, Inc., 1994.

[Martin-Löf(1984)] Per Martin-Löf. *Intuitionistic type theory*, volume 1 of *Studies in Proof Theory*. Lecture Notes. Bibliopolis, 1984.

[Miquel and Werner(2003)] Alexandre Miquel and Benjamin Werner. The not so simple proof-irrelevant model of CC. In *Types for proofs and programs*, volume 2646 of *Lecture Notes in Comput. Sci.*, pages 240–258. Springer, 2003.

[Moschovakis(1974)] Yiannis N. Moschovakis. *Elementary induction on abstract structures*, volume 77 of *Studies in logic and the foundations of mathematics*. North Holland, 1974.

[Moschovakis(1980)] Yiannis N. Moschovakis. *Descriptive set theory*, volume 100 of *Studies in logic and the foundations of mathematics*. North Holland, 1980.

[Nordström et al.(1990) Nordström, Petersson, and Smith] Bengt Nordström, Kent Petersson, and Jan M. Smith. *Programming in Martin-Löf's type theory: An introduction*. Oxford University Press, 1990.

[Paulin-Mohring(1996)] Christine Paulin-Mohring. *Définitions Inductives en Théorie des Types d'Ordre Supérieur*. Habilitation à diriger les recherches. Université Claude Bernard Lyon I, 1996.

[Reynolds(1984)] John C. Reynolds. Polymorphism is not set-theoretic. In *Semantics of Data Types*, volume 173 of *Lecture Notes in Comput. Sci.*, pages 145–156. Springer, 1984.

[Siles and Herbelin(2010)] Vincent Siles and Hugo Herbelin. Equality is typable in semi-full pure type systems. In *LICS*, pages 21–30, 2010.

[Werner(1997)] Benjamin Werner. Sets in Types, Types in Sets. In *Theoretical Aspects of Computer Software*, volume 1281 of *Lecture Notes in Comput. Sci.*, pages 530–546. Springer, 1997.

[Werner(2008)] Benjamin Werner. On the strength of proof-irrelevant type theories. *Logical Methods in Computer Science*, 4(3), 2008.APPENDIX A. DEFINITION OF FREE VARIABLES AND SUBSTITUTION

The definitions of the sets of free variables in a context or term are standard.



(\*) By using  $\alpha$ -conversion, if needed,  $y$  is assumed to be not free in  $u$  such that the variable condition is satisfied.

(†) The variable condition here implies that the names of inductive types, constructors, and recursive functions are uniquely determined, and that they will never be changed once they are defined. Thus, these names are bound variables that differ from variables bound by  $\Pi$  and  $\lambda$ .

APPENDIX B. CONSTRAINED TYPING

Note that not all fix-point definitions can be accepted because of the possibility of non-normalizing terms. If one of the arguments belongs to an inductive type, then the function starts with a case analysis, and recursive calls are performed on variables coming from patterns and representing subterms. This is the usual restriction implemented in Coq when a case distinction with respect to a distinguished inductive type in a definition of a (mutual) recursive function occurs. These restrictions are imposed by the so-called *guarded-by-destructors condition* defined by [Giménez(1995)]. Here, we follow the simplified version given by [Paulin-Mohring(1996)] by using *constrained typing*.

The constraints will be imposed with respect to a variable  $z$  and an inductive specification  $\Delta_I, \Delta_C$ , and they have three forms: the *empty constraint*  $\epsilon$ , the constraint  $<z$ , which describes the structural smallness with respect to  $z$ , and the constraint  $\Rightarrow z$ , which describes the equivalence to  $z$ . The constraints will be added to any occurrence of a variable in a term. Let  $\mathbf{c}, \mathbf{d}, \dots$  vary over constraints. The judgments of constrained typing have the form$$\begin{array}{c}
\text{Ind}_n\{\Delta_I := \Delta_C\} \in \Gamma \quad (d_i : \Pi \vec{p} : \vec{P}. A) \in \Delta_I \quad \text{lh}(\vec{p}) = n \\
\Gamma \vdash Q :^\epsilon B \quad \mathcal{C}(d_i \vec{p} : A; B) \quad \Gamma \vdash e :^\epsilon d_i \vec{p} \vec{u} \\
\Gamma \vdash h_k :^d \Pi(\vec{v} : \vec{V}_k)^{<\epsilon}. Q \vec{w}_k (c_k \vec{p} \vec{v}) \text{ for all } (c_k : \Pi \vec{p} : \vec{P}. \Pi \vec{v} : \vec{V}_k. d_i \vec{p} \vec{w}_k) \in \Delta_C \\
\hline
\Gamma \vdash \mathbf{case}(e, Q, (h_k)_k) :^d Q \vec{u} e \\
\\
\frac{\Gamma \vdash M : s}{\mathcal{WF}(\Gamma, x :^\epsilon M)} \quad \frac{\mathcal{WF}(\Gamma) \quad x :^\epsilon A \in \Gamma}{\Gamma \vdash x :^\epsilon A} \quad \frac{\Gamma \vdash t :^\epsilon A}{\Gamma \vdash t :^\epsilon A} \\
\\
\frac{\Gamma \vdash A :^\epsilon s_1 \quad \Gamma, x :^\epsilon A \vdash B :^\epsilon s_2 \quad \mathcal{P}(s_1, s_2, s_3)}{\Gamma \vdash \Pi x :^\epsilon A. B :^\epsilon s_3} \\
\\
\frac{\Gamma \vdash A = A' :^\epsilon s_1 \quad \Gamma, x :^\epsilon A \vdash B = B' :^\epsilon s_2 \quad \mathcal{P}(s_1, s_2, s_3)}{\Gamma \vdash \Pi x :^\epsilon A. B = \Pi x :^\epsilon A'. B' :^\epsilon s_3} \\
\\
\frac{\Gamma \vdash A :^\epsilon s_1 \quad \Gamma, x :^\epsilon A \vdash B :^\epsilon s_2}{\Gamma, x :^\epsilon A \vdash M :^d B} \\
\\
\frac{}{\Gamma \vdash \lambda x :^\epsilon A. M :^d \Pi x :^\epsilon A. B} \\
\\
\frac{\Gamma \vdash A = A' :^\epsilon s_1 \quad \Gamma, x :^\epsilon A \vdash B = B' :^\epsilon s_2}{\Gamma, x :^\epsilon A \vdash M = M' :^d B} \\
\\
\frac{}{\Gamma \vdash \lambda x :^\epsilon A. M = \lambda x :^\epsilon A'. M' :^d \Pi x :^\epsilon A. B} \\
\\
\frac{\Gamma \vdash M :^d \Pi x :^\epsilon A. B \quad \Gamma \vdash N :^\epsilon A}{\Gamma \vdash MN :^d B[x \setminus N]} \\
\\
\frac{\Gamma \vdash M = M' :^d \Pi x :^\epsilon A. B \quad \Gamma \vdash N = N :^\epsilon A}{\Gamma \vdash MN = M' N' :^d B[x \setminus N]}
\end{array}$$
Figure 4: Constrained typing

$\Gamma \vdash M :^\epsilon N$ , where the constraints are added to all the variables from  $\text{dom}(\Gamma)$ .  $M^\epsilon$  and  $\Gamma^\epsilon$  denote the term  $M$  and the term sequence  $\Gamma$ , respectively, where only the constraint  $\epsilon$  is added.

Given a constraint  $\mathbf{c}$ , the constraint  $<\mathbf{c}$  is defined as follows:



The following defines the restriction of a recursive call of inductive type when defining a mutual recursion. Given a declaration  $\Delta$ ,  $\Delta^{<z}$  is defined as follows:



$\Gamma^{<z}$  is defined similarly for a term sequence  $\Gamma$ . In Figure 4, we list the rules for constrained typing. The omitted rules contain only the empty constraint  $\epsilon$ .APPENDIX C. INTERPRETATION OF INDUCTIVE TYPES

Suppose  $\Gamma \vdash \mathcal{D}$ , where  $\mathcal{D} = \mathbf{Ind}_n\{\Delta_I := \Delta_C\}$ , and  $\gamma \in \llbracket \Gamma \rrbracket$ . As mentioned before, we suppress  $\Gamma$  and  $\gamma$  for better readability. Suppose that

$${\mathrm{\Delta }}_I:=d_0:A_0,\dots ,d_{\mathrm{\ell }}:A_{\mathrm{\ell }},{\mathrm{\Delta }}_C:=c_1:T_1,\dots ,c_m:T_m,\backslash Delta\_I\; :=\; d\_0\; :\; A\_0,\; \backslash dots,\; d\_\backslash ell\; :\; A\_\backslash ell,\; \backslash quad\; \backslash Delta\_C\; :=\; c\_1\; :\; T\_1,\; \backslash dots,\; c\_m\; :\; T\_m,$$

$A_i := \Pi \vec{p} : \vec{P}. \Pi \vec{b}_i : \vec{B}_i. s_i$ ,  $T_k := \Pi \vec{p} : \vec{P}. \Pi \vec{z}_k : \vec{Z}_k. d_{i_k} \vec{p} \vec{t}_k$ ,  $Z_{k,j} := \Pi \vec{u}_{k,j} : \vec{H}_{k,j}. d_{i_{k,j}} \vec{p} \vec{w}_{k,j}$ , where  $lh(\vec{p}) = n$ ,  $lh(\vec{B}_i) = \ell_i$ ,  $lh(\vec{t}_k) = \ell_{i_k}$ ,  $j \in \nu(k) := \{j \mid FV(Z_{k,j}) \cap \text{dom}(\Delta_I) \neq \emptyset\}$ , and  $i_k, i_{k,j} \leq \ell$ . Furthermore,  $\vec{Z}'_k$  is defined as



where  $d'_{i_{k,j}}$  are fresh variables. Further, we suppose that  $\llbracket \vec{P} \rrbracket, \llbracket \vec{Z}'_k \rrbracket_{\rho_k}, \dots$  are already well defined below in the definition of  $\Phi$  (This will be the case by induction hypothesis.).

Then, we set  $\llbracket \mathcal{D} \rrbracket := \mathcal{I}(\Phi)$ , where  $\Phi :=$

$$\bigcup _{i\le \mathrm{\ell }}\bigcup _{k\in {\mu }_i}\{\frac{\bigcup _{j\in {\nu }_k}\{⟨i_{k,j},\vec{p},\mathrm{⟦}{\vec{w}}_{k,j}{\mathrm{⟧}}_{\vec{p},{\vec{z}}_k,\vec{u}},\mathbf{a}\mathbf{p}\mathbf{p}(z_{k,j},\vec{u})⟩\mid \vec{u}\in \mathrm{⟦}{\vec{H}}_{k,j}{\mathrm{⟧}}_{\vec{p},{\vec{z}}_k}\}}{⟨i,\vec{p},\mathrm{⟦}{\vec{t}}_k{\mathrm{⟧}}_{\vec{p},{\vec{z}}_k},⟨k,{\vec{z}}_k⟩⟩}\mid \vec{p},{\vec{z}}_k\in \mathrm{⟦}\vec{P}\mathrm{⟧},\mathrm{⟦}{\vec{Z}}_k^{\mathrm{\prime }}{\mathrm{⟧}}_{{\rho }_k}\}\mathrm{.}\backslash bigcup\_\{i\; \backslash leq\; \backslash ell\}\; \backslash bigcup\_\{k\; \backslash in\; \backslash mu\_i\}\; \backslash left\backslash \{\; \backslash frac\{\backslash bigcup\_\{j\; \backslash in\; \backslash nu\_k\}\; \backslash \{\backslash langle\; i\_\{k,j\},\; \backslash vec\{p\},\; \backslash llbracket\; \backslash vec\{w\}\_\{k,j\}\; \backslash rrbracket\_\{\backslash vec\{p\},\; \backslash vec\{z\}\_k,\; \backslash vec\{u\}\},\; \backslash mathbf\{app\}(z\_\{k,j\},\; \backslash vec\{u\})\; \backslash rangle\; \backslash mid\; \backslash vec\{u\}\; \backslash in\; \backslash llbracket\; \backslash vec\{H\}\_\{k,j\}\; \backslash rrbracket\_\{\backslash vec\{p\},\; \backslash vec\{z\}\_k\}\backslash \}\}\{\backslash langle\; i,\; \backslash vec\{p\},\; \backslash llbracket\; \backslash vec\{t\}\_k\; \backslash rrbracket\_\{\backslash vec\{p\},\; \backslash vec\{z\}\_k\},\; \backslash langle\; k,\; \backslash vec\{z\}\_k\; \backslash rangle\; \backslash rangle\}\; \backslash mid\; \backslash vec\{p\},\; \backslash vec\{z\}\_k\; \backslash in\; \backslash llbracket\; \backslash vec\{P\}\; \backslash rrbracket,\; \backslash llbracket\; \backslash vec\{Z\}\text{'}\_k\; \backslash rrbracket\_\{\backslash rho\_k\}\; \backslash right\backslash \}.$$

Here,  $\mu_i := \{k \mid d_{i_k} = d_i\}$ , and  $\rho_k$  associates  $\mathcal{V}_{\kappa_{r(k,j)}}$  with  $d'_{i_{k,j}}$ , where  $r(k,j) := \text{rank}(d_{i_{k,j}})$ .

We also set  $\llbracket \mathcal{D} \cdot d_i \rrbracket := \mathbf{lam}(f_i)$ , where  $f_i(\vec{p}, \vec{b}_i) = \mathcal{IF}(\Phi)(i, \vec{p}, \vec{b}_i)$  for  $\vec{p}, \vec{b}_i : \llbracket \vec{P}, \vec{B}_i \rrbracket$ , and  $\llbracket \mathcal{D} \cdot c_k \rrbracket := \mathbf{lam}(g_k)$ , where  $g_k(\vec{p}, \vec{z}_k) = \langle k, \vec{z}_k \rangle$  for  $\vec{p}, \vec{z}_k : \llbracket \vec{P}, \vec{Z}_k \rrbracket$ .

APPENDIX D. INTERPRETATION OF WELL-FOUNDED STRUCTURED RECURSION

Below, we use the same notation as that used in Appendix C for the inductive types on which the recursive call is running.

Suppose  $\Gamma \vdash \mathbf{fix} f_\ell \{R\} : A_j$ , where

$$R:=\overrightarrow{f\mathrm{/}k:A:=t},A_i\equiv \mathrm{\Pi }{\vec{x}}_i:{\vec{B}}_i\mathrm{.}{A}_i^{\mathrm{\prime }},lh({\vec{B}}_i)=k_i+1,\mathrm{\ell }\le n,R\; :=\; \backslash overrightarrow\{f/k\; :\; A\; :=\; t\},\; \backslash quad\; A\_i\; \backslash equiv\; \backslash Pi\; \backslash vec\{x\}\_i\; :\; \backslash vec\{B\}\_i.\; A\text{'}\_i,\; \backslash quad\; lh(\backslash vec\{B\}\_i)\; =\; k\_i\; +\; 1,\; \backslash quad\; \backslash ell\; \backslash leq\; n,$$

$$(\mathrm{\Gamma }⊢A_i:s_i{)}_{\mathrm{\forall }i\le n},(\mathrm{\Gamma },\vec{f}:\vec{A}⊢t_i:A_i{)}_{\mathrm{\forall }i\le n},\mathcal{F}(\vec{f},\vec{A},\vec{k},\vec{t})\mathrm{.}(\backslash Gamma\; \backslash vdash\; A\_i\; :\; s\_i)\_\{\backslash forall\; i\; \backslash leq\; n\},\; \backslash quad\; (\backslash Gamma,\; \backslash vec\{f\}\; :\; \backslash vec\{A\}\; \backslash vdash\; t\_i\; :\; A\_i)\_\{\backslash forall\; i\; \backslash leq\; n\},\; \backslash quad\; \backslash mathcal\{F\}(\backslash vec\{f\},\; \backslash vec\{A\},\; \backslash vec\{k\},\; \backslash vec\{t\}).$$

Let  $\gamma \in \llbracket \Gamma \rrbracket$  be given. We suppress  $\Gamma$  and  $\gamma$  for better readability. Then,  $\llbracket \mathbf{fix} f_\ell \{R\} \rrbracket$  will depend on the  $\iota$ -reduction.

Suppose  $\Gamma \vdash \vec{a}, a_{k_\ell+1} : \vec{B}_\ell$ , where  $a_{k_\ell+1} = T_k \vec{p} \vec{u}_k$ , and  $B_{\ell,k_\ell+1} = x_{i_\ell} \vec{p} \vec{t}_k$ , i.e.,  $k \in \mu_{i_\ell}$ , and that  $\vec{a}, \vec{p}$  are all fresh variables, while  $\vec{u}_k$  represents a branch in the tree-like structure. All the free variables occurring in  $\vec{u}_k$  should be fresh. Then,  $(t_\ell[f_i \setminus (\mathbf{fix} f_i \{R\})]) \vec{a} (T_k \vec{p} \vec{u}_k)$   $\beta$ -,  $\iota$ -reduces to the term  $M_{\ell,k}$  which is obtained from the node term of the branch which  $T_k \vec{p} \vec{u}_k$  represents.

Suppose that for some  $g_{\ell,k}, h_{\ell,k} \in \mathbb{N}$ ,  $u'_1, \dots, u'_{g_{\ell,k}}, u'_{g_{\ell,k}+1}, \dots, u'_{h_{\ell,k}}$  list all the subterms of  $M_{\ell,k}$  that are structurally smaller than  $\vec{u}_k$ . Each  $u'_q$  with  $q \leq g_{\ell,k}$  occurs as the  $(k_{n_q} + 1)$ th argument of  $(\mathbf{fix} f_{n_q} \{R\})$ . Thus,

$$((\mathbf{f}\mathbf{i}\mathbf{x}{f}_{n_q}\{R\}){\vec{b}}_{n_q}{u}_q^{\mathrm{\prime }})((\backslash mathbf\{fix\}\; f\_\{n\_q\}\; \backslash \{R\backslash \})\; \backslash vec\{b\}\_\{n\_q\}\; u\text{'}\_q)$$is a subterm of  $M_{j,k}$  for some  $\vec{b}_{n_q} : B_{n_q,1}, \dots, B_{n_q,k_{n_q}}$ . Note that each  $u'_q$  is an argument of some constructor  $T_{m_q} : \Pi \vec{p} : \vec{P}. \Pi \vec{z}_{m_q} : \vec{Z}_{m_q}. x_{i_{m_q}} \vec{p} \vec{t}_{m_q}$  such that the head of  $u'_q$  is of some type  $Z_{m_q,j_q} = \Pi \vec{u}_{m_q,j_q} : \vec{H}_{m_q,j_q}. x_{i_{m_q,j_q}} \vec{p} \vec{w}_{m_q,j_q}$  and that  $x_{i_{m_q,j_q}} = x_{i_{n_q}}$  if  $q \leq g_{\ell,k}$ . Furthermore, we suppose that  $u'_{q_1}, \dots, u'_{q_h}$  are all terms among  $u'_1, \dots, u'_{h_{\ell,k}}$ , which are headed by some variables.

Thus,  $u'_{q_r} = a'_{q_r} \vec{u}'_{m_{q_r},j_{q_r}}$  for a variable  $a'_{q_r}$  of type

$$Z_{m_{q_r},j_{q_r}}=\mathrm{\Pi }{\vec{u}}_{m_{q_r},j_{q_r}}:{\vec{H}}_{m_{q_r},j_{q_r}}\mathrm{.}{x}_{i_{m_{q_r},j_{q_r}}}\vec{p}{\vec{w}}_{m_{q_r},j_{q_r}}Z\_\{m\_\{q\_r\},j\_\{q\_r\}\}\; =\; \backslash Pi\; \backslash vec\{u\}\_\{m\_\{q\_r\},j\_\{q\_r\}\}\; :\; \backslash vec\{H\}\_\{m\_\{q\_r\},j\_\{q\_r\}\}.\; x\_\{i\_\{m\_\{q\_r\},j\_\{q\_r\}\}\}\; \backslash vec\{p\}\; \backslash vec\{w\}\_\{m\_\{q\_r\},j\_\{q\_r\}\}$$

and for some terms  $\vec{u}'_{m_{q_r},j_{q_r}}$ . Note that  $a'_{q_1}, \dots, a'_{q_h}$  are exactly the free variables occurring in  $\vec{u}_k$ . Suppose that  $u'_{q_{r_1}}, \dots, u'_{q_{r_q}}$  are all such terms structurally smaller than  $u'_q$ . Then,

$$u_q^{\mathrm{\prime }}=(\lambda {\vec{u}}_{m_{q_{r_1}},j_{q_{r_1}}}:{\vec{H}}_{m_{q_{r_1}},j_{q_{r_1}}}\dots \lambda {\vec{u}}_{m_{q_{r_q}},j_{q_{r_q}}}:{\vec{H}}_{m_{q_{r_q}},j_{q_{r_q}}}\mathrm{.}{\vec{u}}_q^{\mathrm{\prime }}){\vec{u}}_{m_{q_{r_1}},j_{q_{r_1}}}^{\mathrm{\prime }}\dots {\vec{u}}_{m_{q_{r_q}},j_{q_{r_q}}}^{\mathrm{\prime }}u\text{'}\_q\; =\; (\backslash lambda\; \backslash vec\{u\}\_\{m\_\{q\_\{r\_1\}\},j\_\{q\_\{r\_1\}\}\}\; :\; \backslash vec\{H\}\_\{m\_\{q\_\{r\_1\}\},j\_\{q\_\{r\_1\}\}\}\; \backslash dots\; \backslash lambda\; \backslash vec\{u\}\_\{m\_\{q\_\{r\_q\}\},j\_\{q\_\{r\_q\}\}\}\; :\; \backslash vec\{H\}\_\{m\_\{q\_\{r\_q\}\},j\_\{q\_\{r\_q\}\}\}.\; \backslash vec\{u\}\text{'}\_q)\; \backslash vec\{u\}\text{'}\_\{m\_\{q\_\{r\_1\}\},j\_\{q\_\{r\_1\}\}\}\; \backslash dots\; \backslash vec\{u\}\text{'}\_\{m\_\{q\_\{r\_q\}\},j\_\{q\_\{r\_q\}\}\}$$

for some  $\vec{u}'_q$ . Similarly,  $M_{\ell,k}$  can be written as follows:

$$(\lambda {\vec{u}}_{m_{q_{r_1}},j_{q_{r_1}}}:{\vec{H}}_{m_{q_{r_1}},j_{q_{r_1}}}\dots \lambda {\vec{u}}_{m_{q_{r_q}},j_{q_{r_q}}}:{\vec{H}}_{m_{q_{r_q}},j_{q_{r_q}}}\mathrm{.}(\mathbf{f}\mathbf{i}\mathbf{x}{f}_{n_q}\{R\}){\vec{b}}_{n_q}{\vec{u}}_q^{\mathrm{\prime }}){\vec{u}}_{m_{q_{r_1}},j_{q_{r_1}}}^{\mathrm{\prime }}\dots {\vec{u}}_{m_{q_{r_q}},j_{q_{r_q}}}^{\mathrm{\prime }}(\backslash lambda\; \backslash vec\{u\}\_\{m\_\{q\_\{r\_1\}\},j\_\{q\_\{r\_1\}\}\}\; :\; \backslash vec\{H\}\_\{m\_\{q\_\{r\_1\}\},j\_\{q\_\{r\_1\}\}\}\; \backslash dots\; \backslash lambda\; \backslash vec\{u\}\_\{m\_\{q\_\{r\_q\}\},j\_\{q\_\{r\_q\}\}\}\; :\; \backslash vec\{H\}\_\{m\_\{q\_\{r\_q\}\},j\_\{q\_\{r\_q\}\}\}.\; (\backslash mathbf\{fix\}\; f\_\{n\_q\}\; \backslash \{R\backslash \})\; \backslash vec\{b\}\_\{n\_q\}\; \backslash vec\{u\}\text{'}\_q)\; \backslash vec\{u\}\text{'}\_\{m\_\{q\_\{r\_1\}\},j\_\{q\_\{r\_1\}\}\}\; \backslash dots\; \backslash vec\{u\}\text{'}\_\{m\_\{q\_\{r\_q\}\},j\_\{q\_\{r\_q\}\}\}$$

where

$${\vec{u}}_q^{\mathrm{\prime }}=\lambda {\vec{u}}_{m_{q_{r_1}},j_{q_{r_1}}}:{\vec{H}}_{m_{q_{r_1}},j_{q_{r_1}}}\dots \lambda {\vec{u}}_{m_{q_{r_q}},j_{q_{r_q}}}:{\vec{H}}_{m_{q_{r_q}},j_{q_{r_q}}}\mathrm{.}{\vec{u}}_q^{\mathrm{\prime }}\mathrm{.}\backslash vec\{u\}\text{'}\_q\; =\; \backslash lambda\; \backslash vec\{u\}\_\{m\_\{q\_\{r\_1\}\},j\_\{q\_\{r\_1\}\}\}\; :\; \backslash vec\{H\}\_\{m\_\{q\_\{r\_1\}\},j\_\{q\_\{r\_1\}\}\}\; \backslash dots\; \backslash lambda\; \backslash vec\{u\}\_\{m\_\{q\_\{r\_q\}\},j\_\{q\_\{r\_q\}\}\}\; :\; \backslash vec\{H\}\_\{m\_\{q\_\{r\_q\}\},j\_\{q\_\{r\_q\}\}\}.\; \backslash vec\{u\}\text{'}\_q.$$

Further, set

$${\vec{M}}_{\mathrm{\ell },k}=(\lambda {\vec{u}}_{m_{q_{r_c}},j_{q_{r_c}}}:{\vec{H}}_{m_{q_{r_c}},j_{q_{r_c}}}{)}_c\mathrm{.}(\mathbf{f}\mathbf{i}\mathbf{x}{f}_{n_q}\{R\}){\vec{b}}_{n_q}{\vec{u}}_q^{\mathrm{\prime }}\backslash vec\{M\}\_\{\backslash ell,k\}\; =\; (\backslash lambda\; \backslash vec\{u\}\_\{m\_\{q\_\{r\_c\}\},j\_\{q\_\{r\_c\}\}\}\; :\; \backslash vec\{H\}\_\{m\_\{q\_\{r\_c\}\},j\_\{q\_\{r\_c\}\}\})\_c.\; (\backslash mathbf\{fix\}\; f\_\{n\_q\}\; \backslash \{R\backslash \})\; \backslash vec\{b\}\_\{n\_q\}\; \backslash vec\{u\}\text{'}\_q$$

of type  $(\Pi \vec{u}_{m_{q_{r_c}},j_{q_{r_c}}} : \vec{H}_{m_{q_{r_c}},j_{q_{r_c}}})_c. A'_{n_q} \{ \vec{x}_{n_q} : \vec{b}_{n_q}, u'_q \}$ , where  $c$  ranges over  $1, \dots, q$ . Lastly, let  $M'_{\ell,k}$  be obtained from  $M_{\ell,k}$  by replacing  $\vec{M}_{\ell,k}$  with a fresh variable  $X_{n_q}$ .

Then,  $\bigcup_{\ell} \llbracket \mathbf{fix} f_{\ell} \{R\} \rrbracket$  will correspond to the fixpoint of the following rule set:



We set  $\llbracket \mathbf{fix} f_{\ell} \{R\} \rrbracket := \mathbf{lam}(h)$ , where  $h$  is a function such that

$$h(a_1,\dots ,a_{k_{\mathrm{\ell }}},⟨k,{\vec{z}}_k⟩)=\mathcal{I}\mathcal{F}(\mathrm{\Psi })(a_1,\dots ,a_{k_{\mathrm{\ell }}},⟨k,{\vec{z}}_k⟩)h(a\_1,\; \backslash dots,\; a\_\{k\_\{\backslash ell\}\},\; \backslash langle\; k,\; \backslash vec\{z\}\_k\; \backslash rangle)\; =\; \backslash mathcal\{IF\}(\backslash Psi)(a\_1,\; \backslash dots,\; a\_\{k\_\{\backslash ell\}\},\; \backslash langle\; k,\; \backslash vec\{z\}\_k\; \backslash rangle)$$

where  $\vec{a}, \langle k, \vec{z}_k \rangle \in \llbracket \vec{B}_{\ell} \rrbracket$ .