# The very dependent recursive structure of iterated parametricity in indexed form

Hugo Herbelin, Ramkumar Ramachandra

► To cite this version:

Hugo Herbelin, Ramkumar Ramachandra. The very dependent recursive structure of iterated parametricity in indexed form. 2026. hal-05498288

HAL Id: hal-05498288

https://inria.hal.science/hal-05498288v1

Preprint submitted on 12 Feb 2026

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 CC BY 4.0 - Attribution - International License
# The very dependent recursive structure of iterated parametricity in indexed form

Hugo Herbelin

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

Université Paris Cité, Inria, CNRS, IRIF, Paris

Ramkumar Ramachandra

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

Unaffiliated

## Abstract

Reynolds' parametricity originally equips types with proof-irrelevant binary propositional relations over the types. But such relations can also be taken proof-relevant or unary, and described either in an indexed or fibred way. Parametricity can be iterated, and when types are sets, this results in an interpretation of sets as augmented simplicial sets in the unary case, or cubical sets in the binary case.

In earlier work, equations were given describing the *n*-ary iterated parametricity translation of sets in indexed form. The construction was formalised in Rocq by induction on a large structure embedding equational reasoning.

The current work analyses the dependency structure of the earlier work leading to a presentation of the construction replacing equational reasoning with definitional reasoning. The new construction is very dependent, based on an induction that requires interleaving the specification of the induction hypothesis and the construction of the induction step. At the same time, the construction reduces to its computational essence and can be described in full detail, closely following the new machine-checked formalisation.

2012 ACM Subject Classification 10003752.10003790.10011740

Keywords and phrases Parametricity, Semi-simplicial sets, Semi-cubical sets, Formalization, Rocq, Indexed-fibred correspondence

Digital Object Identifier 10.4230/LIPIcs...

# 1 Introduction

## Parametricity and its ramifications

Introduced by Reynolds in the context of programming language semantics [17], relational parametricity is connected to several similar concepts in logic and mathematics. In its original formulation, it associates binary propositional relations to types. The variant in [7] associates proof-relevant binary relations to types, and the variant in [4] associates relations of arbitrary arity to types. This includes the case of unary relations which assigns predicates to types in the proof-irrelevant case, and families to types in the proof-relevant case. The unary relation case expresses what it means to belong in a type, and the binary relation case expresses what it means to be observationally equal in a type. The canonical predicate associated to $A \to B$ is the predicate over functions $f$ in $A \to B$ such that, for all $a$ in the canonical predicate associated to $A$, $f(a)$ is in the canonical predicate associated to $B$. Similarly, the canonical relation associated to $A \to B$ is the relation over functions $f$ and $f'$ in $A \to B$ such that, for all $a$ and $a'$ related through the canonical relation associated to $A$, $f(a)$ and $f'(a')$ are related through the canonical relation associated to $B$.

Unary parametricity over a language is an extreme form of realisability using the language itself as language of realisers. As such, it relates to *reducibility*, also known as *Tait computability* [18], which is a semantic form of realisability. In the same vein, binary parametricity over a language can be seen as defining *logical relations* [16] over itself, since logical relations are a binary form of reducibility.

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

© Hugo Herbelin and Ramkumar Ramachandra;
licensed under Creative Commons License CC-BY 4.0

Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
## XX:2 The very dependent recursive structure of iterated parametricity in indexed form

Parametricity, like realisability, reducibility, and logical relations, is commonly expressed in *indexed* form. Let us use a type-theoretic language featuring a type of subsingleton types called *HProp* and a type of sets *HSet*. Then, predicates have type $A \to HProp$, families have type $A \to HSet$, relations have type $A \times A \to HProp$, and relevant relations, sometimes called *correspondences*, have type $A \times A \to HSet$. All constructions in indexed form can also be expressed in the *fibred* form, via the indexed-fibred correspondence: there is an equivalence between $A \to HProp$ and $\Sigma B : HSet.(B \xrightarrow{\text{inj}} A)$ in the proof-irrelevant case, and between $A \to HSet$ and $\Sigma B : HSet.(B \to A)$ in the proof-relevant case, for $A : HSet$. A fibred approach to parametricity was considered in [2], who also suggested to iterate parametricity.

### Iterated parametricity

The internalisation of parametricity in unary indexed form was studied in [5] leading to a type theory of iterated parametricity. Such a type theory can be interpreted in the "unary" form of cubical sets [3]. Cubical sets, in their standard definition as presheaves over a cubical category, can be seen as living on the fibred side of iterated parametricity.<fnref n="1" /> This was particularly emphasised in [13] which interprets cubical sets as higher-dimensional parametricity in fibred form. While iterated binary parametricity produces semi-cubical sets, it was also observed that iterated unary parametricity produces augmented semi-simplicial sets.<fnref n="2" />

<table><thead><tr><th>arity</th><th>style</th><th>iteration</th><th>relevance</th><th>logical structure</th></tr></thead><tbody><tr><td rowspan="6">unary</td><td rowspan="3">indexed</td><td>non-iterated</td><td>proof-irrelevant</td><td>predicate</td></tr><tr><td>non-iterated</td><td>relevant</td><td>family</td></tr><tr><td>iterated</td><td>relevant</td><td><i>this work</i></td></tr><tr><td rowspan="3">fibred</td><td>non-iterated</td><td>proof-irrelevant</td><td>subobject</td></tr><tr><td>non-iterated</td><td>relevant</td><td>fibration</td></tr><tr><td>iterated</td><td>relevant</td><td>augmented semi-simplicial set</td></tr><tr><td rowspan="4">binary</td><td rowspan="3">indexed</td><td>non-iterated</td><td>proof-irrelevant</td><td>relation</td></tr><tr><td>non-iterated</td><td>relevant</td><td>correspondence</td></tr><tr><td>iterated</td><td>relevant</td><td><i>this work</i></td></tr><tr><td>fibred</td><td>non-iterated</td><td>proof-irrelevant</td><td>fibred relation</td></tr><tr><td></td><td></td><td>non-iterated</td><td>relevant</td><td>span</td></tr><tr><td></td><td></td><td>iterated</td><td>relevant</td><td>semi-cubical set</td></tr></tbody></table>

### Iterated parametricity in indexed form

An informal description of semi-simplicial sets in indexed form was given in [14]. Several formal definitions in type theory were later proposed [19, 9, 15, 1]. In the previous work, a notion of *v*-sets generalising augmented semi-simplicial and semi-cubical sets and reflecting *v*-ary iterated parametricity was given [10], together with a construction of *v*-sets in *indexed*

<footnote n="1">¹ Interestingly, this contrasts with the case of Grothendieck construction where presheaves live on the indexed side and fibrations on the fibred side</footnote>

<footnote n="2">² The authors learned it from Hugo Moeneclaey and Thorsten Altenkirch</footnote>
form. As an example, for $v = 2$, instead of semi-cubical sets in fibred form, a family of relevant relations was used.

$$ X_0 : \mathbf{HSet} \leftarrow \partial^R - \leftarrow \partial^L - X_1 : \mathbf{HSet} \leftarrow \partial^{\star R} - \leftarrow \partial^{\star L} - \leftarrow \partial^{R\star} - X_2 : \mathbf{HSet} \dots \quad \text{(fibred)} $$

$$ \begin{array}{l} E_0 : \mathbf{HSet} \\ E_1 : E_0 \times E_0 \to \mathbf{HSet} \\ E_2 : \Pi abcd. E_1(a,b) \times E_1(c,d) \times E_1(a,c) \times E_1(b,d) \to \mathbf{HSet} \\ \dots \end{array} \qquad \text{(relevant relations)} $$

Equations specifying $v$-sets in indexed form were given, and the well-foundedness of the construction was by induction on a large structure involving equational reasoning. The current work presents a refined construction which expresses the computational essence of the construction.

## 2 High-level description of iterated parametricity in indexed form

We recall from the previous work how to formally define a type characterising the sequences $E_0, E_1, \dots$. The type theory we consider is with $\Sigma$ and $\Pi$ types, Martin-Löf identity type $=$, universes $U_m$, a unit type, natural numbers, a definitionally proof-irrelevant inequality on natural numbers, streams, and function extensionality. The non-dependent variants of $\Pi$ and $\Sigma$ are written $\to$ and $\times$ respectively. If $e$ is a proof of $x = y$ and $p$ a proof, we write $\overrightarrow{e}p$ for substituting $x$ with $y$ in the statement proved by $p$. The canonical inhabitant of unit is written $\star$, and the subuniverse of types $T: U_m$ satisfying $UIP: \Pi xy: T. \Pi pq: x = y.p = q$ is written $\mathbf{HSet}_m$. The definitional proof-irrelevance of inequality is a priori not essential, and could be replaced with propositional proof-irrelevance up to a few extra transports. Our use of function extensionality comes from representing $n$-tuples as functions, and could be avoided by representing $n$-tuples as lists.

Let us sketch how to define iterated parametricity in indexed form for arity $v$. The dependency of $E_{n+1}$ into all $E_p$ for $p \le n$ makes the family $E$ a very dependent function [11]. The standard way to express it is as a stream whose $(n+1)$-th element $E_{n+1}$ is dependent on the bundle of all previous elements of the stream. We write $v\mathbf{Set}_m^{\le n}$ for the bundle of all $E_0, \dots, E_{n-1}$, and we write $v\mathbf{Set}_m^{\ge n}(D)$ for the residual stream $E_n, E_{n+1}, \dots$, which is dependent on the bundle $E: v\mathbf{Set}_m^{\le n}$ of previous $E_0, \dots, E_{n-1}$. The type of $E_n$, also dependent on a bundle $D: v\mathbf{Set}_m^{\le n}$, is denoted $v\mathbf{Set}_m^{\ge n}(D)$, as shown on tables 1 and 2. When $n = 0$, $v\mathbf{Set}_m^{\le 0}$ is degenerated, and reduced to unit. Then, $v\mathbf{Set}_m^{\ge 0}(\star)$ represents the type of the full stream.

The type $v\mathbf{Set}_m^{\le n}(E_0, \dots, E_{n-1})$ of $E_n$ represents a family. It can be canonically presented into a form fullframe $(E_0, \dots, E_{n-1}) \to \mathbf{HSet}$ where fullframe collects all the dependencies of $E_n$. It is recursively defined in table 3, using frame, layer and painting. A fullframe describes a boundary of a standard form (simplex, cube), which we decompose into $n$ layer, one per dimension, each of them made of $v$ painting, where a painting corresponds to a filled frame. Notice that the type layer relies on an operator of frame restriction $restr_{frame}$ which is defined in table 4 for any $\epsilon$ ranging between 1 and $v$, and this restriction operator is in turn defined using $restr_{layer}$ and $restr_{painting}$.
XX:4 The very dependent recursive structure of iterated parametricity in indexed form

<table><caption>Table 1 Main definition</caption><tr><td>vSet<sub>m</sub></td><td>:</td><td>HSet<sub>m+1</sub></td></tr><tr><td>vSet<sub>m</sub></td><td>△</td><td>vSet<sup>≥0</sup><sub>m</sub>(*)</td></tr><tr><td>vSet<sup>≥n</sup><sub>m</sub> (D : vSet<sup>≤n</sup><sub>m</sub>)</td><td>:</td><td>HSet<sub>m+1</sub></td></tr><tr><td>vSet<sup>≥n</sup><sub>m</sub> D</td><td>△</td><td>ΣE : vSet<sup>=n</sup><sub>m</sub>(D).vSet<sup>≥n+1</sup><sub>m</sub>(D, E)</td></tr></table>

<table><caption>Table 2 Truncated v-sets, the core</caption><tr><td>vSet<sup>≤n</sup><sub>m</sub></td><td>:</td><td>HSet<sub>m+1</sub></td></tr><tr><td>vSet<sup>≤0</sup><sub>m</sub></td><td>△</td><td>unit</td></tr><tr><td>vSet<sup>≤n'</sup><sub>m</sub> +1</td><td>△</td><td>ΣD : vSet<sup>≤n'</sup><sub>m</sub>.vSet<sup>=n'</sup><sub>m</sub>(D)</td></tr><tr><td>vSet<sup>=n</sup><sub>m</sub> (D : vSet<sup>≤n</sup><sub>m</sub>)</td><td>:</td><td>HSet<sub>m+1</sub></td></tr><tr><td>vSet<sup>=n</sup><sub>m</sub> D</td><td>△</td><td>fullframe<sup>n</sup><sub>m</sub>(D) → HSet<sub>m</sub></td></tr></table>

<table><caption>Table 3 frame, layer, and painting</caption><tr><td>fullframe<sup>n</sup><sub>m</sub></td><td>(D : vSet<sup>≤n</sup><sub>m</sub>)</td><td>:</td><td>HSet<sub>m</sub></td></tr><tr><td>fullframe<sup>n</sup><sub>m</sub></td><td>D</td><td>△</td><td>frame<sup>n,n</sup>(D)</td></tr><tr><td>frame<sup>n,p</sup>,<sup>p</sup> ≤<sup>n</sup></td><td>(D : vSet<sup>≤n</sup><sub>m</sub>)</td><td>:</td><td>HSet<sub>m</sub></td></tr><tr><td>frame<sup>n,0</sup></td><td>D</td><td>△</td><td>unit</td></tr><tr><td>frame<sup>n,p+1</sup></td><td>D</td><td>△</td><td>Σd : frame<sup>n,p</sup>(D). layer<sup>n-1,p</sup>(d)</td></tr><tr><td>layer<sup>n,p</sup>,<sup>p</sup> ≤<sup>n</sup></td><td>{D : vSet<sup>≤n+1</sup><sub>m</sub>}<br>(d : frame<sup>n+1,p</sup>(D))</td><td>:</td><td>HSet<sub>m</sub></td></tr><tr><td>layer<sup>n,p</sup></td><td>D d</td><td>△</td><td>Πε. painting<sup>n,p</sup>(D.2)(restr<sup>n,p</sup><sub>frame,q,ε</sub>(d))</td></tr><tr><td>painting<sup>n,p</sup>,<sup>p</sup> ≤<sup>n</sup></td><td>(D : vSet<sup>≤n</sup><sub>m</sub>)<br>(E : vSet<sup>=n</sup><sub>m</sub>(D))<br>(d : frame<sup>n,p</sup>(D))</td><td>:</td><td>HSet<sub>m</sub></td></tr><tr><td>painting<sup>n,p</sup>,<sup>p</sup> =<sup>n</sup></td><td>D E d</td><td>△</td><td>E(d)</td></tr><tr><td>painting<sup>n,p</sup>,<sup>p</sup> <sup>n</sup></td><td>D E d</td><td>△</td><td>Σl : layer<sup>n-1,p</sup>(d). painting<sup>n,p+1</sup>(E)(d,l)</td></tr></table>

<table><caption>Table 4 q-th projection of restr, or faces</caption><tr><td>restr<sup>n,p,q</sup>,<sup>p</sup> ≤<sup>n-p</sup><sub>frame,q,ε</sub></td><td>{D : vSet<sup>≤n+1</sup><sub>m</sub>}<br>(d : frame<sup>n+1,p</sup>(D))</td><td>:</td><td>frame<sup>n,p</sup>(D.1)</td></tr><tr><td>restr<sup>n,0</sup><sub>frame,q,ε</sub></td><td>D *</td><td>△</td><td>*</td></tr><tr><td>restr<sup>n,p+1</sup><sub>frame,q,ε</sub></td><td>D (d, l)</td><td>△</td><td>(restr<sup>n,p</sup><sub>frame,q+1,ε</sub>(d), restr<sup>n-1,p</sup><sub>layer,q,ε</sub>(l))</td></tr><tr><td>restr<sup>n,p</sup><sub>layer,q,ε</sub></td><td>{D : vSet<sup>≤n+2</sup><sub>m</sub>}<br>{d : frame<sup>n+2,p</sup>(D)}<br>(l : layer<sup>n+1,p</sup>(d))</td><td>:</td><td>layer<sup>n,p</sup>(restr<sup>n+1,p</sup><sub>frame,q+1,ε</sub>(d))</td></tr><tr><td>restr<sup>n,p</sup><sub>layer,q,ε</sub></td><td>D d l</td><td>△</td><td>λω.(restr<sup>n,p</sup><sub>painting,q,ε</sub>(D.2)(l<sub>ω</sub>))</td></tr><tr><td>restr<sup>n,p,q</sup>,<sup>p</sup> ≤<sup>n-p</sup><sub>painting,q,ε</sub></td><td>{D : vSet<sup>≤n+1</sup><sub>m</sub>}<br>(E : vSet<sup>=n+1</sup><sub>m</sub>(D))<br>{d : frame<sup>n+1,p</sup>(D)}<br>(c : painting<sup>n+1,p</sup>(E)(d))</td><td>:</td><td>painting<sup>n,p</sup>(D.2)(restr<sup>n,p</sup><sub>frame,q,ε</sub>(d))</td></tr><tr><td>restr<sup>n,p</sup><sub>painting,0,ε</sub></td><td>D E d (l, -)</td><td>△</td><td>l<sub>ε</sub></td></tr><tr><td>restr<sup>n,p,q</sup>,<sup>p</sup> <sup>n</sup></td><td>D E d (l, c)</td><td>△</td><td>(restr<sup>n-1,p</sup><sub>layer,q,ε</sub>(l), restr<sup>n,p+1</sup><sub>painting,q,ε</sub>(E)(c))</td></tr></table>
<table><caption>Table 5 Commutation of q-th projection and r-th projection, or coherence conditions</caption><tr><td>coh<sup>n,p</sup><sub>frame,q,r,ε,ω</sub></td><td>{D : vSet<sup>n+2</sup><sub>m</sub><br/>(d : frame<sup>n+2,p</sup>(D))}</td><td>:</td><td>restr<sup>n,p</sup><sub>frame,q,ε</sub>(restr<sup>n+1,p</sup><sub>frame,r,ω</sub>(d))<br/>= restr<sup>n,p</sup><sub>frame,r,ω</sub>(restr<sup>n+1,p</sup><sub>frame,q+1,ε</sub>(d))</td></tr><tr><td>coh<sup>n,0</sup><sub>frame,q,r,ε,ω</sub></td><td>D *</td><td>Δ</td><td>refl(*)</td></tr><tr><td>coh<sup>n,p+1</sup><sub>frame,q,r,ε,ω</sub></td><td>D (d, l)</td><td>Δ</td><td>(coh<sup>n,p</sup><sub>frame,q+1,r+1,ε,ω</sub>(d), coh<sup>n-1,p</sup><sub>layer,q,r,ε,ω</sub>(l))</td></tr><tr><td>coh<sup>n,p</sup><sub>layer,ε,ω,q,r</sub></td><td>{D : vSet<sup>n+3</sup><sub>m</sub><br/>{d : frame<sup>n+3,p</sup>(D)}<br/>(l : layer<sup>n+2,p</sup>(d))}</td><td>:</td><td>restr<sup>n,p</sup><sub>layer,q,ε</sub>(restr<sup>n+1,p</sup><sub>layer,r,ω</sub>(l))<br/>= restr<sup>n,p</sup><sub>layer,r,ω</sub>(restr<sup>n+1,p</sup><sub>layer,q+1,ε</sub>(l))</td></tr><tr><td>coh<sup>n,p</sup><sub>layer,ε,ω,q,r</sub></td><td>D dl</td><td>Δ</td><td>λθ. coh<sup>n,p</sup><sub>painting,ε,ω,q,r</sub>(D.2)(l<sub>θ</sub>)</td></tr><tr><td>coh<sup>n,p</sup><sub>painting,q,r,ε,ω</sub></td><td>{D : vSet<sup>n+2</sup><sub>m</sub><br/>(E : vSet<sup>n+2</sup><sub>m</sub><br/>{d : frame<sup>n+2,p</sup>(D)}<br/>(c : painting<sup>n+2,p</sup>(E)(d))}</td><td>:</td><td>restr<sup>n,p</sup><sub>painting,q,ε</sub>(D.2)(restr<sup>n+1,p</sup><sub>painting,r,ω</sub>(E)(c))<br/>= restr<sup>n,p</sup><sub>painting,r,ω</sub>(D.2)(restr<sup>n+1,p</sup><sub>painting,q+1,ε</sub>(E)(c))</td></tr><tr><td>coh<sup>n,p</sup><sub>painting,q,0,ε,ω</sub></td><td>D E d (l, -)</td><td>Δ</td><td>refl(restr<sup>n,p</sup><sub>painting,q,ε</sub>(D.2)(l<sub>ε</sub>))</td></tr><tr><td>coh<sup>n,p</sup><sub>painting,q+1,r+1,ε,ω</sub></td><td>D E d (l, c)</td><td>Δ</td><td>(coh<sup>n-1,p</sup><sub>layer,q,r,ε,ω</sub>(l), coh<sup>n,p+1</sup><sub>painting,q,r,ε,ω</sub>(E)(c))</td></tr></table>

The definition of restr<sub>layer</sub> relies on an equality expressing the commutation of the composition of two restr<sub>frame</sub>. The proof of this commutation is made explicit<fnref n="3" /> in table 5. It is by recursion on the structure of frame, layer, and painting. This is what coh<sub>frame</sub> does using the proofs coh<sub>layer</sub> and coh<sub>painting</sub>. Note that for a fixed n, the coherence conditions evaluate to a reflexivity proof, so that the construction builds an effective sequence of types not mentioning coherences anymore.

### 3 Analysis of the recursive structure of iterated parametricity in indexed form

The well-foundedness of the construction of tables 1 to 5, was justified in the previous work by induction on a large structure involving equational reasoning. We show instead in this paper that equational reasoning can be avoided, and that it is enough to build by induction on n the following structure:

<table><tr><td>frame<sup>n,p</sup></td><td>:</td><td>HSet</td></tr><tr><td>painting<sup>n,p</sup></td><td>:</td><td>frame<sup>n,p</sup> → HSet</td></tr><tr><td>restr<sup>n,p</sup><sub>frame</sub></td><td>:</td><td>Πq ≤ n − p. Πε. frame<sup>n+1,p</sup> → frame<sup>n,p</sup></td></tr><tr><td>restr<sup>n,p</sup><sub>painting</sub></td><td>:</td><td>Πq ≤ n − p. Πε. Πd : frame<sup>n+1,p</sup>,<br/>painting<sup>n+1,p</sup>(d) → painting<sup>n,p</sup>(restr<sup>n,p</sup><sub>frame</sub>(d))</td></tr><tr><td>coh<sup>n,p</sup><sub>frame</sub></td><td>:</td><td>Πqreω. restr<sup>n,p</sup><sub>frame,q,ε</sub> ◦ restr<sup>n+1,p</sup><sub>frame,ω,r</sub> =<br/>restr<sup>n,p</sup><sub>frame,ω,r</sub> ◦ restr<sup>n+1,p</sup><sub>frame,q+1,ε</sub></td></tr><tr><td>coh<sup>n,p</sup><sub>painting</sub></td><td>:</td><td>Πqreω. Πd : frame<sup>n+2,p</sup>,<br/>restr<sup>n,p</sup><sub>painting,q,ε</sub>(restr<sup>n+1,p</sup><sub>frame,r,ω</sub>(d)) ◦ restr<sup>n+1,p</sup><sub>painting,r,ω</sub>(d) =<br/>restr<sup>n,p</sup><sub>painting,r,ω</sub>(restr<sup>n+1,p</sup><sub>frame,q+1,ε</sub>(d)) ◦ restr<sup>n+1,p</sup><sub>painting,q+1,ε</sub>(d)</td></tr></table>

The price to pay for this conciseness is to mix the specification of the induction hypothesis with the construction of the induction step. On the outset, restr<sup>n,p</sup><sub>frame</sub> depends on frame<sup>n+1,p</sup>:

<footnote n="3">³ We however omit type conversions in the tables, as if working in extensional type theory. For instance, coh<sub>frame</sub> is implicitly used in the definition of restr<sub>layer</sub>. For details on where coherence proofs are used, see [10].</footnote>
XX:6 The very dependent recursive structure of iterated parametricity in indexed form

it already depends on the ability of building the frame component of the structure at level $n+1$. There is thus an interdependency between specifying the structure assumed at level $n$ and defining from it the structure at level $n+1$. We have to proceed in a specific order: specifying frame$^n$, from which painting$^n$ can be specified, from which frame$^{n+1}$ can be built, from which restr$^{n+1}_{frame}$ can be specified. Now, the definition of frame$^{n+1,p}$, which proceeds by induction on $p$, itself depends on restr$^{n,p-1}_{frame}$ whose type depends in turn on frame$^{n+1,p-1}$. Hence, frame$^{n+1,p}$ and the type of restr$^{n,p}_{frame}$ have to be mutually defined.

The definition of frame$^{n+1,p}$ also depends, via layer$^{n,p-1}$, on painting$^{n,p-1}$. Via painting$^{n,p-1}$ and restr$^{n,p-1}_{frame}$, it depends also on frame$^{n,p-1}$ by typing dependency. This requires us to assume frame$^{n,p-1}$ and painting$^{n,p-1}$. Moreover, the definition of frame$^{n+1,p}$ depends on frame$^{n+1,p-1}$, so frame$^{n,k}$, painting$^{n,k}$, and restr$^{n,k}_{frame}$, for $k < p$, need to be known.

We abbreviate the collection of all frame$^n$ for $k < p$ as frame$^{n,[0,p-1]}$ and similarly for painting$^n$, $frame^{n,[0,p-1]}$ and restr$^{n,[0,p-1]}_{frame}$. Conversely, if frame$^{n,[0,p]}$ is a non-empty sequence, we will write frame$^{n,[0,p-1]}$ for the immediate subsequence of length $p$ and frame$^{n,p}$ for the last component of the sequence. We write frame$^n$ for frame$^{n,[0,-1]}$.

Schematically, using dotted arrows for dependencies in the type and plain arrows for dependencies in the definition, this gives the following graph of dependencies for $p \le n+1$.

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

In particular, the dependency of frame$^{n+1,[0,p-1]}$ within the type of restr$^{n,[0,p-1]}_{frame}$ combined with the dependency of restr$^{n,[0,p-1]}_{frame}$ within the definition of frame$^{n+1,[0,p]}$ requires a mutual definition of the type of restr$^{n,[0,p-1]}_{frame}$ and of frame$^{n+1,p}$ as a function from restr$^{n,[0,p-1]}_{frame}$.

Using this recursive definition of frame$^{n+1,[0,p]}$ and restr$^{n,[0,p-1]}_{frame}$, we are thus able to extend the specification of the structure with its third component, for all $p \le n$.

$$
\begin{array}{lcl}
frame^{n,p} & : & HSet \\
painting^{n,p} & : & frame^{n,p} \rightarrow HSet \\
restr^{n,p}_{frame} & : & \Pi q \le n - p. \Pi c. \quad \left( \begin{array}{l} frame^{n,[0,p-1]} \\ painting^{n,[0,p-1]} \\ restr^{n,[0,p-1]}_{frame} \end{array} \right) \rightarrow frame^{n,p}
\end{array}
$$

This can be reformulated using sequences for appropriate definitions of FRAME$^{n,[0,p]}$, PAINTING$^{n,[0,p]}$, and restr$^{n,[0,p]}_{FRAME}$:

$$
\begin{array}{lcl}
frame^{n,[0,p]} & : & FRAME^{n,[0,p]} \\
painting^{n,[0,p]} & : & PAINTING^{n,[0,p]}(frame^{n,[0,p]}) \\
restr^{n,[0,p]}_{frame} & : & restr^{n,[0,p]}_{FRAME} \left( \begin{array}{l} frame^{n,[0,p-1]} \\ painting^{n,[0,p-1]} \\ restr^{n,[0,p-1]}_{frame} \end{array} \right)
\end{array}
$$
Types such as $\mathrm{restr}_{\mathrm{FRAME}}^{n,[0,p]}$ will be represented by iterated $\Sigma$-types since each $\mathrm{restr}_{\mathrm{frame}}^{n,p}$ may depend on the previous components of the sequence. In the case of frame and painting, there is no dependency, so an ordinary product can be used to represent $\mathrm{FRAME}^{n,[0,p]}$ and $\mathrm{PAINTING}^{n,[0,p]}$.

Let us turn now to the specification of $\mathrm{restr}_{\mathrm{painting}}^{n,p}$. Since it depends on $\mathrm{painting}^{n+1,p}$, we need first to define $\mathrm{painting}^{n+1,p}$ but in addition to the type dependency in $\mathrm{frame}^{n+1,p}$, this requires the definition of $\mathrm{painting}^{n,p-1}$, $\mathrm{frame}^{n,p-1}$ by typing dependency, and $\mathrm{restr}_{\mathrm{frame}}^{n,p-1}$. Since $\mathrm{painting}^{n+1,p}$ also depends on $\mathrm{painting}^{n+1,p+1}$ when $p < n + 1$, these dependencies are actually between $\mathrm{painting}^{n+1,[p,n+1]}$, $\mathrm{painting}^{n,[p,n]}$, $\mathrm{frame}^{n+1,[p,n+1]}$, $\mathrm{frame}^{n,[p,n]}$, and $\mathrm{restr}_{\mathrm{frame}}^{n,[p,n]}$. For $p = n$, this requires the assumption of an inhabitant $E_{n+1}$ of $\mathcal{V}\mathrm{Set}_m^{=n+1}$. Finally, $\mathrm{frame}^{n+1,[p,n+1]}$ depends on $\mathrm{frame}^{n+1,[0,p-1]}$, $\mathrm{frame}^{n+1,[p,n]}$ on $\mathrm{frame}^{n,[0,p-1]}$, and $\mathrm{restr}_{\mathrm{frame}}^{n,[p,n]}$ on $\mathrm{restr}_{\mathrm{frame}}^{n,[0,p-1]}$, leading to the following graph of dependencies where indirect dependencies in definitions are now dashed lines.

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

This is eventually enough to specify the type $\mathrm{restr}_{\mathrm{PAINTING}}^{n,[0,p]}$ of $\mathrm{restr}_{\mathrm{painting}}^{n,[0,p]}$ so that we can focus on the specification of $\mathrm{coh}_{\mathrm{frame}}^{n,p}$. An analysis similar to the one done for $\mathrm{restr}_{\mathrm{frame}}^{n,p}$ leads to conclude that the specification of $\mathrm{coh}_{\mathrm{frame}}^{n,[0,p]}$ should be done mutually with the definition of $\mathrm{restr}_{\mathrm{frame}}^{n+1,[0,p+1]}$.

Then, $\mathrm{coh}_{\mathrm{painting}}^{n,p}$ has to be specified, for which the same analysis done for specifying $\mathrm{restr}_{\mathrm{painting}}^{n,p}$ applies. In particular, it requires first to define $\mathrm{restr}_{\mathrm{painting}}^{n+1,[0,p]}$.

The specification of the six fields being complete, the induction step can be built. All of $\mathrm{frame}^{n+1,[0,p]}$, $\mathrm{painting}^{n+1,[0,p]}$, $\mathrm{restr}_{\mathrm{frame}}^{n+1,[0,p]}$ and $\mathrm{restr}_{\mathrm{painting}}^{n+1,[0,p]}$ have already been built, so only the construction of $\mathrm{coh}_{\mathrm{frame}}^{n+1,[0,p]}$ and $\mathrm{coh}_{\mathrm{painting}}^{n+1,[0,p]}$ remain. Details follow.

## 3.1 Specifying frames ⚙

Assuming $\mathrm{frame}^{n,[0,p-1]}$ for $p \le n + 1$ only requires defining the type $\mathrm{FRAME}^{n,[0,p-1]}$ of frames, which is just a $p$-ary product of $\mathcal{H}\mathrm{Set}$.

$\mathrm{FRAME}^{n,[0,p-1]}$ : $\mathcal{H}\mathrm{Set}$
$\mathrm{FRAME}^n$ : $\mathrm{unit}$
$\mathrm{FRAME}^{n,[0,p]}$ : $\mathrm{FRAME}^{n,[0,p-1]} \times \mathcal{H}\mathrm{Set}$
## 3.2 Specifying paintings 🎨

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

The type `PAINTING<sup>n</sup><sub>n,[0,p-1]</sub>` of `painting<sup>n</sup><sub>n,[0,p-1]</sub>` for $p \le n + 1$ is a product of type families over frames, so `frame<sup>n</sup><sub>n,[0,p-1]</sub>` needs to be assumed.

$$ 
\begin{align*}
\text{PAINTING}^{n,[0,p-1]} & \quad \text{frame}^{n,[0,p-1]} & \quad : & \text{HSet} \\
\text{PAINTING}^n & \quad * & \quad \trianglelefteq & \text{unit} \\
\text{PAINTING}^{n,[0,p]} & \quad \text{frame}^{n,[0,p]} & \quad \trianglelefteq & \text{PAINTING}^{n,[0,p-1]}(\text{frame}^{n,[0,p-1]}) \times (\text{frame}^{n,p} \to \text{HSet})
\end{align*}
$$

## 3.3 Defining frames and specifying frame restrictions 🎨

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

Assuming `frame<sup>n</sup><sub>n,[0,p-1]</sub>` and `painting<sup>n</sup><sub>n,[0,p-1]</sub>` for $p \le n + 1$, we can mutually define the types `restr<sup>n</sup><sub>FRAME</sub>` together with `frame<sup>n+1</sup><sub>n,[0,p]</sub>`, as a function from `restr<sup>n</sup><sub>frame</sub>`. We introduce the abbreviation `DEPS<sup>n</sup><sub>restr</sub>` for the combination of sequences of `frame<sup>n</sup><sub>n,[0,p-1]</sub>`, `painting<sup>n</sup><sub>n,[0,p-1]</sub>` and `restr<sup>n</sup><sub>frame</sub>`.

Once a `deps<sub>restr</sub>` : `DEPS<sub>restr</sub>` is assumed, we freely refer to `frame`, `painting`, `restr<sub>frame</sub>`.

$$ 
\begin{align*}
\text{DEPS}_{\text{restr}}^{n,[0,p-1]} & \quad \triangleq & \quad \left( \begin{array}{ll} \text{frame}^{n,[0,p-1]} & : \text{FRAME}^{n,[0,p-1]} \\ \text{painting}^{n,[0,p-1]} & : \text{PAINTING}^{n,[0,p-1]}(\text{frame}^{n,[0,p-1]}) \\ \text{restr}_{\text{frame}}^{n,[0,p-1]} & : \text{restr}_{\text{FRAME}}^{n,[0,p-1]} \begin{pmatrix} \text{frame}^{n,[0,p-1]} \\ \text{painting}^{n,[0,p-1]} \end{pmatrix} \end{array} \right) \\
\text{frame}^{n+1,[0,p]} & \quad \text{deps}_{\text{restr}}^{n,[0,p-1]} & \quad : & \text{FRAME}^{n+1,[0,p]} \\
\text{frame}^{n+1,[0,0]} & \quad \text{deps}_{\text{restr}}^{n} & \quad \trianglelefteq & (*, \text{unit}) \\
\text{frame}^{n+1,[0,p+1]} & \quad \text{deps}_{\text{restr}}^{n,[0,p]} & \quad \trianglelefteq & \left( \begin{array}{l} \text{frame}^{n+1,[0,p]}(\text{deps}_{\text{restr}}^{n,[0,p-1]}), \\ \Sigma d : \text{frame}^{n+1,p}(\text{deps}_{\text{restr}}^{n,[0,p-1]}), \text{layer}^{n,p}(\text{deps}_{\text{restr}}^{n,[0,p]})(d) \end{array} \right) \\
\text{restr}_{\text{FRAME}}^{n,[0,p-1]} & \quad \text{frame}^{n,[0,p-1]} \quad : & \quad \text{HSet} \\
\text{restr}_{\text{FRAME}}^{n} & \quad * \quad : & \quad \text{unit} \\
\text{restr}_{\text{FRAME}}^{n,[0,p]} & \quad \begin{pmatrix} \text{frame}^{n,[0,p]} \\ \text{painting}^{n,[0,p]} \end{pmatrix} & \quad \triangleq & \left\{ \begin{array}{@{}l@{}} \Sigma \text{restr}_{\text{frame}}^{n,[0,p-1]} : \text{restr}_{\text{FRAME}}^{n,[0,p-1]} \begin{pmatrix} \text{frame}^{n,[0,p-1]} \\ \text{painting}^{n,[0,p-1]} \end{pmatrix} \\ \Pi q \le n-p. \Pi \epsilon. \\ \text{frame}^{n+1,p} \begin{pmatrix} \text{frame}^{n,[0,p-1]} \\ \text{painting}^{n,[0,p-1]} \\ \text{restr}_{\text{frame}}^{n+1,[0,p-1]} \end{pmatrix} \to \text{frame}^{n,p} \end{array} \right. \\
\text{LAYER}^{n,p} & \quad \text{deps}_{\text{restr}}^{n,[0,p]} & \quad : & \text{HSet} \\
\text{LAYER}^{n,p} & \quad \text{deps}_{\text{restr}}^{n,[0,p]} & \quad \trianglelefteq & \text{frame}^{n+1,p}(\text{deps}_{\text{restr}}^{n,[0,p-1]}) \to \text{HSet} \\
\text{layer}^{n,p} & \quad \text{deps}_{\text{restr}}^{n,[0,p]} & \quad : & \text{LAYER}^{n,p}(\text{deps}_{\text{restr}}^{n,[0,p]}) \\
\text{layer}^{n,p} & \quad \text{deps}_{\text{restr}}^{n,[0,p]} & \quad \trianglelefteq & \lambda d. \Pi \epsilon. \text{painting}^{n,p}(\text{restr}_{\text{frame},0,\epsilon}^{n,p}(d))
\end{align*}
$$

## 3.4 Defining paintings 🎨

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

To define `painting<sup>n+1,p</sup>`, let us introduce another abbreviation that combines a full `deps<sub>restr</sub><sup>n,[0,n]</sup>`: `DEPS<sup>n</sup><sub>restr</sub>` with a family `E`: `frame<sup>n+1,n+1</sup>(deps<sub>restr</sub><sup>n,[0,n]</sup>)` $\to$ `HSet`.

$$ 
\text{DEPS}_{\text{fullrestr}}^{n} \triangleq \left( \begin{array}{ll} \text{deps}_{\text{restr}}^{n,[0,n]} & : & \text{DEPS}_{\text{restr}}^{n,[0,n]} \\ E & : & \text{frame}^{n+1,n+1}(\text{deps}_{\text{restr}}^{n,[0,n]}) \to \text{HSet} \end{array} \right)
$$

Then, `painting<sup>n+1,p</sup>` is defined for $p \le n + 1$ by recursion from the base case $n + 1$, and down to $p$.
$$ \text{painting}^{n+1,p} \qquad \text{deps}_{\text{fullrestr}}^n \qquad : \qquad \text{PAINTING}^{n+1,p} $$

$$ \text{painting}^{n+1,n+1} \qquad \text{deps}_{\text{fullrestr}}^n \qquad \triangleq \qquad E $$

$$ \text{painting}^{n+1,p \le n} \qquad \text{deps}_{\text{fullrestr}}^n \qquad \triangleq \qquad \lambda d. \Sigma l : \text{layer}^{n,p}(\text{deps}_{\text{restr}}^{n,[0,p]}) \cdot \text{painting}^{n+1,p+1}(\text{deps}_{\text{fullrestr}}^n)(d,l) $$

From this, we can deduce `painting^{n+1,[0,p-1]}` for $p \le n + 2$ by a second recursion, this time on $p$.

$$ \text{painting}^{n+1,[0,p-1]} \qquad \text{deps}_{\text{fullrestr}}^n \qquad : \qquad \text{PAINTING}^{n+1,[0,p-1]}(\text{frame}^{n+1,[0,p-1]}(\text{deps}_{\text{restr}}^{n,[0,p-1]})) $$

$$ \text{painting}^{n+1} \qquad \text{deps}_{\text{fullrestr}}^n \qquad \triangleq \qquad \text{unit} $$

$$ \text{painting}^{n+1,[0,p]} \qquad \text{deps}_{\text{fullrestr}}^n \qquad \triangleq \qquad (\text{painting}^{n+1,[0,p-1]}(\text{deps}_{\text{fullrestr}}^n), \text{painting}^{n+1,p}(\text{deps}_{\text{fullrestr}}^n)) $$

## 3.5 Specifying painting restrictions 🎨

To go further, we need to specify the type of sequences of painting restrictions, for $p \le n + 1$.

$$ \text{restr}_{\text{PAINTING}}^{n,[0,p-1]} \qquad \text{deps}_{\text{fullrestr}}^n \qquad : \qquad \text{HSet} $$

$$ \text{restr}_{\text{PAINTING}}^n \qquad \text{deps}_{\text{fullrestr}}^n \qquad \triangleq \qquad \text{unit} $$

$$ \text{restr}_{\text{PAINTING}}^{n,[0,p]} \qquad \text{deps}_{\text{fullrestr}}^n \qquad \triangleq \qquad \text{restr}_{\text{PAINTING}}^{n,[0,p-1]} \times \left( \begin{array}{l} \Pi q \le n - p. \Pi \epsilon. \Pi d : \text{frame}^{n+1,p}(\text{deps}_{\text{restr}}^{n,[0,p-1]}). \\ \text{painting}^{n+1,p}(\text{deps}_{\text{fullrestr}}^n)(d) \rightarrow \\ \text{painting}^{n,p}(\text{restr}_{\text{frame},q,\epsilon}^{n,p}(d)) \end{array} \right) $$

## 3.6 Defining frame restrictions and specifying frame coherence laws 🎨

We can now mutually define `restr_{frame}^{n+1,[0,p]}` and specify `coh_{frame}^{n,[0,p-1]}` from `frame^{n,[0,n]}`, `painting^{n,[0,n]}`, `restr_{frame}^{n,[0,n]}`, `restr_{painting}^{n,[0,p-1]}` and some $E : \text{frame}^{n+1,n+1}(\text{deps}_{\text{restr}}^{n,[0,n]}) \rightarrow \text{HSet}$, abbreviating these dependencies and the dependency in `coh_{frame}^{n,[0,p-1]}` as `DEPS_{coh}^{n,[0,p-1]}`, and using abbreviations in passing for `restr_{layer}^{n,p}` and `restr_{LAYER}^{n,p}`. It is convenient to build `deps_{restr}^{n+1,[0,p]}` from `deps_{coh}^{n,[0,p-1]}`, so that we can now build `frame^{n+2,p}` one step further.
$$
\begin{align*}
\text{DEPS}_{\text{coh}}^{n,[0,p-1]} &\triangleq \left( \begin{array}{l} \text{deps}_{\text{fullrestr}}^n : \text{DEPS}_{\text{coh}}^n \\ \text{restr}_{\text{frame}}^{n,[0,p-1]} : \text{restr}_{\text{frame}}^{n,[0,p-1]}(\text{deps}_{\text{coh}}^n) \\ \text{coh}_{\text{frame}}^{n,[0,p-1]} : \text{coh}_{\text{frame}}^{n,[0,p-1]}(\text{deps}_{\text{coh}}^n) \end{array} \right) \\
\text{deps}_{\text{restr}} &\triangleq \text{DEPS}_{\text{restr}}^{n+1,[0,p]} \\
\text{deps}_{\text{coh}} &\triangleq \left( \begin{array}{l} \text{frame}^{n+1,[0,p]}(\text{deps}_{\text{coh}}^n) \\ \text{painting}^{n+1,[0,p]}(\text{deps}_{\text{fullrestr}}^n) \\ \text{restr}_{\text{frame}}^{n+1,[0,p]}(\text{deps}_{\text{coh}}^n) \end{array} \right) \\
\text{restr}_{\text{frame}}^{n+1,[0,p]} &\triangleq \text{restr}_{\text{frame}}^{n+1,[0,p]}(\text{frame}^{n+1,[0,p]}(\text{deps}_{\text{restr}}^n) \\
\text{restr}_{\text{frame}}^{n+1,[0,0]} &\triangleq (\lambda q.\lambda \epsilon.\lambda \dots) \\
\text{restr}_{\text{frame}}^{n+1,[0,p+1]} &\triangleq \left( \begin{array}{l} (\text{restr}_{\text{frame},q,\epsilon}^{n+1,[0,p]}(\text{deps}_{\text{coh}}^n), \lambda q.\lambda \epsilon.\lambda(d,l)) \\ ((\text{restr}_{\text{frame},q,\epsilon}^{n+1,p}(\text{deps}_{\text{coh}}^n))(d), \text{restr}_{\text{layer},q,\epsilon}^{n,p}(\text{deps}_{\text{coh}}^n))(d)(l)) \end{array} \right) \\
\text{coh}_{\text{frame}}^{n,[0,p-1]} &\triangleq \text{HSet} \\
\text{coh}_{\text{frame}}^n &\triangleq \text{unit} \\
\text{coh}_{\text{frame}}^{n,[0,p]} &\triangleq \left( \begin{array}{l} \text{deps}_{\text{fullrestr}}^n \\ \text{restr}_{\text{frame}}^{n,[0,p]} \\ \text{deps}_{\text{fullrestr}}^n \ast \end{array} \right) \\
\text{restr}_{\text{layer}}^{n,p} &\triangleq \text{HSet} \\
\text{restr}_{\text{layer}}^{n,p} &\triangleq \left\{ \begin{array}{l} \text{layer}^{n+1,p}(\text{deps}_{\text{restr}}(\text{deps}_{\text{coh}}^{n,[0,p-2]}))(d) \rightarrow \\ \text{layer}^{n,p}(\text{deps}_{\text{restr}}(\text{deps}_{\text{coh}}^{n,[0,p]}))(\text{restr}_{\text{frame}}^{n,p}(\text{deps}_{\text{coh}}^{n,[0,p-1]}))(d) \end{array} \right. \\
\text{restr}_{\text{layer}}^{n,p} &\triangleq \text{restr}_{\text{layer}}^{n,p}(\text{deps}_{\text{coh}}^{n,[0,p]}) \\
\text{restr}_{\text{layer},q,\epsilon}^{n,p} &\triangleq \lambda d.\lambda l.\lambda \omega.\text{coh}_{\text{frame},q,0,\epsilon,\omega}^{n,p} \rightarrow \\
&\qquad \text{restr}_{\text{frame},q,\epsilon}^{n,p}(\text{restr}_{\text{frame},q,\epsilon}(\text{deps}_{\text{coh}}^{n,[0,p-1]}))(d)(l_{\omega})
\end{align*}
$$

## 3.7 Defining painting restrictions

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

Armed with $\text{restr}_{\text{frame}}^{n+1,[0,p]}$ and $\text{coh}_{\text{frame}}^{n,[0,p-1]}$, thus also with $\text{restr}_{\text{layer}}^{n,[0,p-1]}$, it is possible to define $\text{restr}_{\text{layer}}^{n+1,p}$. First, we define a notion of full dependencies at the level of coherence conditions, that combines a full $\text{deps}_{\text{coh}}^{n,[0,n]}$ with a set $E' : \text{frame}^{n+2,n+2}(\overline{\text{deps}_{\text{restr}}(\text{deps}_{\text{coh}}^{n,[0,n]})}) \rightarrow \text{HSet}$.

$$
\text{DEPS}_{\text{fullcoh}}^n \triangleq \left( \begin{array}{l} \text{deps}_{\text{coh}}^{n,[0,n]} : \text{DEPS}_{\text{coh}}^{n,[0,n]} \\ E' : \text{frame}^{n+2,n+2}(\overline{\text{deps}_{\text{restr}}(\text{deps}_{\text{coh}}^{n,[0,n]})}) \rightarrow \text{HSet} \end{array} \right)
$$

We can then extend $\overline{\text{deps}_{\text{restr}}}$ to build $\text{deps}_{\text{fullrestr}}$ from $\text{deps}_{\text{fullcoh}}$.
$$ \frac{\text{\textit{deps}}_{\text{fullrestr}}}{\text{\textit{deps}}_{\text{fullrestr}}} \text{\textit{deps}}_{\text{fullcoh}}^{n} : \text{\textit{DEPS}}_{\text{fullrestr}}^{n+1} \quad \text{\textit{\textit{deps}}}_{\text{restr}}(\text{\textit{deps}}_{\text{coh}}^{n,[0,n]}) \\ \text{\textit{\textit{deps}}}_{\text{fullrestr}} \text{\textit{deps}}_{\text{fullcoh}}^{n} \triangleq \left( \frac{\text{\textit{deps}}_{\text{restr}}}{E'} \right) $$

Then we can define $\text{restr}_{\text{painting}}^{n+1,p}$ for $p \le n+1$ by recursion on $n+1-p$.

$$ \text{restr}_{\text{painting},q,\epsilon}^{n+1,p} \text{\textit{deps}}_{\text{fullcoh}}^{n} : \left( \begin{array}{l} \Pi d : \text{frame}^{n+2,p}(\text{\textit{deps}}_{\text{restr}}(\text{\textit{deps}}_{\text{coh}}^{n,[0,p-2]})). \\ \text{painting}^{n+2,p}(\text{\textit{deps}}_{\text{fullrestr}}(\text{\textit{deps}}_{\text{fullcoh}}^{n})) (d) \to \\ \text{painting}^{n+1,p}(\text{\textit{deps}}_{\text{fullrestr}})(\text{\textit{restr}}_{\text{frame}}^{n+1,p}(\text{\textit{deps}}_{\text{coh}}^{n,[0,p-1]})(d)) \end{array} \right) \\ \text{restr}_{\text{painting},q,\epsilon}^{n+1,n+1} \text{\textit{deps}}_{\text{fullcoh}}^{n} \triangleq \lambda d.\lambda(l,c).l_{\epsilon} \\ \text{restr}_{\text{painting},q,\epsilon}^{n+1,p \le n} \text{\textit{deps}}_{\text{fullcoh}}^{n} \triangleq \lambda d.\lambda(l,c). \left( \begin{array}{l} \text{restr}_{\text{layer},q,\epsilon}^{n,p}(\text{\textit{deps}}_{\text{coh}}^{n,[0,p]})(d)(l), \\ \text{restr}_{\text{painting},q,\epsilon}^{n+1,p+1}(\text{\textit{deps}}_{\text{fullcoh}}^{n})(d,l)(c) \end{array} \right) $$

From this, we can deduce $\text{restr}_{\text{painting}}^{n+1,[0,p-1]}$ for $p \le n+2$ again by a second recursion, this time on $p$.

$$ \text{restr}_{\text{painting}}^{n+1,[0,p-1]} \text{\textit{deps}}_{\text{fullcoh}}^{n} : \text{restr}_{\text{PAINTING}}^{n+1,[0,p-1]}(\text{\textit{deps}}_{\text{fullrestr}}^{n}) \\ \text{restr}_{\text{painting}}^{n+1} \text{\textit{deps}}_{\text{fullcoh}}^{n} \triangleq \text{unit} \\ \text{restr}_{\text{painting}}^{n+1,[0,p]} \text{\textit{deps}}_{\text{fullcoh}}^{n} \triangleq (\text{restr}_{\text{painting}}^{n+1,[0,p-1]}(\text{\textit{deps}}_{\text{fullcoh}}^{n}), \text{restr}_{\text{painting}}^{n+1,p}(\text{\textit{deps}}_{\text{fullcoh}}^{n})) $$

## 3.8 Specifying painting coherence laws ⚙️

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

To go further, we need to specify the type $\text{coh}_{\text{PAINTING}}^{n,[0,p-1]}$ of painting coherence laws, for $p \le n+1$.

$$ \begin{array}{l} \text{coh}_{\text{PAINTING}}^{n,[0,p-1]} \text{\textit{deps}}_{\text{fullcoh}}^{n} : \text{HSet} \\ \text{coh}_{\text{PAINTING}}^{n} * \text{\textit{\textit{deps}}}_{\text{fullcoh}}^{n} \triangleq \text{unit} \\ \text{coh}_{\text{PAINTING}}^{n,[0,p]} \text{\textit{deps}}_{\text{fullcoh}}^{n} \triangleq \text{coh}_{\text{PAINTING}}^{n,[0,p-1]}(\text{\textit{deps}}_{\text{fullcoh}}^{n}) \times \\ \left\{ \begin{array}{l} \Pi q \le n - p. \Pi r \le q. \Pi \epsilon. \Pi \omega. \\ \Pi d : \text{frame}^{n+2,p}(\text{\textit{deps}}_{\text{restr}}(\text{\textit{deps}}_{\text{coh}}^{n,[0,p-2]})). \\ \Pi c : \text{painting}^{n+2,p}(\text{\textit{deps}}_{\text{fullrestr}}(\text{\textit{deps}}_{\text{fullcoh}}^{n})). \\ \text{restr}_{\text{painting},q,\epsilon}(\text{restr}_{\text{frame}}^{n+1,p}(\text{\textit{deps}}_{\text{coh}}^{n,[0,p-1]})(d))(\text{restr}_{\text{painting},r,\omega}(\text{\textit{deps}}_{\text{fullcoh}}^{n})(d)(c)) = \text{coh}_{\text{frame},q,r,\epsilon,\omega}^{n,p} \\ \text{restr}_{\text{painting},r,\omega}(\text{restr}_{\text{frame}}^{n+1,p}(\text{\textit{deps}}_{\text{coh}}^{n,[0,p-1]})(d))(\text{restr}_{\text{painting},q+1,\epsilon}(\text{\textit{deps}}_{\text{fullcoh}}^{n})(d)(c)) \end{array} \right. \end{array} $$

where we use the “equality over” notation $t =_e u$ to mean $\vec{e}(t) = u$ whenever $t$ is of some type $P(a)$, $u$ of type $P(b)$ and $e$ a proof of $a = b$.

## 3.9 Defining frame coherence laws and specifying frame 2-dimensional coherence laws ⚙️

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

With $\text{coh}_{\text{PAINTING}}^{n,[0,p-1]}$, we can mutually define $\text{coh}_{\text{frame}}^{n+1,[0,p]}$ and $\text{coh}_{\text{FRAME}}^{n,[0,p-1]}$ for $p \le n+1$ from $\text{deps}_{\text{fullcoh}}^{n}$. Due to reasoning in HSet, we do not need to have $\text{coh}_{\text{frame}}^{n+1,[0,p]}$ depending on a proof of $\text{coh}_{\text{FRAME}}^{n,[0,p-1]}$ as the latter can be proved by uniqueness of identity proofs. It is enough to consider $\text{coh}_{\text{FRAME}}^{n,p}$ instead of $\text{coh}_{\text{FRAME}}^{n,[0,p-1]}$.

It is also convenient to build $\text{deps}_{\text{coh}}^{n+1,[0,p]}$ from $\text{deps}_{\text{coh}2}^{n,[0,p-1]}$, so that we can now build $\text{frame}^{n+3,p}$. We implicitly use in $\text{coh}_{\text{frame}}^{n+1,[0,p]}$ that equalities in a $\Sigma$-type are equivalent to the $\Sigma$-type of the underlying equalities.
## 3.10 Defining painting coherence laws ⚙

It is convenient to introduce a notion of full dependencies at the level of the coherence conditions of dimension 2, that combines a full $\text{deps}_{\text{coh2}}^{n, [0,n]}$ with an extra $E''$ at level $n+3$.

$$ \text{DEPS}_{\text{fullcoh2}}^{n} \triangleq \left( \begin{array}{ll} \text{deps}_{\text{coh2}}^{n, [0,n]} & : \text{DEPS}_{\text{coh2}}^{n, [0,n]} \\ E'' & : \text{frame}^{n+3, n+3} \left( \overline{\text{deps}_{\text{restr}}(\text{deps}_{\text{coh}}(\text{deps}_{\text{coh2}}^{n, [0,n]}))} \right) \rightarrow \text{HSet} \end{array} \right) $$

We can then extend $\overline{\text{deps}}_{\text{coh}}$ to build $\text{deps}_{\text{fullcoh}}^{n+1}$ from $\text{deps}_{\text{fullcoh2}}^{n}$.

$$ \begin{array}{ll} \overline{\text{deps}}_{\text{fullcoh}} & \text{deps}_{\text{fullcoh2}}^{n} : \text{DEPS}_{\text{fullcoh}}^{n+1} \\ \overline{\text{deps}}_{\text{fullcoh}} & \text{deps}_{\text{fullcoh2}}^{n} \triangleq \left( \overline{\text{deps}}_{\text{coh}}(\text{deps}_{\text{coh2}}^{n, [0,n]}) \right) \end{array} $$

We are then ready to define the final component of the construction, namely $\text{coh}_{\text{painting}}^{n+1, p}$ for $p \le n+1$, by recursion on $n+1-p$.

$$ \begin{align*} \text{coh}^{n+1, p}_{\text{painting}} &\quad \text{deps}^{n}_{\text{fullcoh2}} : \quad \text{coh}^{n+1, p}_{\text{PAINTING}}(\overline{\text{deps}_{\text{fullcoh}}(\text{deps}^{n}_{\text{fullcoh2}})}) \\ \text{coh}^{n+1, n+1}_{\text{painting}, q, r, \epsilon, \omega} &\quad \text{deps}^{n}_{\text{fullcoh2}} \triangleq \lambda d.\lambda(l, c).I_{\epsilon} \\ \text{coh}^{n+1, p \le n}_{\text{painting}, q, r, \epsilon, \omega} &\quad \text{deps}^{n}_{\text{fullcoh2}} \triangleq \lambda d.\lambda(l, c). \left( \begin{array}{l} \text{coh}^{n, p}_{\text{layer}, q, r, \epsilon, \omega}(\overline{\text{deps}_{\text{coh2}}^{n, [0,p-1]}})(d)(l), \\ \text{coh}^{n+1, p+1}_{\text{painting}, q, r, \epsilon, \omega}(\overline{\text{deps}_{\text{fullcoh2}}^{n}})(d, l))(c) \end{array} \right) \end{align*} $$

From the latter, we can deduce $\text{coh}_{\text{painting}}^{n+1, [0, p-1]}$ for $p \le n+2$, by induction on $p$.

$$ \begin{align*} \text{coh}^{n+1, [0, p-1]}_{\text{painting}} &\quad \text{deps}^{n}_{\text{fullcoh2}} : \quad \text{coh}^{n+1, [0, p-1]}_{\text{PAINTING}}(\overline{\text{deps}^{n}_{\text{fullcoh}}}) \\ \text{coh}^{n+1}_{\text{painting}} &\quad \text{deps}^{n}_{\text{fullcoh}} \triangleq \text{unit} \\ \text{coh}^{n+1, [0, p]}_{\text{painting}} &\quad \text{deps}^{n}_{\text{fullcoh2}} \triangleq (\text{coh}^{n+1, [0, p-1]}(\overline{\text{deps}^{n}_{\text{fullcoh2}}}), \text{coh}^{n+1, p}_{\text{painting}}(\overline{\text{deps}^{n}_{\text{fullcoh2}}})) \end{align*} $$

## 3.11 Completing the construction by induction ⚙

Armed with all the constructions, we are now able to specify the whole structure on which we can reason by induction, for $D: \text{vSet}_m^{<n+1}$ given:

$$ \begin{align*} \text{frame}^{n, [0,n]} & : & \text{FRAME}^{n, [0,n]} \\ \text{painting}^{n, [0,n]} & : & \text{PAINTING}^{n, [0,n]}(\text{frame}^{n, [0,n]}) \\ \text{restr}^{n, [0,n]}_{\text{frame}} & : & \text{restr}^{n, [0,n]}_{\text{FRAME}} \left( \begin{array}{l} \text{frame}^{n, [0,n]} \\ \text{painting}^{n, [0,n]} \end{array} \right) \\ \text{deps}^{n, [0,n]}_{\text{restr}} & \triangleq & \left( \begin{array}{l} \text{frame}^{n, [0,n]} \\ \text{painting}^{n, [0,n]} \\ \text{restr}^{n, [0,n]}_{\text{frame}} \end{array} \right) \\ \text{deps}^{n}_{\text{fullrestr}}(E) & \triangleq & \left( \begin{array}{l} \text{deps}^{n}_{\text{restr}}(E) \\ E \end{array} \right) \\ \text{restr}^{n, [0,n]}_{\text{painting}}(E) & : & \text{restr}^{n, [0,n]}_{\text{PAINTING}}(\text{deps}^{n}_{\text{fullrestr}}(E)) \\ \text{coh}^{n, [0,n]}_{\text{frame}}(E) & : & \text{coh}^{n, [0,n]}_{\text{FRAME}} \left( \begin{array}{l} \text{deps}^{n}_{\text{fullrestr}}(E) \\ \text{restr}^{n, [0,n]}_{\text{frame}}(E) \end{array} \right) \\ \text{deps}^{n}_{\text{coh}}(E) & \triangleq & \left( \begin{array}{l} \text{deps}^{n}_{\text{fullrestr}}(E) \\ \text{restr}^{n, [0,n]}_{\text{painting}}(E) \\ \text{coh}^{n, [0,n]}_{\text{frame}}(E) \end{array} \right) \\ \text{deps}^{n}_{\text{fullcoh}}(E)(E') & \triangleq & \left( \begin{array}{l} \text{deps}^{n}_{\text{coh}}(E) \\ E' \end{array} \right) \\ \text{coh}^{n, [0,n]}_{\text{painting}}(E)(E') & : & \text{coh}^{n, [0,n]}_{\text{PAINTING}}(\overline{\text{deps}^{n}_{\text{fullcoh}}(E)(E')}) \end{align*} $$
where

$$E : \mathit{frame}^{n+1,n+1}(\mathit{deps}_{\mathit{restr}}^{n,[0,n]}) \to \mathit{HSet}$$

$$E' : \mathit{frame}^{n+2,n+2}(\overline{\mathit{deps}_{\mathit{restr}}}(\mathit{deps}_{\mathit{coh}}^{n,[0,n]}(E))) \to \mathit{HSet}$$

To lift from level $n$ from level $n+1$, it is then enough to assume $E$ at level $n+1$. We get $\mathit{deps}_{\mathit{restr}}^{n,[0,n]}$ from the assumptions at level $n$ and we can build the following:

- $\mathit{frame}^{n+1,[0,n+1]}$ comes from $\mathit{deps}_{\mathit{restr}}^{n,[0,n]}$ (section 3.3).

- $\mathit{painting}^{n+1,[0,n+1]}$ comes from $\mathit{deps}_{\mathit{fullrestr}}^n(E)$ (section 3.4).

- $\mathit{restr}_{\mathit{frame}}^{n+1,[0,n+1]}$ comes from $\mathit{deps}_{\mathit{coh}}^{n,[0,n]}(E)$ (section 3.6).

- $\mathit{restr}_{\mathit{painting}}^{n+1,[0,n+1]}(E')$ comes from $\mathit{deps}_{\mathit{fullcoh}}^n(E)(E')$ (section 3.7).

- we define $\mathit{deps}_{\mathit{coh2}}^{n,[0,n]}(E)(E')$ from $\mathit{deps}_{\mathit{fullcoh}}^n(E)(E')$ and $\mathit{coh}_{\mathit{painting}}^{n,[0,n]}(E)(E')$.

- $\mathit{coh}_{\mathit{frame}}^{n+1,[0,n+1]}(E')$ comes from $\mathit{deps}_{\mathit{coh2}}^{n,[0,n]}(E)(E')$ (section 3.9).

- we define $\mathit{deps}_{\mathit{fullcoh2}}^n(E)(E')(E'')$, for $E'' : \mathit{frame}^{n+3,n+3}(\overline{\mathit{deps}_{\mathit{restr}}(\overline{\mathit{deps}_{\mathit{coh}}(\mathit{deps}_{\mathit{coh2}}^{n,[0,n]})}))} \to \mathit{HSet}$, from $\mathit{deps}_{\mathit{coh2}}^{n,[0,n]}(E)(E')$ and $E''$.

- $\mathit{coh}_{\mathit{painting}}^{n+1,[0,n+1]}(E')(E'')$ comes from $\mathit{deps}_{\mathit{fullcoh2}}^n(E)(E')(E'')$ (section 3.10).

Therefore, assuming a construction of $\mathit{frame}^{n,n}$ from $D : \mathcal{v}\mathit{Set}_m^{<n+1}$, we are able to build a $\mathit{frame}^{n+1,n+1}$ from $D$ extended with some $E : \mathit{frame}^{n+1,n+1}(\mathit{deps}_{\mathit{restr}}^{n,[0,n]}) \to \mathit{HSet}$. This is enough to build $\mathcal{v}\mathit{Set}_m^{<n+1}(D)$, for $D : \mathcal{v}\mathit{Set}_m^{<n+1}$, and thus $\mathcal{v}\mathit{Set}_m$, by starting with an empty $D$, since all fields of the structure are trivially inhabited by $\star$ when $n=0$.

## 4 Differences between presentation and Rocq formalisation

- The formalisation is not parameterised by $n$ but instead by $k \triangleq n - p$. This makes the presentation less intuitive since the dimension has to be mentally recomputed by adding $p$ to $k$, but it eases formalisation. The interesting information when building some component up to $p$ is not the dimension, but the distance from to the expected dimension, computationally speaking.

- The structures $\mathit{deps}_{\mathit{fullrestr}}$, $\mathit{deps}_{\mathit{fullcoh}}$ and $\mathit{deps}_{\mathit{fullcoh2}}$ from the informal presentation are implemented by using a "zipper" structure [12]: anytime we build some construction at $p$, we split $\mathit{frame}^{n,[0,n]}$ into two lists constructed in opposite directions: $\mathit{frame}^{n,[0,p-1]}$ and $\mathit{frame}^{n,[p,n]}$, which aids in proofs of induction on $p$.

- In section 3, we left implicit the management of inequality proofs occurring in restrictions and coherence conditions. In practice, we stated inequalities as strict propositions [8], or propositions whose proofs are all definitionally equal, which simplified formalisation.

- Rocq does not support mutual fixpoints for which one component depends on another component in its type<fnref n="5" />, nor mutual fixpoints including abbreviations, as we expect in sections 3.3, 3.6, and 3.9. We address the absence of abbreviations by defining abbreviations in advance and address the absence of recursive-recursive definitions by instead recursively building the $\Sigma$-type of the two components of the recursive-recursive definition, and recovering the individual components using projections.

<footnote n="5">⁵ also termed as a recursive-recursive definition [6]</footnote>
# 5 Comparison with previous work

To address the dependency of $restr_{frame}^{n,p}$ in frame$^{n+1,p}$, and that of $coh_{frame}^{n,p}$ in frame$^{n+2,p}$ and $restr_{frame}^{n+1,p}$ without having to mix the specification of the induction hypothesis and the construction of the next step, the previous work [10] was assuming all of frame$^{n,p}$, frame$^{n+1,p}$, frame$^{n+2,p}$, $restr_{frame}^{n,p}$, $restr_{frame}^{n+1,p}$, and $coh_{frame}^{n,p}$ together with propositional equations defining frame$^{n+1,p}$, frame$^{n+2,p}$, and $restr_{frame}^{n+1,p}$. The induction step then constructed frame$^{n+3,p}$, $restr_{frame}^{n+2,p}$ and $coh_{frame}^{n+1,p}$ and inherited frame$^{n+1,p}$, frame$^{n+2,p}$ and $restr_{frame}^{n+1,p}$ from the induction hypothesis. The current work can be seen as the result of analysing how dependencies are finely organised so that those propositional equations are replaced by definitions of frame$^{n+1,p}$, frame$^{n+2,p}$ and $restr_{frame}^{n+1,p}$. In other words, in the previous work, the induction hypothesis combines assumptions of the form frame$^{n+1,p}$: HSet with equations of the form frame$^{n+1,0}$ = unit and frame$^{n+1,p+1}$ = $\Sigma d: frame^{n+1,p} \Pi e. painting^{n,p} (restr_{frame,0,e}^{n,p}(d))$. These are replaced by a *definition* of frame$^{n+1,p}$. And similarly for frame$^{n+2,p}$, $restr_{frame}^{n+1,p}$, as well as for painting$^{n+1,p}$, painting$^{n+2,p}$, $restr_{painting}^{n+1,p}$, in the current work.

# 6 Perspectives

Our construction shows a pattern: start from FRAME, define PAINTING, mutually define frame and $restr_{FRAME}$, define painting, define $restr_{PAINTING}$, mutually define $restr_{frame}$ and $coh_{FRAME}$, define $restr_{painting}$, define $coh_{PAINTING}$, mutually define $coh_{frame}$ and $coh_{2FRAME}$, define $coh_{PAINTING}$. On HSet, $coh_{2FRAME}$ is trivially provable and the construction stops here. If we were working in an untruncated universe $U$, the construction would continue recursively: prove the coherence at dimension $i$ on frames mutually with the type of coherence on frames at dimension $i+1$, prove the coherence on paintings at dimension $i$, define the type of coherence on paintings at dimension $i+1$. Such an infinite process can again be represented using streams, so that from a stream at level $n$, a stream at level $n+1$ can be built, as in section 3. This would solve the semi-simplicial type problem [14].

# References

1. Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus. Extending homotopy type theory with strict equality. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, volume 62 of LIPIcs, pages 21:1-21:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. With a formalization in . doi:10.4230/LIPIcs.CSL.2016.21.

2. Robert Atkey, Neil Ghani, and Patricia Johann. A relationally parametric model of dependent type theory. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014., 2014.

3. Jean-Philippe Bernardy, Thierry Coquand, and Guilhem Moulin. A presheaf model of parametric type theory. Electr. Notes Theor. Comput. Sci., 319:67-82, 2015. doi:10.1016/j.entcs.2015.12.006.

4. Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. Parametricity and dependent types. In Paul Hudak and Stephanie Weirich, editors, Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010, pages 345-356. ACM, 2010. URL: http://doi.acm.org/10.1145/1863543.1863592, doi:10.1145/1863543.1863592.

5. Jean-Philippe Bernardy and Guilhem Moulin. A computational interpretation of parametricity. In 2012 27th Annual IEEE Symposium on Logic in Computer Science, pages 135-144. IEEE, 2012.
6 Fredrik Nordvall Forsberg. *Inductive-inductive definitions*. PhD thesis, Swansea University, UK, 2013. URL: https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.752308.

7 Neil Ghani, Fredrik Nordvall Forsberg, and Federico Orsanigo. Proof-relevant parametricity. In Sam Lindley, Conor McBride, Philip W. Trinder, and Donald Sannella, editors, *A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday*, volume 9600 of *Lecture Notes in Computer Science*, pages 109–131. Springer, 2016.

8 Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. Definitional proof-irrelevance without K. *Proc. ACM Program. Lang.*, 3(POPL):3:1–3:28, 2019. doi:10.1145/3290316.

9 Hugo Herbelin. A dependently-typed construction of semi-simplicial types. *Mathematical Structures in Computer Science*, 25(5):1116–1131, 2015.

10 Hugo Herbelin and Ramkumar Ramachandra. A parametricity-based formalization of semi-simplicial and semi-cubical sets. *Mathematical Structures in Computer Science*, 35:e13, 2025. doi:10.1017/S096012952500009X.

11 Jason J. Hickey. Formal objects in type theory using very dependent types. In *FOOL 3: The Third International Workshop on Foundations of Object-Oriented Languages*, July 1996. URL: https://api.semanticscholar.org/CorpusID:14983194.

12 Gérard P. Huet. The zipper. *J. Funct. Program.*, 7(5):549–554, 1997. URL: https://doi.org/10.1017/s0956796897002864, doi:10.1017/S0956796897002864.

13 Patricia Johann and Kristina Sojakova. Cubical categories for higher-dimensional parametricity. *CoRR*, abs/1701.06244, 2017. URL: http://arxiv.org/abs/1701.06244, arXiv:1701.06244.

14 Peter LeFanu Lumsdaine. Semi-simplicial types, September 2012. URL: https://web.archive.org/web/20180728221737/http://uf-ias-2012.wikispaces.com/Semi-simplicial+types.

15 Fedor Part and Zhaohui Luo. Semi-simplicial types in logic-enriched homotopy type theory. *CoRR*, abs/1506.04998, 2015. URL: http://arxiv.org/abs/1506.04998, arXiv:1506.04998.

16 Gordon D. Plotkin. Lambda-definability and logical relations. Technical Report Memorandum SAI-RM-4, Univ. of Edinburgh, School of Artificial Intelligence, 1973.

17 John C. Reynolds. Types, abstraction and parametric polymorphism. In R. E. A. Mason, editor, *Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19-23, 1983*, pages 513–523. North-Holland/IFIP, 1983.

18 William W. Tait. Intensional interpretations of functionals of finite type i. *Journal of Symbolic Logic*, 32(2):198–212, 1967.

19 Vladimir Voevodsky. Semi-simplicial types, Nov 2012. Briefly described in Section 8 of [9].