1. Foreword

The present paper was submitted by Erik Palmgren in September 2019 and was under review when he sadly passed away in November the same year. After discussions between the main editor (Pierre-Louis Curien), the managing editor (Thierry Coquand), and the reviewer (Peter Dybjer), it was decided to publish the paper as submitted. We think that it is an important paper, since it provides a formalized interpretation of the extensional version of Martin-Löf type theory in an intensional version and since such an interpretation has foundational significance. The draft paper is also well-written and will be published as submitted with only a few minor changes, indicated by footnotes in the text. Nevertheless, the reader should be aware that it still is a draft version.

The publication of this paper is a tribute to our dear friend and valued colleague Erik Palmgren. It is sad to realize that it will be the last in the long list of Erik’s important contribution to type theory and logic.

3. Preliminaries

We recall some definitions and facts around setoids. Note that we use the propositions-as-types principle throughout. In particular, the notion of setoid uses this principle (in contrast to, for example, setoids of the standard library in the Coq system).

3.1 Setoids

Definition 3.1 A setoid $A=(|A|,=_A)$ is type A together with an equivalence relation $=_A$ , so that $x=_Ay$ is type. A setoid map, or extensional function $f: A \rightarrow B,$ is a pair $f=(|f|, \textrm{ext}_f)$ consisting of a function $|f| : |A| \rightarrow |B|$ and $\textrm{ext}_f$ a proof of extensionality, i.e.

$$(\forall x,y : |A|)[x =_A y \Rightarrow |f|(x) =_B |f|(y)].$$

Write $a : A$ for $a : |A|$ , and $f(x) = |f|(x)$ for a setoid A and a setoid map f.

For setoids A and B, the product setoid $A\times B$ is given by

$$|A\times B| =_\textrm{def} |A| \times |B|$$

and

$$(a,b) =_{A \times B} (c,d) \Longleftrightarrow_\textrm{def} a=_A c \land b =_B d.$$

For setoids A and B, the exponent setoid $[A \rightarrow B] = B^A $ is given by

$$|B^A| =_\textrm{def} (\Sigma f: |A| \rightarrow |B|)(\forall x,y: |A|)(x=_A y \Rightarrow f(x) =_B f(y))$$

and

$$(f,p) =_{B^A} (g,q) \Longleftrightarrow_\textrm{def} (\forall x: |A|)(f(x)=_B g(x)).$$

With type universes, we may introduce some distinctions of setoids which are useful and necessary to solve predicativity problems. Let $U_n$ , $n=0,1,2,\ldots$ denote the cumulative universes of a Martin-Löf type theory, à la Russell. (In Agda and Coq these are available as Set0, Set1, Set2, … resp Type0, Type1, Type2, ….) We recall a definition and some examples from Reference PalmgrenPalmgren, (2018a ):

Definition 3.2 An (m, n)-setoid $A=(|A|,=_A)$ is a type $|A| \in U_m$ with an equivalence relation $=_A : |A| \rightarrow |A| \rightarrow U_n$ . An (n,n)-setoid will be called simply n-setoid. An $(n+1,n)$ -setoid is called an n-classoid.

As a justification for the term classoid, we note that there is a “replacement scheme”: if $f:A \rightarrow B$ is an extensional function from A, an m-setoid, to B an m-classoid, the image $\textrm{Im}(f)$ is an m-setoid. This is analogous to the replacement scheme in set theory.

Example 3.3 1. If $A \in U_n$ , then $\overline{A}=(A, \textrm{Id}_A(\cdot, \cdot))$ is an n-setoid.

2. The pair $\Omega_n = (U_n,\leftrightarrow)$ , where $\leftrightarrow$ is logical equivalence, is an n-classoid.

3. Aczel’s standard model V of CZF is built on the W-type over a universe $U_0$ with $|V| = W(U_0,T_0)$ and the equality $ =_V$ defined by bisimulation as function $|V| \rightarrow |V| \rightarrow U_0$ . Thus, $V=(|V|, =_V)$ forms a 0-classoid. Similarly, constructing $V_k$ from a universe $U_k$ , $T_k$ yields a k-classoid.

4. If A is an (m,n)-setoid and B is an (m’,n’)-setoid, then the exponential $[A \rightarrow B]$ is an $(\max(m,m',n,n'),\max(m,n'))$ -setoid. In particular, if A and B are both (m,n)-setoid, then $[A \to B]$ is an $(\max(m,n),\max(m,n))$ -setoid. Thus, (m,n)-setoids are also closed under exponents.

5. For an n-setoid A, the setoid of extensional propositional functions of level n

$$P_n(A) = [A \rightarrow \Omega_n]$$

is an n-classoid.

Subsetoids may be defined following Bishop cf. (Palmgren, Reference Palmgren2005).

Definition 3.4 Let A be a setoid. A subsetoid of A is a setoid $\delta S$ together with an injective setoid map $\iota_S : \delta S \rightarrow A$ . An element $a : A$ is said to be a member of the subsetoid $S= (\delta S, \iota_S)$ if there is an $s:\delta S$ such that $a =_A \iota_S(s)$ . We then write $a \in S$ or $a \in_A S$ . (Note that s is unique.) If S and T are subsetoids of A, then we define

(4) \begin{equation} S \subseteq_A T \Longleftrightarrow_\textrm{def} (\forall x: A)[x \in_A S \Longrightarrow x \in_A T].\end{equation}

When A is clear from the context, we drop this subscript. Define also

$$S \equiv_A T \Longleftrightarrow_\textrm{def} S \subseteq_A T \land T \subseteq_A S.$$

Using the axiom of unique choice, it can be seen that

(5) \begin{equation} S \subseteq_A T \Longleftrightarrow (\exists f: [\delta S \rightarrow \delta T])[\iota_T \circ f = \iota_S].\end{equation}

Here, f is in fact injective and unique. Whenever $(\delta S,\iota_S) \equiv_A (\delta T,\iota_T),$ there is a unique isomorphism $\phi : \delta S \to \delta T$ such that $\iota_T \circ \phi = \iota_S$ .

Definition 3.5 Let A be a fixed (m,n)-setoid. Define $\textrm{Sub}^{m,n}_{k,\ell}(A)$ to be the type of all subsetoids $(S,\iota_S)$ such that S is a $(k,\ell)$ -setoid, and the type is equipped with the equivalence relation $\equiv_A$ . Each such subsetoid is given by the data

• $|S| \in U_k$ ,

• $=_S : |S| \rightarrow |S| \rightarrow U_\ell$ ,

• $|\iota_S| : |S| \rightarrow |A|$

such that $(\forall x, y : |S|)[x=_S y \leftrightarrow \iota_S(x) =_A \iota_S(y)].$

In this paper, we will be using only the cases $\textrm{Sub}^{m,m}_{m,m}(A)$ and $\textrm{Sub}^{m+1,m}_{m,m}(A)$ , i.e. when A is an m-setoid or an m-classoid, and we are collecting the m-subsetoids. However, the levels for the general cases can be analyzed as follows.

Remark 3.6 The data of the subsetoid are captured by a $\Sigma$ -construction in the universe of level $\max(k+1,\ell+1, m, n)$ . Two subsetoids $(S,\iota_S)$ and $(T,\iota_T)$ are equal, $(S,\iota_S) \equiv_A (T,\iota_T)$ , iff $(\exists f: [S \rightarrow T])[\iota_T \circ f = \iota_S]$ and $(\exists g: [T \rightarrow S])[\iota_S \circ g = \iota_T].$ Now, $[S \rightarrow T]$ has type level $\max(k,\ell)$ and $\iota_T \circ f = \iota_S$ has level $\max(k,n)$ . The level of the equivalence relation is thus $\max(k, \ell, n)$ .

Thus, $\textrm{Sub}^{m,n}_{k,\ell}(A)$ forms a $(\max(k+1,\ell+1, m, n), \max(k, \ell, n))$ -setoid.

In particular, $\textrm{Sub}^{m,m}_{m,m}(A)$ forms a $(m+1, m)$ -setoid, i.e. an m-classoid.

Further, $\textrm{Sub}^{m+1,m}_{m,m}(A)$ forms a $(m+1, m)$ -setoid, i.e. it is also an m-classoid.

For A an m-setoid or an m-classoid, we write $\textrm{Sub}(A)$ for $\textrm{Sub}^{m,m}_{m,m}(A)$ and $\textrm{Sub}^{m+1,m}_{m,m}(A),$ respectively. Thus, in either case $\textrm{Sub}(A)$ is an m-classoid.

Example 3.7 $\textrm{Sub}({\mathbb V})$ is a 0-classoid.

3.2 Families of setoids

Definition 3.8 Let A be a setoid. A proof-irrelevant setoid family consists of a family F(a) of setoids indexed by $a : A$ , with extensional transport functions $F(p) : F(a) \to F(b)$ for each proof $p : a =_A b$ , that are satisfying

• $F(p) =_\textrm{ext} F(q)$ for each pair of proofs $p, q : a =_A b$ (proof-irrelevance)

• $F(\textrm{r}_a) = \textrm{id}_{F(a)}$ where $\textrm{r}_a : a=_A a$ is the standard proof of reflexivity.

• $F(p \odot q) = F(p) \circ F(q)$ if $q : a =_A b$ and $p : b =_A c$ , and where $p \odot q : a =_A c$ , using the standard proof $\odot$ of transitivity.

We also write $p^{-1}: b =_A a$ for $a =_A b$ using the standard proof $(-)^{-1}$ of symmetry. Note that by functoriality and proof-irrelevance

$$F(p) \circ F(p^{-1}) = F(p^{-1}) \circ F(p) = \textrm{id}_{F(a)}$$

so each F(p) is an isomorphism.

Below, we will refer to a proof-irrelevant family of setoids as just a family of setoids, when there is no chance of confusion.

Example 3.9 The operation $\kappa$ of (2) extends to a family of setoids over the classoid ${\mathbb V}$ , for $p : \alpha =_V \beta$ we let $\kappa(p): [\kappa(\alpha) \rightarrow \kappa(\beta)]$ be given by

$$\kappa(p)(x)= \pi_1(p_1(x))$$

where

$$p= (p_1, p_2): ((\Pi x: A)(\Sigma y:B) f(x) =_V g(y)) \times ((\Pi y: B)(\Sigma x:A) f(x) =_V g(y))$$

assuming $\alpha= \textrm{sup}(A,f)$ and $\beta= \textrm{sup}(B,g)$ .

Functions into power setoids give families of setoids as can be expected:

Example 3.10 Let A and X be setoids. Let $F: A \rightarrow \textrm{Sub}(X)$ be an extensional function. Then, $F(x) = (\delta(F(x)), \iota_{F(x)})$ , with $\iota_{F(x)} : \delta F(x) \to X$ injective, and for $p: x =_A y$ , there is a unique isomorphism $\phi_p : \delta(F(x)) \rightarrow \delta(F(y))$ such that

(6) \begin{equation} \iota_{F(x)} = \iota_{F(y)} \phi_p.\end{equation}

Thus, we obtain a proof-irrelevant family $F^*$ of setoids over A by letting:

$$F^*(x) := \delta(F(x)) \qquad F^*(p) := \phi_p.$$

The conditions of the transport function are easy to check.

For a setoid map $f: A \to X,$ we say f is a global member of F if for all $x : A$ , $f(x) \in_X F(x)$ . Thus for every $x:A$ , there is a unique $s : \delta(F(x))$ such that

$$f(x) =_X \iota_{F(x)}(s).$$

Thus, there is a unique function $f^* : (\Pi x : |A|)|F^*(x)|$ such that

$$f(x) =_X \iota_{F(x)}(f^*(x)).$$

If $p: x=_A y$ , then $f(x) =_X f(y)$ , so indeed

$$\iota_{F(x)}(f^*(x)) =_X \iota_{F(y)}(f^*(y)).$$

By (6) we get

$$ \iota_{F(y)}(\phi_p(f^*(x))) =_X \iota_{F(y)}(f^*(y)).$$

Now since $\iota_{F(y)}$ is injective we have $ \phi_p(f^*(x)) =_{F^*(y)} f^*(y)$ , and thus,

$$F^*(p)(f^*(x)) =_{F^*(y)} f^*(y).$$

This leads to the following definition:

Definition 3.11 Let G be a setoid family over A. A global element of G is a family $g(x) : G(x)$ of elements indexed by $x:A$ , which is extensional in the sense that

$$(\forall p : x=_A y)[G(p)(g(x)) =_{G(y)} g(y)]$$

Note that if $g=(|g|, \textrm{ext}_g) : A \to B$ is an extensional function, and F is a family on B, the we can form a family by composition $F \circ g$ on A by defining

• $(F\circ g)(x) := F(|g|(x))$ for $x : A$

• $(F\circ g)(p) := F(\textrm{ext}_g(p))$ for $p : x =_A y$ and $x, y : A$

If f is a global element of F, then $f\circ g$ is a global element of $F\circ g$ .

Definition 3.12 For F a family on A, we can form the dependent sum $\Sigma(A,F)$ and the dependent product setoid $\Pi(A,F)$ as follows

$\Sigma(A,F) = ((\Sigma x: |A|)|F(x)|, \sim)$ where

$$(x,y) \sim (u,v) := (\exists p : x =_A u)[ F(p)(y) =_{B(u)} v ]$$

$\Pi(A,F) = (P, \sim)$ where

(7) \begin{align} P := (\Sigma f : (\Pi x: &|A|)|F(x)|)(\forall x, y : A)(\forall p : x=_A y)[F(p)(f(x)) =_{B(y)} f(y) ]\\&(f, e) \sim (g, e') := (\forall x: A)[f(x) =_{B(x)} g(y)].\end{align}

Note that $\Pi(A,F)$ consists of the global elements of F.

Next, we introduce an auxiliary notion. For a classoid X and a family H of setoids over X, we define a classoid of parameterizations

$$\textrm{Par}(X,H) =((\Sigma I : | X |)|[H(I) \rightarrow X]|, =_{\textrm{Par}(X,H)}).$$

where the equivalence relation $ (I, f) =_{\textrm{Par}(X,H)} (I',f')$ is defined as

$$(\exists p: I =_X I')(\forall x : H(I))f(x) =_X f'(H(p)(x))$$

This construction is used in (8) below.

4. Basic Types

From the type universe Set in Agda, we construct Aczel’s type of iterative sets V

which corresponds to the Agda recursive data type definition

(Note that V lives in the next type universe Set1 of Agda (Set is Set0).) This definition introduces two constants, $\texttt{V}$ a code for a type, and $\texttt{sup}$ an introduction constant. Explained in terms of LF (Section 10), one can say that Agda automatically generates the corresponding elimination constant and the associated computational equality.

Define operations to extract the index type A and the ath element f(a) from the set $\textrm{sup}(A,f)$ :

$$\# \textrm{sup}(A,f) = A \qquad \textrm{sup}(A,f) \blacktriangleright a = f(a).$$

The familiar set-theoretic construction $< a, b > \; = \{\{a\},\{a, b\}\}$ of ordered pairs is used.

The natural numbers in V may be constructed as the set

$$\textrm{natV}= \textrm{sup}(N, \textrm{nV})$$

where $\textrm{nV}(0) = \emptyset$ and $\textrm{nV}(s(m)) = \{\textrm{nV}(m)\}$ . Then, it can readily be shown that $\kappa(\textrm{natV})$ is isomorphic to the standard setoid ${\mathbb N}$ of natural numbers.

The set-theoretic version of the $\Sigma$ -construction is, for $a: V$ , $g : [\kappa(a) \rightarrow {\mathbb V}]$ ,

$$\textrm{sigmaV}(a,g) = \textrm{sup}((\Sigma y: \#(a)) \#(g(y)), \lambda u. )$$

or expressed in Agda code:

Here, $\texttt{pj1} \, \texttt{u}$ and $\texttt{pj2} \, \texttt{u}$ denote the first and second projection of the $\Sigma$ -type, respectively. Further, $\texttt{VV}$ is the classoid ${\mathbb V}$ , and $\texttt{setoidmap1}$ is the type of extensional maps. The operator $\cdot$ indicates application of such maps.

Viewing $\kappa$ as a family of setoids over ${\mathbb V,}$ we define

(8) \begin{equation} \textrm{sigma}{\mathbb V} = \lambda u.\textrm{sigmaV}(\pi_1(u), \pi_2(u)) : [\textrm{Par}({\mathbb V},\kappa) \rightarrow {\mathbb V}].\end{equation}

The set-theoretic $\Pi$ -construction is more involved. For $a : V$ and $g: [\kappa(a) \rightarrow {\mathbb V}],$ define

\begin{eqnarray*}\text{piV-iV}(a, g) &=& (\Sigma f : (\Pi x : \#(a))\#(g(a))) \\& & \quad (\forall x, y : \#(a))(\forall p : x =_{\kappa(a)} y) (\kappa \circ g)(p)(f(x)) =_{(\kappa \circ g)(y)} f(y) \\\text{piV-bV}(a, g) &=& \lambda h. \textrm{sup}(\#(a), (\lambda x. < a \blacktriangleright x , g(x) \blacktriangleright (\pi_1(h)(x)) >)) \\\text{piV}(a, g) &= & \textrm{sup}(\text{piV-iV}, \text{piV-bV}(a, g)) \\\end{eqnarray*}

The first type $\text{piV-iV}(a, g)$ singles out the extensional functions employing a $\Sigma$ -type just as in (7). The branching function piV-bV then transforms such an extensional function to its graph in terms of set-theoretic pairs. Similarly to the sigma-construction, we define:

$$\textrm{pi}{\mathbb V} = \lambda u.\textrm{piV}(\pi_1(u), \pi_2(u)) : [\textrm{Par}({\mathbb V},\kappa) \rightarrow {\mathbb V}]$$

The interpretation of the extensional identity is as expected very simple: for $a:V$ and $x, y : \kappa(a)$ , let

$$\textrm{idV}(a, x, y) = \textrm{sup}((a \blacktriangleright x =_V a \blacktriangleright y), (\lambda u.a \blacktriangleright x)).$$

5. Universes

We use the type universe Set as a superuniverse (Palmgren, Reference Palmgren1998). Agda’s data construct allows building universes via a so-called simultaneous inductive-recursive definition (Dybjer, Reference Dybjer2000), such a definition has two parts, one inductive part which builds up the data part ( $\texttt{Uo}$ below) and a second part which defines a function ( $\texttt{To}$ below) by recursion on the data part. These parts may depend mutually on each other, as in the example below, where it is crucial.

To explain the above, we note that the universe

has the same closure rules as type universes à la Tarski in (Martin-Lof, 1984). In addition, it has constructors for lifting a given family A,(x)B into the universe

See Palmgren, (Reference Palmgren1998) for details.

Considering that the set universe V can be obtained by applying a W-type

to a type universe (Aczel Reference Aczel1982; Martin-Löf Reference Martin-Löf1984), we get a method for constructing a hierarchy of Aczel universes. This gives us a set universe $\textrm{sV}(I, F)$ for each family of types I, F.

The elements of the small set universe $\textrm{sV}(I, F)$ can be embedded into V

and they form a set $\textrm{uV}(I,F)$ in V

We can think of $\textrm{uV}(I,F)$ as a constructive version of an inaccessible (Rathjen et al. Reference Rathjen, Griffor and Palmgren1998). Now, iterating the universe building operator

(here $I_0$ , $F_0$ is an empty family) we then obtain an infinite hierarchy of inaccessibles

$$V_k = \textrm{uV}(I_k, F_k)$$

in V such that $V_k \in V_{k+1}$ . Each is a transitive set so $V_k \subseteq V_{k+1} \subseteq V$ . This will be the basis for the interpretation of the hierarchy of universes in extensional type theory (Martin-Löf Reference Martin-Löf1984).

6. Bracket and Quotient Types

The bracket type is a type construction which to any type A introduces a type [A] whose elements are all definitionally equal (Reference Awodey and BauerAwodey and Bauer (2004)). The idea is that [A] is the proposition corresponding to A, and [A] is inhabited if and only if A is inhabited, but [A] does not distinguish the proof objects. These properties are expressed by introduction and elimination rules, and some further equalities. See Section 8.3.8 (where the notation $\textrm{Br}(A)$ is used for [A]).

A corresponding set-theoretic construction we use for the interpretation is the “set squasher.” If $\alpha= \textrm{sup}(A,f)$ is an arbitrary set, then its squashed version is

$$\textrm{Sq}(\alpha) =_\textrm{def} \textrm{sup}(A,\lambda x. \emptyset).$$

Clearly, all its elements must be equal (to $\emptyset$ ), and also $\textrm{Sq}(\alpha)$ has an element just in case $\alpha$ has an element.

Bracket types are one extreme form of quotient types. In fact, CZF and hence its models admit general quotient sets, see, for example, Aczel and Rathjen (2000/Reference Rathjen2001). Quotient rules for extensional type theory have been formulated by Hofmann (Reference Hofmann1997, Ch. 5.1.5), Maietti (Reference Maietti2005) and for HoTT in The Univalent Foundations Program, (2013).

7. Interpretation

Now we fix the interpretation. Define the judgments on the left to have the meaning of those on the right.

(9) \begin{equation} \begin{array}{llll}&\Gamma \; \textrm{context} &\qquad & \Gamma : {\mathbb V} \\&\Gamma \Longrightarrow A \; \textrm{type} &\qquad & A : [\kappa(\Gamma) \rightarrow {\mathbb V}]\\&\Gamma \Longrightarrow A == B && A =_\textrm{ext} B : [\kappa(\Gamma) \rightarrow {\mathbb V}]\\&\Gamma \Longrightarrow a \; \textrm{raw} && a : [\kappa(\Gamma) \rightarrow {\mathbb V}] \\&\Gamma \Longrightarrow a :: A && \forall x : \kappa(\Gamma), a(x) \in_V A(x) \\& \Gamma \Longrightarrow a == b :: A && \forall x : \kappa(\Gamma), a(x)=_V b(x) \in_V A(x)\end{array}\end{equation}

Those on the right are judgments in Agda about setoids. As usual, we assume that judgments satisfy all their presuppositions.

Further, we introduce judgments for substitutions between contexts, and their corresponding interpretations

(10) \begin{equation} \begin{array}{llll}&f: \Delta \longrightarrow \Gamma &\qquad & f : [\kappa(\Delta) \rightarrow \kappa(\Gamma)] \\&f == g: \Delta \longrightarrow \Gamma &\qquad & f =_\textrm{ext} g : [\kappa(\Delta) \rightarrow \kappa(\Gamma)] \\\end{array}\end{equation}

The interpretation of application of substitutions to (raw) types and terms is given by composition

(11) \begin{equation} \begin{array}{llll}&a[f] &\qquad & a \circ f \\&A[f] &\qquad & A \circ f \\\end{array}\end{equation}

Composition of substitutions is interpreted as composition of maps

(12 \begin{equation} \begin{array}{llll}&f \frown g &\qquad & f \circ g\end{array}\end{equation}

Next, the operations for context extension $\rhd$ and the display map/left projection $\downarrow$ , last variable/right projection $\textrm{v}$ , and extension of substitutions $ \langle \; , \; \rangle$ are defined.

(13) \begin{equation} \begin{array}{llll}&\Gamma \rhd A &\qquad & \textrm{sigmaV}(\Gamma, A) \\& \downarrow(A) : \Gamma \rhd A \longrightarrow \Gamma & \qquad & \pi_1 : [\kappa(\textrm{sigmaV}(\Gamma, A)) \rightarrow \kappa(\Gamma)] \\& \Gamma \rhd A \Longrightarrow \textrm{v}_A \; \textrm{raw} & \qquad & \pi_2 : [\kappa(\textrm{sigmaV}(\Gamma, A)) \rightarrow {\mathbb V}] \\& \langle f , a \rangle_{A,p} : \Delta \longrightarrow \Gamma \rhd A& \qquad &\lambda u. < f(u) , \pi_1(p(u)) >\; : [\kappa(\Delta) \rightarrow \kappa(\textrm{sigmaV}(\Gamma, A)) ] \\\end{array}\end{equation}

here $p : (\Delta \Longrightarrow a :: A[f])$

Finally, we may introduce a judgment for equality of contexts which is interpreted as equality of sets

(14) \begin{equation} \begin{array}{llll}&\Delta == \Gamma &\qquad & \Delta =_V \Gamma \\\end{array}\end{equation}

Now by Example 3.9, each $p : \Delta =_V \Gamma$ gives an isomorphism

$$\phi_p =_\textrm{def} \kappa(p) : [\kappa(\Delta) \rightarrow \kappa(\Gamma)]$$

which is independent of p and functorial in p. Moreover, it has the property that

Some remarks about the notation to guide reading of the code. The interpretation will mainly use 0-setoids and 0-classoids, simply called setoids and classoids. Due to some limitations of Agda notation (no subscripts), we use the following notation for $a =_A a'$ and $b=_B b'$ , when A and B are, respectively, setoids and classoids

The underlying types $|A|$ and $|B|$ are denoted, respectively

When A, A’ are setoids, and B,B’ are classoids, we use the following notations for $|[A,A']|$ , $|[A,B]|$ and $|[B,B']|$

8. Interpreted Rules

The following is a list of the interpreted rules of the formalization (Section 9). The rule names refer to the Agda code.

We recall that the judgment forms are

$$\begin{array}{l@{\quad}l}\Gamma \; \text{context} & \Gamma \Longrightarrow A \; \text{type}\\\Gamma == \Delta & \Gamma \Longrightarrow A == B\\f: \Gamma \longrightarrow \Delta & \Gamma \Longrightarrow a :: A\\f == g : \Gamma \longrightarrow \Delta & \Gamma \Longrightarrow a==b :: A\end{array}$$

The following presupposition rules are valid in the model

8.1 Substitutions and general equality rules

8.2 Context extension and associated rules

Two derived rules:

8.3 Rules for particular type constructions

The general principle of Martin-Löf type theory is that each type construction comes with a formation rule, a finite number of introduction rules, one elimination rule, and computation rules. There may be additional equality rules in extended theories. Moreover, each constant has a congruence rule. If the theory is based on explicit substitution (as is the case here), there are also equality rules that state that substitutions commute with constants and abstractions.

8.3.1 $\Pi$ -rules

8.3.2 Id-rules

8.3.3 $\Sigma$ -rules

8.3.4 N-rules

Here, $\text{step-sub}(\Gamma): \Gamma \rhd \textrm{Nat}\longrightarrow \Gamma \rhd \textrm{Nat}$ is the straightforward substitution that applies the successor to the second argument.

8.3.5 $N_0$ -rules

8.3.6 $+$ -rules

Here, $\text{Sum-sub-lf}(A,B): \Gamma \rhd A \longrightarrow \Gamma \rhd \textrm{Sum}(A,B)$ and $\text{Sum-sub-rg}(A,B): \Gamma \rhd B \longrightarrow \Gamma \rhd \textrm{Sum}(A,B)$ are defined from $\textrm{lf}$ and $\textrm{rg}$ using $\langle,\rangle$ in the straightforward way.

8.3.7 Universe rules

For each $k \in {\mathbb N,}$

Footnote ¹

8.3.8 Bracket type rules

The universes are closed under bracket types

8.4 Hidden arguments

In the actual verification of the rules in Agda (Section 9), there are implicit arguments that we have hidden in the above listing of rules. For instance,

looks as follows in Agda code:

9. Formalization in Agda

This paper describes the formalization available atFootnote ²

https://github.com/peterlefanulumsdaine/palmgren-archive/tree/MSCS-2023/MLTT-and-setoids

The following files are part of the formalization we describe. Loading V-model-all-rules. agda in Agda verifies all relevant files. Agda version 2.5.2 has been used.

Basic definitions and results concerning setoids

Basic constructions and results concerning Aczel’s iterative sets

The setoid model of extensional Martin-Löf type theory

10. Comparing the Logical Framework and Agda

The Logical Framework (LF) is a dependently type lambda calculus which was designed to present dependent type theories in a compact form; see Nordström et al. (Reference Nordström, Petersson and Smith1990). There is one basic type former for dependent products (or dependent function space)

It has an introduction rule which gives the only abstraction construction for terms, together with an elimination rules which is application.

There are corresponding $\beta$ - and $\eta$ -rules. Usual syntactic conventions are used to reduce the number of parentheses $c(a_1) \cdots(a_n)$ is abbreviated as $c(a_1,\ldots,a_n)$ . If a type $\beta$ does not depend on x, $(x : \alpha) \beta$ is abbreviated as $\alpha \rightarrow \beta$ . LF has one basic dependent type which is a type universe $\textrm{Set}$ with a decoding function $\textrm{El}(\cdot)$ .

A type theory T can now be axiomatized by introducing a number of new constants $c_1,\ldots,c_m$ with types in contexts

and furthermore equations in contexts

In standard type theories, the constants are type formers, introduction and elimination constants, and the equations express the computation rules. We refer to Nordstrom et al. (1990), Ranta, (Reference Ranta1995) for elaborations of Martin-Löf type theory in this form.

The interactive proof system Agda has similar basic constructions (cf. right column)

Agda has an infinite cumulative hierarchy of type universes $\textrm{Set} = \textrm{Set}0, \textrm{Set}1, \textrm{Set}2, \ldots $ with the rules

Note that there is no explicit decoding function $\textrm{El}$ . In fact, every type in the system belongs to some $\textrm{Set}N$ for some index N. Each universe $\textrm{Set}N$ is closed under inductive-recursive definitions, which includes record types (generalized $\Sigma$ types) and recursive data types, as well as inductive families.