# The Rooster and the Syntactic Bracket

Hugo Herbelin, Arnaud Spiwack

► To cite this version:

Hugo Herbelin, Arnaud Spiwack. The Rooster and the Syntactic Bracket. 19th International Conference on Types for Proofs and Programs (TYPES 2013), Jul 2014, Toulouse, France. pp.169–187, 10.4230/LIPIcs.TYPES.2013.169 . hal-01097919

HAL Id: hal-01097919

https://inria.hal.science/hal-01097919

Submitted on 22 Dec 2014

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
# The Rooster and the Syntactic Bracket*

Hugo Herbelin¹ and Arnaud Spiwack²

1 Inria Paris-Rocquencourt
Paris, France
hugo.herbelin@inria.fr

2 Inria Paris-Rocquencourt
Paris, France
arnaud@spiwack.net

## Abstract

We propose an extension of pure type systems with an algebraic presentation of inductive and co-inductive type families with proper indices. This type theory supports coercions toward from smaller sorts to bigger sorts via explicit type construction, as well as impredicative sorts. Type families in impredicative sorts are constructed with a bracketing operation. The necessary restrictions of pattern-matching from impredicative sorts to types are confined to the bracketing construct. This type theory gives an alternative presentation to the calculus of inductive constructions on which the Coq proof assistant is an implementation.

1998 ACM Subject Classification F.3.3 Studies of Program Constructs

**Keywords and phrases** Coq, Calculus of inductive constructions, Impredicativity, Strictly positive type families, Inductive type families

Digital Object Identifier 10.4230/LIPIcs.xxx.yyy.p

## 1 Introduction

In the Coq proof assistant [14] inductive types are treated as toplevel definitions. If it makes sense from a convenience or an efficiency point of view, the monolithic nature of the definitions make it hard to describe what they precisely mean. As a matter of fact, inductive definitions mean different things depending on the type they are defined in: specifically, some types are interpreted differently in impredicative sorts like **Prop** or the impredicative variant of **Set**.

In this article, we present a calculus of inductive and co-inductive constructions where inductive and co-inductive types are presented algebraically. The algebraic presentation is an extension of a PTS [3] with inductive and co-inductive type families. Thanks to its modularity, it is meant to serve as a description which is simpler to expose and more mathematically amenable than the monolithic scheme which is found in a practical system such as Coq. For the sake of clarity, the system is given with a single universe and explicit subtyping, although Coq has an unbounded cumulative hierarchy of universes and implicit subtyping. Apart from these technicalities, it is believed that our calculus of algebraic inductive and co-inductive constructions expresses all the features of the Set-impredicative Calculus of Inductive Constructions that Coq implements, e.g. in its version 8.4 when launched with option -impredicative-set.

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

<footnote>* This research has received funding from the European Research Council under the FP7 grant agreement 278673, Project MemCAD</footnote>
<figure><img src="image_3.png" /><figcaption>Figure 1 Generic rules of PTS</figcaption></figure>

This work draws most of its inspiration from Morris & al [9, 10] for the algebraic presentation of inductive type families in a predicative sort, and Awodey & Bauer [2] for the treatment of impredicative sorts.

We use examples from Coq to illustrate the algebraic presentation. To differentiate expressions in Coq from expressions in the algebraic presentation, the former are typeset in a sans-serif font and the latter in a roman font.

## 2 Pure type systems

To model the type system of Coq, we start with the classic presentation of pure type systems (PTS) of Barendregt [3], which we will then extend to model type families. A PTS is characterised by a single syntactic category of terms which are used both as λ-terms and as types. It has a single form of typing judgment Γ ⊢ u : A, where u and A are terms, and Γ a context assigning terms to variables. A PTS has a set of sorts, which we shall denote schematically by the symbol s. Every sort is an atomic term. A PTS has a conversion relation u ≡ v. Here we diverge from the presentation of [3] which always uses β-conversion. Coq, on the other hand, uses βη-conversion on the fragment described in this section. In this article we will take the conversion rule as abstract, not even requiring it to be decidable. We will only require that it contains all the reduction rules which are given in the form u ↣ v (in this section, we only have β-reduction).

The typing rules of a PTS comprise of a set of generic rules given in Figure 1, together with a number of rules of the form

$$ \vdash s_1 : s_2 $$

called axioms, and rules of the form

$$ \frac{\Gamma \vdash A : s_1 \quad \Gamma, x:A \vdash B : s_2}{\Gamma \vdash \prod_{x:A} B : s_3} $$

of product formation rules. As usual we write $A \to B$ for $\prod_{x:A} B$ when $x$ does not bind a variable in $B$.

As a starting point of the algebraic presentation, we shall use a PTS with two sorts, Type
and □, together with the following axiom:

$$ \Gamma \vdash \text{Type} : \square $$

and the following product formation rule:

$$ \frac{\Gamma \vdash A : s_1 \quad \Gamma, x:A \vdash B : s_2}{\Gamma \vdash \prod_{x:A} B : \max s_1 s_2} $$

where $\max s = s$ and $\max \text{Type} = \max \square \text{Type} = \square$

The sorts Type and □ are predicative. The sort □ plays a technical role in allowing type variable and the formation of type-level functions; it cannot, however, be referenced in terms. In the following sections, □ will also be used to be able to define types by pattern-matching (strong elimination).

To model the entire Coq system, Type and □ would be replaced with a hierarchy of predicative sorts $Type_i$, such that

$$ \Gamma \vdash Type_i : Type_{i+1} $$

are axioms. Adapting the presentation to a hierarchy of sorts is straightforward, but in the interest of keeping to the heart of the matter we give a presentation with two sorts.

## 3 Inductive type families

We shall now extend the algebraic presentation with a notion of inductive type families to model (dependent) datatypes. In this section we will stay in the predicative fragment of Coq.

Contrary to the inductive types of Coq, where inductive definitions must be named at toplevel, like in:

**Inductive** Even : Type :=

| eo : Even

| es : Odd → Even

**with** Odd : Type :=

| os : Even → Odd.

the presentation given here is essentially anonymous, and inductive families need not be defined at toplevel prior to use. Mutually inductive types such as Even and Odd are not modelled directly, rather they are encoded using an index:

**Inductive** EvenOdd : bool → Type :=

| eo : EvenOdd true

| es : EvenOdd false → EvenOdd true

| os : EvenOdd true → EvenOdd false.

**Definition** Even := EvenOdd true.

**Definition** Odd := EvenOdd false.
4 The Rooster and the Syntactic Bracket

This encoding works as long as all the mutual definitions are all in the same sort. A variant for mutual definition involving **Type** and **Prop** is demonstrated in Section 4.3. When the types being defined are in different predicative sorts, however, we have to resort to another encoding which involves nested datatypes [4, Section 8.6].

We will not explore the latter kind of mutual definition. However, nested datatypes – where recursive calls occur as arguments of another type – such as:

**Inductive List (A:Type) : Type :=**
| nil : List A
| cons : A → List A → List A.

**Inductive Tree : Type :=**
| node : List Tree → Tree.

are indeed modelled in the algebraic presentation.

3.1 Regular types

To be able to traverse terms of inductive type, the core PTS constructions is extended with a
*recursive fixed point* on functions:

$$
\frac{
  \begin{array}{l}
    \Gamma \vdash \coprod_{x_1:A_1, \dots, x_{n-1}:A_{n-1}, x_n:A_n} B : s & \text{protected } f x_1 \dots x_{n-1} x_n u \\
    \Gamma, f : \coprod_{x_1:A_1, \dots, x_{n-1}:A_{n-1}, x_n:A_n} B, x_1:A_1, \dots, x_{n-1}:A_{n-1}, x_n:A_n \vdash u : B
  \end{array}
}{
  \Gamma \vdash \text{fix } f x_1:A_1 \dots x_{n-1}:A_{n-1} x_n:A_n \Rightarrow u : \coprod_{x_1:A_1, \dots, x_{n-1}:A_{n-1}, x_n:A_n} B
}
$$

Recursive fixed points are unfolded when fully applied

$$
(\text{fix } f x_1:A_1 \dots x_n:A_n \Rightarrow u) v_1 \dots v_n \rightsquigarrow u[x_i \setminus v_i]
$$

To ensure strong normalisation, this reduction rule is limited, and a guard condition is imposed on the recursive calls to *f*. It is not, however, the object of this article to discuss these restriction or the guard condition. Briefly, Coq currently relies on a single *structural* argument in the block *x*₁, ..., *x*ₙ: fixed points are not unfolded until their structural argument starts with a constructor, and the guard condition ensures that each recursive call is performed on a subterm of said structural argument, for a relaxed notion of subterm. Other possibilities exist: Agda2 [11] uses any number of arguments as structural, and tries to find a lexicographic ordering. Yet another possibilities is to use sized types [1]. We shall simply assume that an adequate guard condition is given.

We now extend the grammar of type constructors. The presentation of this article is largely inspired by the synthetic definition of *strictly positive families* by Morris & al [9, 10], but is adapted to *intensional type theory*. The presentation of [9, 10] is designed for generic programming inside a type theory, they give codes for strictly positive families which are then decoded into an actual type of the ambient theory. No elimination principle needs to be given for the strictly positive families, as they are implicit in their decoding. Here, we are defining the syntax of inductive type families, including their elimination rules.

The regular type constructors, whose typing rules are given in Figure 2, are the empty type 0, the unit type 1, and the sum of two types. The elimination rules are given in the form of *dependent pattern-matching* with a syntax made to remind of that of Coq. We shall
Sum type

$$ \frac{\Gamma \vdash A : \text{Type} \quad \Gamma \vdash B : \text{Type}}{\Gamma \vdash A + B : \text{Type}} $$

$$ \frac{\Gamma \vdash A + B : s \quad \Gamma \vdash t : A}{\Gamma \vdash \text{inl} t : A + B} $$

$$ \frac{\Gamma \vdash A + B : s \quad \Gamma \vdash u : B}{\Gamma \vdash \text{inr} u : A + B} $$

$$ \frac{\Gamma \vdash u : A + B \quad \Gamma, x : A + B \vdash P : s \quad \Gamma, y : A \vdash v : P[x \setminus \text{inl} y] \quad \Gamma, z : A \vdash w : P[x \setminus \text{inr} z]}{\text{match } u \text{ as } x \text{ return } P \text{ with}} $$

$$ \Gamma \vdash \left| \begin{array}{l} \text{inl} y \Rightarrow v \\ \text{inr} z \Rightarrow w \end{array} \right. : P[x \setminus u] $$

match inly as x return P with

$$ \left| \begin{array}{l} \text{inl} y \Rightarrow v \\ \text{inr} z \Rightarrow w \end{array} \right. \rightsquigarrow v[y \setminus u] $$

match inr u as x return P with

$$ \left| \begin{array}{l} \text{inl} y \Rightarrow v \\ \text{inr} z \Rightarrow w \end{array} \right. \rightsquigarrow w[z \setminus u] $$

Unit type

$$ \overline{\Gamma \vdash 1 : \text{Type}} $$

$$ \overline{\Gamma \vdash () : 1} $$

$$ \frac{\Gamma \vdash u : 1 \quad \Gamma, x : 1 \vdash P : s \quad \Gamma \vdash v : P[x \setminus ()]}{\Gamma \vdash \text{match } u \text{ as } x \text{ return } P \text{ with} : P[x \setminus u]} $$

$$ \left| \begin{array}{l} \text{match } u \text{ as } x \text{ return } P \text{ with} \\ () \Rightarrow v \end{array} \right. : P[x \setminus u] $$

$$ \text{match } () \text{ as } x \text{ return } P \text{ with} \quad \rightsquigarrow v $$

Empty type

$$ \overline{\Gamma \vdash 0 : \text{Type}} $$

$$ \frac{\Gamma \vdash u : 0 \quad \Gamma \vdash A : \text{Type}}{\Gamma \vdash \text{match } u \text{ return } A \text{ with } \cdot : A} $$

<caption>Figure 2 Regular type constructors</caption>
often omit the typing predicate when it is clear from the context, especially when it does not depend on the branch. With this material we can define a first example type, namely the booleans:

$$ \begin{cases} \mathbb{B} = 1 + 1 \\ \text{true} = \text{inl} () \\ \text{false} = \text{inr} () \end{cases} $$

## 3.2 Inductive type families

Inductive families differ from regular inductive types in that they are parametrised by *indices*, that is they are functions $F: A \to \text{Type}$ for some $A$. An inductive family of the form $\lambda x^A.R$, is said to be *uniformly parametrised* by $A$. In general, inductive families are not uniformly parametrised: the value of the index is allowed to vary in recursive calls, and constructors may build values of $F x$ for certain $x$ only. Remember, for instance, the *EvenOdd* family:

$$ \begin{array}{l} \textbf{Inductive} \ EvenOdd : \mathbf{bool} \to \mathbf{Type} := \\ \quad | eo : EvenOdd true \\ \quad | es : EvenOdd false \to EvenOdd true \\ \quad | os : EvenOdd true \to EvenOdd false. \end{array} $$

The inductive family constructors, presented in Figure 3, warrant individual discussion. First, notice that as a simplifying hypothesis, inductive families have exactly one index. This is, of course, not a limitation in expressive power as multiple indices can be encoded as a dependent sum, and the unit type allows us to write families without an index.

The construction $\mu X^{A \to \text{Type}}. F$ constructs the *inductive fixed point* of $F$. It acts on type families, because indices vary through recursive calls to $X$. To be able to form an inductive fixed point, occurrences of $X$ must be strictly positive in $F$, rules for strict positivity are given in Figure 4. The rules of Figure 4 are a simple set which suits the needs of this article, however in practice, we may want to consider strict positivity rules involving elimination rules and a finer treatment of application. Strict positivity ensures that no non-terminating term can be written without recursive fixed points, so that the guard condition suffices to enforce termination. Paradoxes which can be derived from non-positive or non-strictly positive inductive fixed points can be found in [13, Chapter 4, Section 4.2][8, Chapter 3][4, Chapter 8]. To avoid clutter, we give a presentation where inductive fixed points can be freely rolled and unrolled thanks to the conversion. An alternative can be to give an explicit term constructor for fixed points, see Section 3.4.

We will also use an inductive fixed point on nullary families, defined as:

$$ \mu X^{\text{Type}}. F = (\mu Y^{1 \to \text{Type}}. F[X \setminus Y ()]) () $$

from which we have that $\mu X^{\text{Type}}. F$ can be freely rolled from or unrolled to $F[X \setminus \mu X^{\text{Type}}. F]$.

With inductive fixed points, we can, for instance, define the accessibility predicate. In Coq:

$$ \begin{array}{l} \textbf{Inductive} \ Acc (A:\mathbf{Type}) (R:A \to A \to \mathbf{Type}) (x:A) : \mathbf{Type} := \\ | acc\_intro : (\mathbf{forall} \ y:A, R \ y \ x \to Acc A R y) \to Acc A R x. \end{array} $$
## Inductive fixed point

$$ \frac{\Gamma \vdash A : s \quad \Gamma, X:A \to \text{Type} \vdash F : A \to \text{Type} \quad \mathbf{sp}_X F}{\Gamma \vdash \mu X^{A \to \text{Type}}. F : A \to \text{Type}} $$

$$ \mu X^{A \to s}. F \equiv F[X \setminus \mu X^{A \to s}. F] $$

## Proper indices

$$ \frac{\Gamma \vdash A : \text{Type} \quad \Gamma \vdash B : \text{Type} \quad \Gamma, x:A \vdash T : \text{Type} \quad \Gamma, x:A \vdash f : B}{\Gamma \vdash \sum_{x:A}^f T : B \to \text{Type}} $$

$$ \frac{\Gamma \vdash \sum_{x:A}^f T : B \to s \quad \Gamma \vdash u : A \quad \Gamma \vdash v : T[x \setminus u]}{\Gamma \vdash (u, v)_{x:A,T}^f : (\sum_{x:A}^f T)(f[x \setminus u])} $$

$$ \frac{\Gamma \vdash u : (\sum_{x:A}^f T)b \quad \Gamma, y:B, z: (\sum_{x:A}^f T)y \vdash P : s \quad \Gamma, i:A, j:T i \vdash v : P[y \setminus f i, z \setminus (i,j)_{x:A,T}^f]}{\Gamma \vdash \text{match } u \text{ as } z \text{ in } y \text{ return } P \text{ with } |(i,j)_{x:A,T}^f \Rightarrow v : P[y \setminus b, z \setminus u]} $$

$$ \text{match } (u, v)_{x:A,T}^f \text{ as } z \text{ in } y \text{ return } P \text{ with } |(i, j)_{x:A,T}^f \Rightarrow w \rightsquigarrow w[i \setminus u, j \setminus v] $$

<caption>Figure 3 Inductive type families</caption>

$\overline{\mathbf{sp}_X y}$

$\overline{\mathbf{sp}_X 0}$

$\overline{\mathbf{sp}_X 1}$

$$ \frac{X \text{ is fresh in } A \quad \mathbf{sp}_X B}{\mathbf{sp}_X (\prod_{x:A} B)} $$

$$ \frac{\mathbf{sp}_X A \quad \mathbf{sp}_X B}{\mathbf{sp}_X (A + B)} $$

$$ \frac{X \text{ is fresh in } A \quad \mathbf{sp}_X F}{\mathbf{sp}_X (\mu Y^A . F)} $$

$$ \frac{X \text{ is fresh in } A \quad \mathbf{sp}_X T}{\mathbf{sp}_X (\lambda x^A . T)} $$

$$ \frac{\mathbf{sp}_X U \quad X \text{ is fresh in } t}{\mathbf{sp}_X (U t)} $$

$$ \frac{\mathbf{sp}_X B \quad B \equiv A}{\mathbf{sp}_X A} $$

$$ \frac{X \text{ is fresh in } f \quad \mathbf{sp}_X A \quad \mathbf{sp}_X T}{\mathbf{sp}_X (\sum_{x:A}^f T)} $$

<caption>Figure 4 Strict positivity condition</caption>
This type represents the generic form of termination proofs: any terminating recursive fixed
point can be made structural over a proof of accessibility. In the algebraic presentation, it is
defined as:

$$
\left\{
\begin{array}{l}
\mathrm{Acc} = \lambda A^{\mathrm{Type}} R^{A \to A \to \mathrm{Type}} . \mu \mathrm{Acc}^{A \to \mathrm{Type}} . \lambda x^A . \prod_{y:A} R y x \to \mathrm{Acc} y \\[1em]
\mathrm{acc}_{\mathrm{intro}} = \lambda A^{\mathrm{Type}} R^{A \to A \to \mathrm{Type}} x^A f \prod_{y:A} R y x \to \mathrm{Acc} A R y . f
\end{array}
\right.
$$

Because inductive fixed points are treated transparently, the constructor is rather trivial. However, notice how, in the definition of Acc, the parameter *x* is treated differently from *A* and *R*. The reason is that *A* and *R* are *uniform parameters*, in that they do not vary through recursive calls, whereas *x* does: it is a *non-uniform parameter*. The parameter *x* is, hence, represented as an index. However, such an index is not sufficient to encode types like *EvenOdd*.

Representing proper indices requires a new type construction, which we write $\sum_{x:A}^f T$. This construction comes from [9, 10], where it is inspired by a categorical point of view: in a sufficiently extensional setting, $\sum_{x:A}^f T$ is the right adjoint to a pullback functor. The similarity with the usual notation of dependent sum is not fortuitous, indeed we can define dependent sum as a special case of proper indexing:

$$
\left\{
\begin{array}{l}
\sum_{x:A} B = \left( \sum_{x:A} {}^{(0)} B \right) {}(0) \\[1em]
(u, v)_{x:A.B} = (u, v)_{x:A.B}^{(0)}
\end{array}
\right.
$$

We also write $A \times B$ and $(u, v)$ for $\sum_{x:A} B$ and $(u, v)_{x:A.B}$, respectively, when $x$ is not free in $B$.

In the case of dependent sums, the index is trivial. When it is not, however, the pattern matching return clause *P* is allowed to depend on the value of the index. This is the purpose of Coq’s in-pattern. With the algebraic presentation, the in-pattern has the pleasant property of being confined to the proper indexing construction, hopefully making its meaning more explicit. The syntax differs a little from that of Coq, however: Coq renders the in clause as a pattern with the type name at the head:

match n as n' in EvenOdd b return P n' b with

...

end.

In the algebraic presentation, types not having a name, the in clause simply consists of a
name for the index.

The prototype of proper indexing is the identity type, which we name Eq. In Coq:

**Inductive Eq (A:Type) (x:A) : A → Type :=**
| eq_refl : Eq A × x

in the algebraic presentation:

$$
\left\{
\begin{array}{l}
\mathrm{Eq} = \lambda A^{\mathrm{Type}} x^A . \sum_{\_:-1}^{x} 1 \\[1em]
\mathrm{eq}_{\mathrm{refl}} = \lambda A^{\mathrm{Type}} x^A . (((),())^x)_{\_:-1.1}
\end{array}
\right.
$$
In fact, dependent sums and identity types are sufficient to define proper indexing. Indeed $\sum_{x:A} T$ can be redefined as:

$$ \left\{ \begin{array}{l} \sum_{x:A}^{f} T = \lambda y^B \cdot \sum_{x:A} (\mathrm{Eq} \ B \ y \ f) \times T \\ (u, v)_{x:A.T}^{f} = (u, (\mathrm{eq}_{\mathrm{refl}} B \ f[x \setminus u], v))_{x:A.(\mathrm{Eq} \ B(f[x \setminus u])f) \times T} \end{array} \right. $$

It is closer to the spirit of Coq, but in no way essential, to take a proper indexing construction rather than equality as primitive. In Morris & al [9, 10], the dependent sum and equality of the ambient type theory is used to define $\sum_{x:A} T$ which is then taken as primitive.

An other choice lies in the use of $A+B$ as primitive. It is the only type construction which allows to define a type with distinct elements. However, a common alternative is to take $\mathbb{B}$ as primitive, in which case we can define $A+B$ as:

$$ \left\{ \begin{array}{l} A + B = \sum_{b:\mathbb{B}} \left| \begin{array}{l} \text{match } b \text{ with} \\ \quad \text{true} \Rightarrow A \\ \quad \text{false} \Rightarrow B \end{array} \right. \\ \text{inl} = \lambda x^A . (\text{true}, x) \quad \left| \begin{array}{l} \text{match } b \text{ with} \\ \quad \text{true} \Rightarrow A \\ \quad \text{false} \Rightarrow B \end{array} \right. \\ \text{inr} = \lambda y^B . (\text{false}, y) \quad \left| \begin{array}{l} \text{match } b \text{ with} \\ \quad \text{true} \Rightarrow A \\ \quad \text{false} \Rightarrow B \end{array} \right. \end{array} \right. $$

### 3.3 Examples

The previous section concludes the description of the predicative fragment of the algebraic presentation. We can now give definitions of the remaining inductive families we have encountered in terms of the algebraic presentation. Starting with EvenOdd:

$$ \begin{array}{l} \textbf{Inductive} \ EvenOdd : \mathbf{bool} \to \mathbf{Type} := \\ \quad | eo : \mathbf{EvenOdd} \ true \\ \quad | es : \mathbf{EvenOdd} \ false \to \mathbf{EvenOdd} \ true \\ \quad | os : \mathbf{EvenOdd} \ true \to \mathbf{EvenOdd} \ false. \end{array} $$

translates, in the algebraic presentation, to:

$$ \left\{ \begin{array}{l} \mathrm{EvenOdd} = \mu \mathrm{EvenOdd}^{\mathbb{B} \to \mathrm{Type}} . \left( \sum_{\_1}^{\mathrm{true}} 1 + \mathrm{EvenOdd} \ \mathrm{false} \right) + \left( \sum_{\_1}^{\mathrm{false}} \mathrm{EvenOdd} \ \mathrm{true} \right) \\ \quad \mathrm{eo} = \mathrm{inl} (((), \mathrm{inl} ((), \_1)), \_1) \\ \quad \mathrm{es} = \lambda x^{\mathrm{EvenOdd} \ \mathrm{false}} . \mathrm{inl} (((), \mathrm{inr} x)_{\_1}, \_1) \\ \quad \mathrm{os} = \lambda x^{\mathrm{EvenOdd} \ \mathrm{true}} . \mathrm{inr} (((), x)_{\_1}, \_1) \end{array} \right. $$

Here is the definition of List in Coq:

$$ \begin{array}{l} \textbf{Inductive} \ List (A:\mathbf{Type}) : \mathbf{Type} := \\ \quad | \mathbf{nil} : \mathbf{List} A \\ \quad | \mathbf{cons} : A \to \mathbf{List} A \to \mathbf{List} A. \end{array} $$
and in the algebraic presentation:

$$
\left\{
\begin{array}{l}
\text{List} = \lambda A^{\text{Type}}. \mu \text{List}^{\text{Type}}. 1 + A \times \text{List} \\
\text{nil} = \lambda A^{\text{Type}}. \text{inl} () \\
\text{cons} = \lambda A^{\text{Type}} x^A l^{\text{List } A}. \text{inr} (x, l)
\end{array}
\right.
$$

Finally the definition of Tree :

$$
\begin{array}{l}
\textbf{Inductive Tree : Type} := \\
\quad | \text{node} : \text{List Tree} \to \text{Tree}.
\end{array}
$$

translates to:

$$
\left\{
\begin{array}{l}
\text{Tree} = \mu \text{Tree}^{\text{Type}}. \text{List Tree} \\
\text{node} = \lambda f^{\text{List Tree}}. f
\end{array}
\right.
$$

Note that in the definition of Tree, we must $\beta$-reduce List Tree for the recursive definition to be strictly positive.

A more complex example is given by the type of lists indexed by their length, often called
vectors:

$$
\begin{array}{l}
\textbf{Inductive Nat : Type} := \\
\quad | o : \text{Nat} \\
\quad | s : \text{Nat} \to \text{Nat}.
\end{array}
$$

$$
\begin{array}{l}
\textbf{Inductive Vector (A:\textbf{Type}) : Nat} \to \textbf{Type} := \\
\quad | \text{vnil} : \text{Vector A o} \\
\quad | \text{vcons} : \textbf{forall } n, A \to \text{Vector A } n \to \text{Vector A } (s n).
\end{array}
$$

It is encoded in the algebraic presentation as:

$$
\left\{
\begin{array}{l}
\text{Nat} = \mu \text{Nat}^{\text{Type}}. 1 + \text{Nat} \\
\qquad o = \text{inl} () \\
\qquad s = \lambda n^{\text{Nat}}. \text{inr } n \\
\\
\text{Vector} = \lambda A^{\text{Type}}. \mu V^{\text{Nat} \to \text{Type}}. \lambda n^{\text{Nat}}. \left( \sum_{i:1}^{o} 1 \right) n + \left( \sum_{n':\text{Nat}} s^{n'} A \times V n' \right) n \\
\\
\text{vnil} = \lambda A^{\text{Type}}. \text{inl} (((), ()))^{o}_{\_1 1} \\
\\
\text{vcons} = \lambda A^{\text{Type}} n^{\text{Nat}} a^A v^{\text{Vector } n a}. \text{inr} (n, (a, v))^{s n'}_{n' : \text{Nat}}. A \times V n'
\end{array}
\right.
$$

Contrary to proper indices, the types of non-uniform parameters are allowed to be in $\square$,
this allows the definition of types such as the binary lists [12]:

$$
\begin{array}{l}
\textbf{Inductive BList (A:\textbf{Type}) : Type} := \\
\quad | \text{one} : A \to \text{BList } A \\
\quad | \text{twice} : \text{BList } (A*A) \to \text{BList } A \\
\quad | \text{stwice} : A \to \text{BList } (A*A) \to \text{BList } A
\end{array}
$$
which are rendered in the algebraic presentation as:

$$
\left\{
\begin{array}{l}
\text{BList} = \mu\text{BList}^{\text{Type} \to \text{Type}}. \lambda A^{\text{Type}}. A + (\text{BList}(A \times A) + A \times (\text{BList}(A \times A))) \\
\text{one} = \lambda A^{\text{Type}} x^A. \text{inl} x \\
\text{twice} = \lambda A^{\text{Type}} l^{\text{BList}(A \times A)}. \text{inr} (\text{inl} l) \\
\text{stwice} = \lambda A^{\text{Type}} x^A l^{\text{BList}(A \times A)}. \text{inr} (\text{inr}(a, l))
\end{array}
\right.
$$

In Coq, where there is a hierarchy of universe, types of proper indices can be in any sort.
However, a proper index whose type is in Typeᵢ constrains the final type to be in Typeᵢ₊₁
or higher. Uniform parameters, of any type, do not constrain the type they parametrise.

Inductive types are consumed by recursive fixed points. Using the implicit unfolding of inductive fixed points, we can pattern-match over the top constructor directly. The Coq function

Fixpoint add (x y:Nat) : Nat :=
match y with
  | o ⇒ x
  | s y' ⇒ s (add x y')
end

is rendered in the algebraic presentation as

$$
\text{add} = \text{fix} \ \text{add} \ x:\text{Nat} \ y:\text{Nat} \Rightarrow \left| \begin{array}{l} \text{match } y \text{ as } \_ \text{ return Nat with} \\ \quad \text{inl } \Rightarrow x \\ \quad \text{inr } y' \Rightarrow s (\text{add } x y') \end{array} \right.
$$

3.4 Co-induction

In addition to inductive fixed points, Coq also has support for co-inductive fixed points.
Co-inductive fixed points are required to be strictly positive, like inductive fixed points. We
choose in this section, a presentation of co-inductive data where fixed points are explicitly
introduced with a constructor. Below we will use this explicit presentation to give a variation
on Coq's co-inductive fixed points.

$$ \frac{\Gamma \vdash A : s \quad \Gamma, X : A \to \text{Type} \vdash F : A \to \text{Type} \quad \text{sp}_X F}{\Gamma \vdash \nu X^{A \to \text{Type}} . F : A \to \text{Type}} $$

$$ \frac{\Gamma \vdash \nu X^{A \to s} . F : A \to s \quad \Gamma \vdash i : A \quad \Gamma \vdash u : F [ X \setminus \nu X^{A \to s} . F ] i}{\Gamma \vdash \text{forced } u : ( \nu X^{A \to s} . F ) i} $$

$$ \frac{\Gamma \vdash \nu X^{A \to s} . F : A \to s \qquad \Gamma \vdash i : A \qquad \Gamma \vdash u : (\nu X^{A \to s} . F) i}{\Gamma, x : (\nu X^{A \to s} . F) i \vdash P : s' \qquad \Gamma, y : F [X \setminus \nu X^{A \to s} . F] i \vdash v : P[x \setminus \text{forced } y]} $$

$$ \Gamma \vdash \left| \begin{array}{l} \text{match } u \text{ as } x \text{ return } P \text{ with} \\ \text{forced } y \Rightarrow v \end{array} \right. : P[x \setminus u] $$

$$ \text{match forced } u \text{ as } x \text{ return } P \text{ with} \\ \qquad \underset{\text{forced } y \Rightarrow v}{\sim} v[y \setminus u] $$

Just like inductive data is *destructed* by a recursive fixed point operation, co-inductive data is *constructed* by a co-recursive fixed point operation, allowing co-inductive data to be infinite. The guard condition on co-recursive fixed points ensures that a finite number of unfolding will eventually produce a forced value.

$$ \frac{\Gamma \vdash \prod_{x_1:A_1, \dots, x_n:A_n} (\nu X^{A \to s} . F) i : s \qquad \text{coguarded } f x_1 \dots x_n u}{\Gamma, f : \prod_{x_1:A_1, \dots, x_n:A_n} (\nu X^{A \to s} . F) i, x_1:A_1, \dots, x_n:A_n \vdash u : (\nu X^{A \to s} . F) i}{\Gamma \vdash \text{cofix } f x_1:A_1 \dots x_n:A_n \Rightarrow u : \prod_{x_1:A_1, \dots, x_n:A_n} (\nu X^{A \to s} . F) i} $$

Co-recursive fixed-point are meant to represent infinite data: they cannot be unfolded eagerly, lest they would fail to terminate. They are unfolded only when they appear at the head of a pattern-matching expression:

$$ \begin{array}{l} \text{match } (\text{cofix } f x_1:A_1 \dots x_n:A_n \Rightarrow u) v_1 \dots v_n \text{ as } x \text{ return } P \text{ with} \\ \qquad \underset{\text{forced } y \Rightarrow v}{\mid} \\ \text{match } u[f \setminus (\text{cofix } f x_1:A_1 \dots x_n:A_n \Rightarrow u), x_i \setminus v_i] \text{ as } x \text{ return } P \text{ with} \\ \qquad \underset{\text{forced } y \Rightarrow v}{\sim} \end{array} $$

The dependent elimination rule for co-inductive fixed points asserts, in essence, that every co-inductive data is of the form forced $u$. Even though it would be fine for inductive fixed points – this is why we could leave the unrolling to the conversion – this does not reflect well the computational aspects of co-inductive data: suspended co-recursive fixed points are values, and won't be evaluated until the context demands it. The fact that the elimination for co-inductive data claims that all values are forced gives rise to undesirable behaviour.

Take for instance the following simple co-inductive type, and data:

$$ \begin{cases} T = \nu X \cdot X \\ i = \text{cofix } i \Rightarrow \text{forced } i \end{cases} $$
So that $i$ is effectively an infinite sequence of forced. Using the elimination principle above, it is possible to give a closed proof that Eq $T i$ (forced $i$):

$$ \begin{array}{l} \text{match } i \text{ as } x \text{ return Eq } T x \left( \text{forced} \left( \begin{array}{l} \text{match } x \text{ with} \\ \mid \text{forced } y \Rightarrow y \end{array} \right) \right) \text{ with} \\ \mid \text{forced } y \Rightarrow \text{eq}_{\text{refl}} T y \end{array} $$

However, $i$ and (forced $i$) are not convertible, yet, as every closed proof of equality does, this proof reduces to $\text{eq}_{\text{refl}}$, hence should relate convertible terms. The dependent elimination rule of co-inductive fixed points compromises the type safety of the logic.

Coq uses the above dependent elimination rule for co-inductive fixed points. It was a deliberate decision made for practical purposes. Nonetheless, one may want to weaken it to avoid the incompatibility between equality and conversion. To do so, it suffices to erase the dependency of the return predicate over the matched term:

$$ \frac{\Gamma \vdash \nu X^{A \to s}. F : A \to s \quad \Gamma \vdash i : A \quad \Gamma \vdash u : (\nu X^{A \to s}. F) i \quad \Gamma \vdash P : s' \quad \Gamma \vdash v : P}{\Gamma \vdash \begin{array}{l} \text{match } u \text{ return } P \text{ with} \\ \mid \text{forced } y \Rightarrow v \end{array} : P} $$

## 4 Prop

With all the common baggage for predicative sorts set in place, we can add impredicative sorts to the algebraic presentation. The main such sort in Coq is the sort **Prop** of propositions. The design of **Prop** is guided by *proof irrelevance*: even if it is not actually provable in Coq, different proofs of a proposition are thought of as being equal. This property is useful for program extraction: only the *computationally relevant* parts of a program need to be executed to get the final result. In other words: propositions are considered as *static* data. It is why, with disjunction and existential defined as:

**Inductive Or (A B:Prop) : Prop** :=

| or_introl : A → A ∨ B

| or_intror : B → A ∨ B.

**Inductive Ex (A:Type) (P:A→Prop) : Prop** :=

| ex_intro : **forall** x:A, P x → Ex A P.

the following terms are refused by type-checking:

**match x with**

| or_introl _ ⇒ true

| or_intror _ ⇒ false

**end.**

and

**match x with**

| ex_intro x _ ⇒ x

**end.**
14 The Rooster and the Syntactic Bracket

On the other hand, it is not the case of every inductive type defined in **Prop**, that they
cannot be eliminated into **Type**. Conjunction and falsity are two counter-examples:

**Inductive** False : **Prop** := .

**Inductive** And (A B:Prop) : Prop :=

$$
| \text{conj} : A \to B \to A \wedge B.
$$

Coq allows elimination over these two propositions into **Type**, and both following terms are
well-typed:

match x return Bool with end.

and

match x with

$$
| conj \_ \_ \Rightarrow true
$$

end.

The object of this section is to make syntactically explicit what happens when an inductive
type of Coq is declared to be of sort **Prop**. The description elaborated in this section has
strong similarities with the system of bracket-types proposed by Awodey & Bauer [2]. They
describe the propositions as the subset of types with at most one element, and introduce a
left adjoint, written as brackets, to the inclusion of propositions into types. We will reuse
their notation, even though, in our intensional setting, **T:Prop** does not enforce that **T** has a
most one element, and the bracketing operation does not properly form an adjunction with
the inclusion from **Prop** to **Type**.

**4.1 Impredicativity**

Let us start by introducing the new sort Prop in the algebraic presentation:

$$
\Gamma \vdash \mathrm{Prop} : \mathrm{Type}
$$

As in [2], propositions form a subset of types. Coq has a subtyping rule (also known as *cumulativity*) to make the inclusion transparent. We will, however, render it with a syntactic construct:

$$
\frac{\Gamma \vdash A : \mathbf{Prop}}{\Gamma \vdash \{A\} : \mathbf{Type}}
$$

$$
\frac{\Gamma \vdash u : A}{\Gamma \vdash \mathrm{prf} \ u : \{A\}}
$$

$$
\frac{
  \begin{array}{l}
    \Gamma \vdash u : \{A\} \quad \Gamma, x : \{A\} \vdash P : s \quad \Gamma, y : A \vdash v : P[x \setminus u] \\
    \text{match } u \text{ as } x \text{ return } P \text{ with } : P[x \setminus u] \\
    | \text{prf } y \Rightarrow v
  \end{array}
}{
  \Gamma \vdash
  \begin{array}{l}
    \text{match } u \text{ as } x \text{ return } P \text{ with } : v[y \setminus u] \\
    | \text{prf } y \Rightarrow v
  \end{array}
}
$$

$$
\frac{
  \begin{array}{l}
    \text{match } \text{prf } u \text{ as } x \text{ return } P \text{ with } : v[y \setminus u] \\
    | \text{prf } y \Rightarrow v
  \end{array}
}{
  \Gamma \vdash
  \begin{array}{l}
    \text{match } \text{prf } u \text{ as } x \text{ return } P \text{ with } : v[y \setminus u] \\
    | \text{prf } y \Rightarrow v
  \end{array}
}
$$
$$ \Gamma \vdash 0 : \text{Prop} $$

$$ \Gamma \vdash 1 : \text{Prop} $$

$$ \frac{\Gamma \vdash A : \text{Prop} \quad \Gamma \vdash B : \text{Prop} \quad \Gamma, x:A \vdash T : \text{Prop} \quad \Gamma, x:A \vdash f : B \quad \Gamma \vdash \sum_{x:A}^f T : B \to \text{Prop}} $$

Figure 5 Singleton rules

This definition simply makes {$A$} a synonym of $A$, except of sort Type. It is strictly positive in $A$:

$$ \frac{\mathit{sp}_X A}{\mathit{sp}_X \{A\}} $$

The fact that Prop is impredicative – i.e. supports the following product formation rules:

$$ \frac{\Gamma \vdash A : s \quad \Gamma, x:A \vdash B : \text{Prop}}{\Gamma \vdash \prod_{x:A} B : \text{Prop}} $$

is easily understood in terms of proof irrelevance. Indeed, if for all $x$, $B$ has at most one element, so has the product over $x$. Even though it uses functional extensionality, which is not provable.

## 4.2 Singleton rules

The types which (ideally) preserve the proof irrelevance property are sometimes called singleton types in the setting of Coq. In our algebraic presentation, they correspond to inductive type family constructors with extra formation rules to make them preserve propositions. The rules are shown in Figure 5. This elucidates why Coq allows elimination over **False** and **And** into arbitrary type: **False** is implemented as $0$ and **And A B** and $A \times B$. The elimination rules being unchanged, pattern-matching over proofs of **False** and **And** are unrestricted. Because restricted pattern-matching is often seen as the default, singleton types are said to enjoy *singleton elimination*.

Remark that, proofs of propositions being uninformative, there is essentially nothing to be gained from depending on, or being indexed over a proposition. In consequence, the type formation rule for proper indexing in Figure 5 is only useful, in practice, for the subcase of cartesian product.

Coq actually implements two other singleton rules. The first one is for inductive fixed points. In our algebraic presentation:

$$ \frac{\Gamma \vdash A : s \quad \Gamma, X:A \to \text{Prop} \vdash F : A \to \text{Prop} \quad \mathit{sp}_X F}{\Gamma \vdash \mu X^{A \to \text{Prop}}. F : A \to \text{Prop}} $$

It allows to type the accessibility predicate Acc in Prop. This rule is sound in that fixed points indeed preserve proof irrelevance in presence of functional extensionality. It is also very useful for extraction: structural recursion over Acc allows the definition of functions
whose termination cannot be proved automatically by the guard condition. However, the proof is no longer needed to ensure termination in the target languages of extraction. In this sense, at least, it is static data.

The last singleton rule allows properly indexed families in Prop (not how it is stronger than the rule dependent sum of Figure 5):

$$ \frac{\Gamma \vdash A : \text{Prop} \quad \Gamma \vdash B : \text{Type} \quad \Gamma, x:A \vdash T : \text{Prop} \quad \Gamma, x:A \vdash f : B}{\Gamma \vdash \sum_{x:A}^f T : B \rightarrow \text{Prop}} $$

It turns the identity type Eq into a proposition. It is known to be sound to accept that Eq is proof irrelevant [6]. It is also useful for extraction, as equal types, in a closed environment, are extracted to the same type. Hence a program may safely eliminate over Eq knowing that it will not affect the performances of the extracted code. In Coq, the index B in the rule above can be of any sort Type<sub>i</sub>, however, this wisdom has been challenged in recent years with the formulation of the *univalence principle* [15], of which a simple consequence is that Eq is *not* proof irrelevant at every type. Indeed, some extracted Coq programs written assuming the univalence principle crash.

To correct for the univalence principle, the singleton rule for proper indices can be simply dropped; but it can also be restricted to the lowest sort: B : Type<sub>0</sub>. More precisely the conjunction of the univalence principle and the proof irrelevance principle is consistent as long as the singleton rule of proper indices is restricted to sorts s such that there is no sort s' other than Prop such that s' : s. Because, if such a sort s' exists, B : s' and by univalence, Eq B has two distinct elements contradicting proof irrelevance.

For types which do not enjoy singleton elimination, turning them into propositions means restricting their elimination. We achieve this effect by adding a single type construction coercing from Type to Prop:

$$ \frac{\Gamma \vdash A : \text{Type}}{\Gamma \vdash [A] : \text{Prop}} $$

$$ \frac{\Gamma \vdash u : A}{\Gamma \vdash \langle u \rangle : [A]} $$

$$ \frac{\Gamma \vdash u : [A] \quad \Gamma, x : [A] \vdash P : \text{Prop} \quad \Gamma, y : A \vdash v : P[x \setminus \langle y \rangle]}{\Gamma \vdash \left[ \begin{array}{l} \text{match } u \text{ as } x \text{ return } P \text{ with} \\ \quad \langle y \rangle \Rightarrow v \end{array} \right]} $$

$$ \text{match } \langle u \rangle \text{ as } x \text{ return } P \text{ with } \quad \begin{array}{l} \leadsto v[y \setminus u] \\ \quad \langle y \rangle \Rightarrow v \end{array} $$

The important rule is the elimination rule, where the return clause is limited to be of sort Prop, whereas every other type construction can be eliminated to any sort. Apart from this restriction [A] is a synonym of A, except in Prop. In [2], the type theory is extensional, in that the identity type and the conversion relation coincide. The elimination rules for bracket is much finer and reflects precisely the fact that propositions are proof-irrelevant. In an intensional type theory, restricting with respect to sorts approximates this behaviour: even if we constrained propositions to be proof-irrelevant, not every proof irrelevant type will have
type Prop. The bracketing construction is also strictly positive:

$$ \frac{\mathrm{sp}_X A}{\mathrm{sp}_X [A]} $$

It is actually possible, using only the impredicative dependent product to define a bracketing operation: $\prod_{P:\mathrm{Prop}} (A \to P) \to P$. Like $[A]$ it behaves as $A$ except it can only be used to form a proposition. However, the impredicative encoding is positive but not strictly, which motivates the introduction of the extra construction.

## 4.3 Examples

The logical connectives can be defined as follows:

$$
\left\{
\begin{array}{l}
\text{False} = 0 \\
\text{And} = \lambda A^{\text{Prop}} B^{\text{Prop}}. A \times B \\
\text{pair} = \lambda A^{\text{Prop}} B^{\text{Prop}} x^A y^B. (x, y) \\
\text{Or} = \lambda A^{\text{Prop}} B^{\text{Prop}}. [A + B] \\
\text{or\_introl} = \lambda A^{\text{Prop}} B^{\text{Prop}} x^A. \langle \mathrm{inl} x \rangle \\
\text{or\_intror} = \lambda A^{\text{Prop}} B^{\text{Prop}} y^B. \langle \mathrm{inr} y \rangle \\
\mathrm{Ex} = \lambda A^{\text{Type}} P^{A \to \mathrm{Prop}}. \left[ \sum_{x:A} P x \right] \\
\mathrm{ex\_intro} = \lambda A^{\text{Type}} P^{A \to \mathrm{Prop}} x^A p^P x. \langle (x, p) \rangle_{x:A,P}
\end{array}
\right.
$$

Note how, because of the brackets, existentials and disjunctions are prohibited from being eliminated to non-propositional types. Thanks to the singleton rules, however, conjunction and falsity do not require brackets.

As a final example, consider the type Ascending n p of ascending sequences of integers between p and n defined by mutual recursion with the proposition Ge m p which stands from m is greater than or equal to p:

$$
\begin{array}{l}
\textbf{Inductive} \textbf{Ascending} : \text{Nat} \to \text{Nat} \to \textbf{Type} := \\
\quad \mid \textbf{top} : \textbf{forall} \ n, \textbf{Ascending} \ n \ n \\
\quad \mid \textbf{up} : \textbf{forall} \ n \ p \ m, \text{Ge} \ m \ (s \ p) \to \textbf{Ascending} \ n \ m \to \textbf{Ascending} \ n \ p \\
\quad \textbf{with} \ \text{Ge} : \text{Nat} \to \text{Nat} \to \textbf{Prop} := \\
\quad \quad \mid \textbf{ascend} : \textbf{forall} \ m \ p, \textbf{Ascending} \ m \ p \to \text{Ge} \ m \ p.
\end{array}
$$

As Ascending has type Type, whereas Ge has type Prop, the translation to a single inductive type is not as straightforward as Even and Odd. The translation requires the use of brackets around the recursive calls:

$$
\left\{
\begin{array}{l}
\mu X^{(\mathrm{Nat} \times \mathrm{Nat}) + (\mathrm{Nat} \times \mathrm{Nat})} \to \mathrm{Type}. \lambda i^{(\mathrm{Nat} \times \mathrm{Nat}) + (\mathrm{Nat} \times \mathrm{Nat})} \\
\text{AscendingGe} = \\
\quad + \left( \sum_{n:\mathrm{Nat}}^{\mathrm{inl}(n,n)} 1 \right) i \\
\quad + \left( \sum_{j:\mathrm{Nat} \times \mathrm{Nat}}^{\mathrm{inl}j} \sum_{m:\mathrm{Nat}} [X(\mathrm{inr}(m, s(\pi_2 j)))] \times X(\mathrm{inl}(\pi_1 j, m)) \right) i \\
\quad + \left( \sum_{j:\mathrm{Nat} \times \mathrm{Nat}}^{\mathrm{inr}j} X(\mathrm{inl}j) \right) i \\
\text{Ascending} = \lambda n p. \text{AscendingGe}(\mathrm{inl}(n, p)) \\
\text{Ge} = \lambda m p. [\text{AscendingGe}(\mathrm{inr}(m, p))]
\end{array}
\right.
$$
## 5 Impredicative Set

In addition to the impredicative sort Prop, Coq has a sort Set which is predicative by default but can be turned impredicative with a flag. Where Prop is meant to be used in the context of separating static and dynamic information, the spirit of the impredicative sort Set is to be as powerful as possible without being inconsistent. In the algebraic presentation, that means being stable by every construction except dependent sums with the first projection in an arbitrary sort (*strong sums*).

To mirror the optional nature of the impredicativity of Set, the rules for a predicative sort Set are given in Figure 6; to turn impredicativity on, the rules of Figure 7 must be used *in addition* to those of predicative Set. This presentation makes immediately apparent that impredicative Set is an extension of predicative Set, in that every program of the latter typechecks in the former.

The rules of Set are the same as those of Prop, with the exception of $A + B$ which is in Set when both $A$ and $B$ are – even with predicative Set. Hence, there are types in Set with several elements – e.g. $\mathbb{B}$. As a consequence, the bracketing operation which coerces types in Type to Set does not enjoy an explanation in terms of proof irrelevance, as was the case in Prop. As a matter of fact, there is no clear set-theoretical description at all. A close cousin of Set bracketing, however, can be found in homotopy type theory [15], where, roughly, groupoids are *truncated* to sets through a quotient of their homsets by the total relation.

## 6 Conclusion

The algebraic presentation of Coq makes the conversion between sorts explicit. The toplevel inductive definitions of Coq can be understood as implicitly inserting canonical bracketing operations when an inductive type is declared inside an impredicative sort but should be of a different sort due to its form; and inserting type coercion from a smaller sort to a bigger sort when applying a cumulativity rule.

Monolithic type definitions like in Coq have a number of advantages over the algebraic presentation, they boil down to better type errors due to naming, better type inference and better memory representation due to *n*-ary sums and products. However, the value of the implicit coercions between sorts is less clear. In particular, the bracketing operation to impredicative sorts is probably a better guide for program extraction than the current method of figuring whether or not a given type is a proposition, which interacts badly with universe polymorphism [7]. Explicit coercions for extraction are also in the spirit of [5].

All of the algebraic type constructors can actually be defined in Coq, except the two fixed-points because there is no way to abstract over strictly positive type families. So is it clear that expressions of the algebraic presentation which do not use inductive or co-inductive fixed points can be translated into Coq. Occurrences of the fixed points in a type must be $\lambda$-lifted and given a toplevel name. Some care must be given to avoiding the duplication of such definitions otherwise types which must be convertible for the expression to typecheck, might be seen as different in the Coq translation. Apart from this technicality, translation from the algebraic presentation to Coq is straightforward. We claim that, at least if we extend the algebraic presentation to a hierarchy of universes and the strict positivity condition is made a bit more fine-grained, Coq terms can be, conversely, translated into the algebraic presentation.
$$ \frac{\Gamma \vdash A : \text{Set} \quad \Gamma, x:A \vdash B : \text{Set}}{\Gamma \vdash \coprod_{x:A} B : \text{Set}} $$

$$ \frac{\Gamma \vdash A : \text{Set} \quad \Gamma, x:A \vdash P : \text{Set}}{\Gamma \vdash \sum_{x:A} P : \text{Set}} $$

$$ \frac{\Gamma \vdash A : \text{Set} \quad \Gamma \vdash B : \text{Set}}{\Gamma \vdash A + B : \text{Set}} \qquad \frac{\Gamma \vdash 1 : \text{Set}}{\Gamma \vdash 0 : \text{Set}} $$

$$ \frac{\Gamma \vdash A : s \quad \Gamma, X:A \to \text{Set} \vdash F : A \to \text{Set} \quad \mathbf{sp}_X F}{\Gamma \vdash \mu X^{A \to \text{Set}}. F : A \to \text{Set}} $$

$$ \frac{\Gamma \vdash A : \text{Set} \quad \Gamma \vdash B : \text{Set} \quad \Gamma, x:A \vdash T : \text{Set} \quad \Gamma, x:A \vdash f : B}{\Gamma \vdash \sum_{x:A}^f T : B \to \text{Set}} $$

$$ \frac{\Gamma \vdash A : s \quad \Gamma, X:A \to \text{Set} \vdash F : A \to \text{Set} \quad \mathbf{sp}_X F}{\Gamma \vdash \nu X^{A \to \text{Set}}. F : A \to \text{Set}} $$

$$ \frac{\Gamma \vdash A : \text{Set}}{\Gamma \vdash \{A\}_{\text{Set}} : \text{Type}} \qquad \frac{\Gamma \vdash u : A}{\Gamma \vdash \text{elt } u : \{A\}_{\text{Set}}} $$

$$ \frac{\Gamma \vdash u : \{A\}_{\text{Set}} \quad \Gamma, x:\{A\}_{\text{Set}} \vdash P : s \quad \Gamma, y:A \vdash v : P[x \setminus \text{elt } y]}{\Gamma \vdash \begin{array}{l} \text{match } u \text{ as } x \text{ return } P \text{ with} \\ \qquad \text{elt } y \Rightarrow v \end{array} : P[x \setminus u]} $$

$$ \frac{\text{match } \text{elt } u \text{ as } x \text{ return } P \text{ with} \quad \text{elt } y \Rightarrow v}{\text{elt } y \Rightarrow v} \rightsquigarrow v[y \setminus u] $$

$$ \frac{\mathbf{sp}_X A}{\mathbf{sp}_X \{A\}_{\text{Set}}} $$

<caption>Figure 6 Rules for predicative Set</caption>
$$ \frac{\Gamma \vdash A : s \quad \Gamma, x:A \vdash B : \text{Set}}{\Gamma \vdash \prod_{x:A} B : \text{Set}} $$

$$ \frac{\text{sp}_X A}{\text{sp}_X [A]_{\text{Set}}} $$

$$ \frac{\Gamma \vdash A : \text{Type}}{\Gamma \vdash [A]_{\text{Set}} : \text{Set}} $$

$$ \frac{\Gamma \vdash u : A}{\Gamma \vdash \langle u \rangle_{\text{Set}} : [A]_{\text{Set}}} $$

$$ \frac{\Gamma \vdash u : [A]_{\text{Set}} \quad \Gamma, x:[A]_{\text{Set}} \vdash P : \text{Set} \quad \Gamma, y:A \vdash v : P[x \setminus \langle y \rangle_{\text{Set}}]}{\Gamma \vdash \left| \langle y \rangle_{\text{Set}} \Rightarrow v \right. : P[x \setminus u]} $$

$$ \frac{\text{match } \langle u \rangle_{\text{Set}} \text{ as } x \text{ return } P \text{ with } \quad \left| \langle y \rangle_{\text{Set}} \Rightarrow v \right. : v[y \setminus u]}{\text{match } \langle u \rangle_{\text{Set}} \text{ as } x \text{ return } P \text{ with } \quad \left| \langle y \rangle_{\text{Set}} \Rightarrow v \right. : v[x \setminus u]} $$

<caption>Figure 7 Rules for impredicative Set</caption>

References

1 Andreas Abel. *A polymorphic lambda-calculus with sized higher-order types*. PhD thesis, 2006.

2 Steve Awodey and Andrej Bauer. Propositions as [Types]. *Journal of Logic and Computation*, 14(4):447–471, August 2004.

3 Henk Barendregt. Lambda calculus with types. *Handbook of logic in computer science*, 1992.

4 Bruno Barras. Semantical Investigations in Intuitionistic Set Theory and Type Theories with Inductive Families. *Thèse d'Habilitation*, 2013.

5 Bruno Barras and Bruno Bernardo. The implicit calculus of constructions as a programming language with dependent types. *Foundations of Software Science and Computational Structures*, 4962:365–379, 2008.

6 Gyesik Lee and Benjamin Werner. Proof-irrelevant model of CC with predicative induction and judgmental equality. 2011.

7 Pierre Letouzey and Bas Spitters. Implicit and noncomputational arguments using monads. pages 1–16, 2005.

8 Peter Morris. *Constructing Universes for Generic Programming*. PhD thesis, 2007.

9 Peter Morris and Thorsten Altenkirch. Constructing strictly positive families. *CATS '07 Proceedings of the thirteenth Australasian symposium on Theory of computing*, pages 111–121, 2007.

10 Peter Morris, Thorsten Altenkirch, and Neil Ghani. A universe of strictly positive families. *International journal of foundations of computer science*, pages 83–107, 2009.

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

12 Chris Okasaki. *Purely functional data structures*. 1999.

13 Christine Paulin-Mohring. *Définitions inductives en théorie des types d'ordre supérieur*. PhD thesis, Université Claude Bernard-Lyon I, 1996.

14 The Coq development team. The Coq Proof Assistant.

15 The Univalent Foundations Program. *Homotopy Type Theory: Univalent Foundations of Mathematics*.