Liqian Chen
email: lqchen@nudt.edu.cn

Jiangchao Liu
email: jliu@di.ens.fr

Antoine Miné
email: mine@di.ens.fr

Deepak Kapur
email: kapur@cs.unm.edu

Ji Wang

An Abstract Domain to Infer Octagonal Constraints with Absolute Value ⋆

HAL is

Introduction

The precision and efficiency of program analysis based on abstract interpretation [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF][START_REF] Cousot | Systematic design of program analysis frameworks[END_REF] rely a lot on the chosen abstract domains. Most existing numerical abstract domains (such as intervals [START_REF] Cousot | Static determination of dynamic properties of programs[END_REF], octagons [START_REF] Miné | The octagon abstract domain[END_REF], polyhedra [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF], etc.) can only express convex sets, due to the fact that they usually utilize a conjunction of convex constraints to represent abstract elements. At control-flow joins in programs, an abstract domain often exploits a join operation to abstract the disjunction (union) of the convex constraint sets from the incoming edges into a conjunction of new convex constraints. The convexity limitations of abstract domains may lead to imprecision in the analysis and thus may cause many false alarms. E.g., to remove a division-by-zero false alarm, the analysis needs to find a range excluding 0 for the divisor, which is in general a non-convex property and may be out of the reasoning power of convex abstract domains.

The Absolute Value (AV) function is one of the most used functions in mathematics and widely used in numerical computations. The AV function is supported by many modern program languages. E.g., the C99 standard for the C programming language provides the abs() and fabs() functions to compute the absolute value of an integer number and a floating-point number respectively. However, due to non-convexity, the AV function in the program code is rarely well handled during program analysis. Moreover, the AV function has natural ability to encode disjunctions of linear constraints in a program that account for a large class of non-convex constraints in practice. E.g., x ≤ -1 ∨ x ≥ 1 can be encoded as |x| ≥ 1, while (x 1 ∨ y 2) can be encoded as |x -1| + |y -2| > 0. Hence, we could exploit the non-convex expressiveness of the AV function to design non-convex abstract domains. Based on this insight, in [START_REF] Chen | Linear absolute value relation analysis[END_REF], Chen et al. proposed an abstract domain of linear AV inequalities but which is exponential in complexity and thus has scalability limitations in practice.

In this paper, we propose a new abstract domain, namely the abstract domain of octagonal constraints with absolute value (AVO), to infer relations of the form {±X ± Y ≤ c, ±X ±|Y| ≤ d, ±|X|±|Y| ≤ e} over each pair of variables X, Y in the program where constants c, d, e ∈ R are automatically inferred by the analysis. AVO is more expressive than the classic octagon abstract domain and allows expressing certain non-convex (even unconnected) sets, thanks to the non-convex expressiveness of the AV function. We propose several closure algorithms over AV octagons to offer different time-precision tradeoffs. On this basis, we provide algorithms for domain operations such that the new domain still enjoys the same asymptotic complexity as the octagon domain. In addition, we show how to extend AVO to support strict inequalities over rational or real-valued variables. In other words, after the extension, AVO can additionally infer relations that are of the form {±X±Y < c, ±X±|Y| < d, ±|X|±|Y| < e}. Experimental results of our prototype are encouraging on benchmark programs and large embedded C programs; AVO is scalable to large-scale programs and able to find non-convex invariants of interest in practice.

Motivating Example. In Fig. 1, we show a small instructive example adapted from [START_REF] Ghorbal | Donut domains: Efficient non-convex domains for abstract interpretation[END_REF] (by replacing the double type by real type), which is originally extracted from the XTide1 package that provides tide and current predictions in various formats. It shows a frequently used pattern in implementing a Digital Differential Analyzer algorithm in computer graphics. This example is challenging to analyze as it involves complicated non-convex constraints (due to disjunctions, the usage of the AV function) as well as strict inequalities, and precise reasoning over these constraints is required to prove the absence of the potential risk of division-by-zero errors.

At location ① in Fig. 1, it holds that (dx 0∨dy 0) which describes a non-convex set of points that includes all points in R 2 except the origin (0, 0). Using octagonal constraints with absolute value, it can be encoded as -|dx| -|dy| < 0. At location ②, it holds that -|dx| -|dy| < 0 ∧ |dx| -|dy| < 0 which implies that -|dy| < 0 and thus the division by dy in the then branch will not cause division-by zero error. At location ③, it holds that -|dx| -|dy| < 0 ∧ -|dx| + |dy| ≤ 0 which implies that -|dx| < 0 and thus the division by dx in the else branch will not cause division-by zero error. However, if using convex abstract domains such as octagons and polyhedra, ⊤ (no information) will be obtained at ① and thus the division-by-zero false alarms will be issued in both the then and else branches. Moreover, since the program involves strict inequality tests, we need an abstract domain supporting strict inequalities to do precise reasoning. ...

} } Loc AV octagons ① -|dx| -|dy| < 0 -|dx| -|dy| < 0∧ ② |dx| -|dy| < 0∧ -|dy| < 0 -|dx| -|dy| < 0∧ ③ -|dx| + |dy| ≤ 0∧ -|dx| < 0
Fig. 1. Motivating example from [START_REF] Ghorbal | Donut domains: Efficient non-convex domains for abstract interpretation[END_REF] which is originally extracted from the XTide package.

The rest of the paper is organized as follows. Section 2 reviews the octagon abstract domain. Section 3 presents a new abstract domain of octagonal constraints with absolute value. Section 4 presents our prototype implementation together with experimental results. Section 5 discusses some related work before Section 6 concludes.

The octagon abstract domain

In this section, we give a brief review of the background of the octagon abstract domain and we refer the reader to [START_REF] Miné | The octagon abstract domain[END_REF] for details.

Octagon representation

Let V = {V 1 , . . . , V n } be a finite set of program variables in a numerical set I (which can be Q, or R). The octagon abstract domain manipulates a set of so-called octagonal constraints (also called Unit Two Variable Per Inequality or UTVPI constraints) that are of the form ±V i ± V j ≤ c where ± ∈ {-1, 0, +1} and c ∈ I. From the geometric point of view, the set of points satisfying a conjunction of octagonal constraints forms an octagon (the projection of which on a 2D plane parallel to the axes is a 8-sided polygon).

Potential Constraints. An octagonal constraint over V = {V 1 , . . . , V n } can be reformulated as a so-called potential constraint that is of the form

V ′ i -V ′ j ≤ c over V ′ = {V ′ 1 , . . . , V ′ 2n } where V ′ 2k-1 represents +V k and V ′ 2k represents -V k . E.g., the octag- onal constraint V i + V j ≤ c can be encoded as either V ′ 2i-1 -V ′ 2 j ≤ c or V ′ 2 j-1 -V ′ 2i ≤ c. Moreover, a unary octagonal constraint such as V i ≤ c (and -V i ≤ c) can be encoded as V ′ 2i-1 -V ′ 2i ≤ 2c (and V ′ 2i -V ′ 2i-1 ≤ 2c
). A conjunction of potential constraints can be represented as a directed weighted graph G with nodes V ′ and edges labeled with weights in I. For each constraint V ′ j -V ′ i ≤ c in the constraint conjunction, there will be an edge from V ′ i to V ′ j labelled with weight c in G. Difference Bound Matrices. An equivalent but more practical representation for the conjunction of potential constraints C over n variables is to use a Difference Bound Matrix (DBM) [START_REF] Dill | Timing assumptions and verification of finite-state concurrent systems[END_REF]. A DBM representing C is a n × n matrix M defined by

M i j def = inf{ c | (V j -V i ≤ c) ∈ C}
where inf(∅) = +∞ and n is the number of variables involved in C. For a set of potential constraints described by a DBM M of dimension n, we define the following concretization function γ Pot : DBM → P(V → I):

γ Pot (M) def = { (V 1 , . . . , V n ) ∈ I n | ∀i, j, V j -V i ≤ M i j }.
Similarly, for a set of octagonal constraints described by a DBM M of dimension 2n, we define the following concretization function γ Oct : DBM → P(V → I):

γ Oct (M) def = { (V 1 , . . . , V n ) ∈ I n | (V 1 , -V 1 , . . . , V n , -V n ) ∈ γ Pot (M) }.
Some octagonal constraints over V have two different encodings as potential constraints over V ′ , and thus can be represented by two elements in the DBM. E.g., V i + V j ≤ c can be described by either

V ′ 2i-1 -V ′ 2 j ≤ c (i.e., M (2 j)(2i-1) = c) or V ′ 2 j-1 -V ′ 2i ≤ c (i.e., M (2i)(2 j-1) = c).
To ensure that elements of such pairs encode equivalent constraints, we define the coherence of a DBM as

M is coherent ⇐⇒ ∀i, j, M i j = M  ī
where the • operator on indices is defined as:

ī def = i + 1 if i is odd i -1 if i is even
Let DBM denote the set of all DBMs. We enrich DBM with a new smallest element, denoted by ⊥ DBM . Then we get a lattice (DBM, ⊑ DBM , ⊔ DBM , ⊓ DBM , ⊥ DBM , ⊤ DBM ) where

M ⊑ DBM N def ⇐⇒ ∀i, j, M i j ≤ N i j (M ⊔ DBM N) i j def = max(M i j , N i j ) (⊤ DBM ) i j def = +∞ (M ⊓ DBM N) i j def = min(M i j , N i j )

Closure

An octagon can still have several distinct representations using coherent DBMs. To compare octagons, we thus construct a normal form on DBMs to represent octagons.

The octagon abstract domain utilizes a so-called strong closure of the DBM, as the normal form for a non-empty DBM representing octagons. The strong closure (denoted as M • ) of a DBM M encoding octagonal constraints is defined as:

M • def = inf ⊑ DBM {X ♯ ∈ DBM | γ Oct (M) = γ Oct (X ♯ )}
The octagon domain uses a modified version of the Floyd-Warshall algorithm to compute M • (which is firstly proposed by Miné [START_REF] Miné | The octagon abstract domain[END_REF] and later improved by Bagnara et al. [START_REF] Bagnara | Widening operators for weakly-relational numeric abstractions[END_REF]), which is of cubic-time complexity. Strong closure is a basic operator in the octagon domain. Most abstract operators over octagons can be obtained based on the strong closure of DBMs. We refer the reader to [START_REF] Miné | The octagon abstract domain[END_REF] for details.

An abstract domain of octagonal constraints with absolute value

In this section, we show how to extend the octagon abstract domain with absolute value.

Octagonal constraints with absolute value

A constraint is said to be an AV octagonal constraint if it is of the following forms:

• octagonal constraints: ±V i ± V j ≤ a • constraints with absolute value of one variable per inequality: ±V i ± |V j | ≤ b • constraints with absolute value of two variables per inequality: ±|V i | ± |V j | ≤ c
where ± ∈ {-1, 0, +1} and a, b, c ∈ I ∪ {+∞}. From the geometric point of view, we call AV octagon the geometric shape of the set of points satisfying a conjunction of AV octagonal constraints. Now, we will design a new abstract domain, namely AVO, to infer AV octagonal constraints among program variables V = {V 1 , . . . , V n }.

According to Theorem 1 in [START_REF] Chen | Linear absolute value relation analysis[END_REF], it is easy to derive the following theorem.

Theorem 1. Let e be an arbitrary expression that does not involve variable X. Then

|X| + e ≤ c ⇐⇒ X + e ≤ c -X + e ≤ c
A direct consequence of Theorem 1 is that those constraints with positive coefficients on the AV term are redundant with other AV octagonal constraints and do not bring additional expressiveness. Hence, in the domain representation of AVO, we only need to encode AV octagonal constraints of the following forms:

• ±V i ± V j ≤ a • ±V i -|V j | ≤ b • -|V i | -|V j | ≤ c
For example, to describe a planar AV octagon over program variables x, y, we only need to consider at most 15 AV octagonal constraints, which are listed in Fig. 4(a).

Due to the non-convexity expressiveness of the AV function, an AV octagon is nonconvex in general, but its intersection with each orthant in R n gives a (possibly empty)

C = {x ≤ 4, -x ≤ 4, y ≤ 4, -y ≤ 4, x + y ≤ 7, x -y ≤ 7, -x + y ≤ 7, -x -y ≤ 7}; (b) depicts -|x| ≤ -1; (c) depicts -|x| + y ≤ 2; (d) depicts -|x| -y ≤ 2; (e) depicts -|x| -|y| ≤ -4; (f) depicts an AV octagon with constraint set C ′ = C ∪ {-|x| ≤ -1, -|y| ≤ -1, -|x| + y ≤ 2, -|x| -y ≤ 2, x -|y| ≤ 2, -x -|y| ≤ 2, -|x| -|y| ≤ -4}.
octagon. Fig. 2 shows typical geometric shape of AV octagonal constraints. In particular, Fig. 2(a) shows a typical shape of octagons, while Fig. 2(f) shows an example of an AV octagon that is non-convex and even unconnected.

Expressiveness lifting. Note that in the AVO domain representation, the AV function | • | applies to only (single) variables rather than expressions. E.g., consider the relation y = ||x| -1| + 1 which encodes a piecewise linear function with more than two pieces, whose plot is shown in Fig. 3. The AVO domain cannot express directly this piecewise linear function (in the space of x, y), since | • | applies to an expression |x| -1. Indeed, in Fig. 3 the region in the orthant where both x and y are positive is not an octagon. In order to express such complicated relations, we follow the same strategy as in [START_REF] Chen | Linear absolute value relation analysis[END_REF]. We introduce new auxiliary variables to denote those expressions that appear inside the AV function. E.g., we could introduce an auxiliary variable ν to denote the value of the expression |x| -1. Then using AVO domain elements in the space with higher dimension (involving 3 variables: x, y, ν), such as {y = |ν| + 1, ν = |x| -1}, we could express complicated relations in the space over lower dimension (involving 2 variables: x, y), such as y = ||x| -1| + 1. Note that due to the octagonal shape, the expression inside the AV function can only be

e ::= ±X ± c | ±|e| ± c
where c is a constant and X is a variable.

Extending difference-bound matrices

Now, we show how to encode AV octagonal constraints using DBMs. Similarly to octagonal constraints, an AV octagonal constraint over {V 1 , . . . , V n } can be reformulated as a potential constraint of the form

V ′′ i -V ′′ j ≤ c over {V ′′ 1 , . . . , V ′′ 4n } where • V ′′ 4k-3 represents +V k , • V ′′ 4k-2 represents -V k , • V ′′ 4k-1 represents |V k |, • V ′′ 4k represents -|V k |.
As an example, in Fig. 4, we show a general set of constraints for a planar AV octagon (left) and its DBM representation (right). For a set of AV octagonal constraints described by a DBM M of dimension 4n, we define the following concretization function γ AVO : DBM → P(V → I):

x ≤ a 1 -x ≤ a 2 y ≤ a 3 -y ≤ a 4 x +y ≤ a 5 x -y ≤ a 6 -x +y ≤ a 7 -x -y ≤ a 8 -|x| ≤ b 1 -|y| ≤ b 2 -|x| +y ≤ b 3 -|x| -y ≤ b 4 x -|y| ≤ b 5 -x -|y| ≤ b 6 -|x| -|y| ≤ c 1 (a) x -x |x| -|x| y -y |y| -|y| x 0 2a 2 -x 2a 1 0 |x| 0 2b 1 -|x| 0 y a 6 a 8 b 4 0 2a 4 -y a 5 a 7 b 3 2a 3 0 |y| b 5 b 6 c 1 0 2b 2 -|y| 0 (b)
γ AVO (M) def = (V 1 , . . . , V n ) ∈ I n | (V 1 , -V 1 , |V 1 |, -|V 1 |, . . . , V n , -V n , |V n |, -|V n |) ∈ γ Pot (M) .
Some AV octagonal constraints have two different encodings as potential constraints in V ′′ , and can be represented by two elements in the DBM. E.g.,

-|V i | -|V j | ≤ c can be described by either V ′′ 4 j -V ′′ 4i-1 ≤ c (i.e., M (4i-1)(4 j) = c) or V ′′ 4i -V ′′ 4 j-1 ≤ c (i.e., M (4 j-1)(4i) = c).
In addition, according to the specific property over AV constraints shown in Theorem 1, DBMs encoding AV octagons have another restriction, i.e.,

e + V i ≤ c 1 ∧ e -V i ≤ c 2 =⇒ e + |V i | ≤ max(c 1 , c 2 ) ( 1
)
where e ∈ {±V j , ±|V j |}. To this end, we define the AV coherence of a DBM as

M is AV coherent ⇐⇒          ∀i, j, M i j = M  ī ∀ j, k, M (4k) j = max(M (4k-3) j , M (4k-2) j ) if j 4k ∀i, k, M i(4k-1) = max(M i(4k-2) , M i(4k-3) ) if i 4k -1
The first condition is similar to the coherence condition for DBMs that encode octagons. The second condition is due to the restriction (1) over the -|V k | row, while the third condition is due to the restriction (1) over the |V k | column.

Conversions between octagons and AV octagons

The intersection of an AV octagon with each orthant gives an octagon. Based on this insight, we now present operators for conversions between octagons and AV octagons. Let u = (1, . . . , 1) T be the unit vector, and S n = {s ∈ R n | |s| = u}. We define an operator C = S2Cons(s) to derive a conjunction C of sign constraints from s ∈ S n , such that

C i def = x i ≥ 0 if s i = 1 x i ≤ 0 if s i = -1
First, we define an operator AVO2Oct(M, s) to convert an AV octagon (described by M that is a DBM of dimension 4n) into an octagon (described by N that is a DBM of dimension 2n) with respect to a given orthant (described by s ∈ S n ), as:

N def = AVO2Oct(M, s)
such that γ Oct (N) equals to the solution set of the conjunction of S2Cons(s) with the constraint set corresponding to M. From the algorithmic view, N can be easily obtained from M, by considering the sign of each variable defined in s. E.g.,

N (2k-1)(2k) = M (4k-3)(4k-2) if s k = -1 min(M (4k-3)(4k-2) , M (4k-1)(4k) ) if s k = 1 where M (4k-3)(4k-2) and M (4k-1)(4k) denote the upper bounds for (-V k ) -V k and (-|V k |) - |V k | respectively. If V k ≥ 0, we know the upper bound for (-V k ) -V k (denoted by N (2k-1)(2k)
in the DBM representation of octagons) will be min(M (4k-3)(4k-2) , M (4k-1)(4k) ).

Note that an octagon itself is an AV octagon. However, if we know the orthant that an octagon lies in, we could deduct additionally upper bounds for AV expressions (such as -|X| -|Y|), to saturate the DBM. To this end, we define an operator Oct2AVO(N, s) to convert an octagon (N) in a given orthant (s ∈ S n ) into an AV octagon (M), as:

M def = Oct2AVO(N, s)
such that the solution set of the conjunction of the constraint set corresponding to M with S2Cons(s) is equivalent to γ Oct (N).

Closure algorithms

To obtain a unique representation for a non-empty AV octagon, we define the so-called AV strong closure M |•| for a DBM encoding a non-empty AV octagon, as

M |•| def = inf ⊑ DBM {X ♯ ∈ DBM | γ AVO (M) = γ AVO (X ♯ )}
Strong closure by enumerating the signs of all n variables. We provide an approach to compute the AV strong closure M |•| by enumerating the signs of all n variables:

AVOStrClo(M) def = ⊔ DBM s∈S n M ′ ∈ DBM | M ′ = Oct2AVO(N • , s), N = AVO2Oct(M, s)
The intuition is as follows. The intersection of an AV octagon M with each orthant s gives an octagon N. Hence, we could enumerate all orthants and in each orthant we compute the AV strong closure via the regular strong closure of the octagon domain. It M/{V k , V i , V j } denotes the sub-matrix of M consisting of the rows and columns corresponding to variables in {V k , V i , V j }.

1 DBM 4n×4n WeakCloVia3Sign(M : DBM 4n×4n ){ 2 M ′ , M ′′ , M ′|•| : DBM 12×12 ; 3 N : DBM 6×6 ; 4 for k ← 1 to n 5 for i ← 1 to n 6 for j ← 1 to n { 7 M ′ ← M/{V k , V i , V j }; 8 M ′|•| ← ⊔ DBM s∈S 3 {M ′′ ∈ DBM | M ′′ = Oct2AVO(N • , s), N = AVO2Oct(M ′ , s)}; 9 M/{V k , V i , V j } ← M ′|•| ; } 10 for i ← 1 to 4n 11 if (M ii < 0) return ⊥ DBM ; else M ii ← 0;
is not hard to see that AVOStrClo(M) = M |•| . However, the time complexity of this approach is O(2 n ×n 3 ). At the moment, we do not know whether the problem of computing the AV strong closure for AV octagons is NP-hard or not.

To offer different time-precision tradeoffs, we now propose two approaches that are of cubic time complexity to compute weak closures M • (such that M |•| ⊑ DBM M • ) for AV octagons. Note that the key behind the closure algorithm is to combine the constraints over (V i , V k ) and those over (V k , V j ) to tighten the constraints over (V i , V j ), by constraint propagation through the intermediate variable V k . Based on this insight, we first propose a weak closure algorithm WeakCloVia3Sign() by enumerating the signs of 3 variables {V i , V k , V j } each time to perform constraint propagation. Then we propose a cheaper weak closure algorithm WeakCloVia1Sign() by enumerating only the sign of the intermediate variable V k each time to perform constraint propagation.

Weak closure by enumerating the signs of 3 variables each time. In Fig. 5, we show the WeakCloVia3Sign() algorithm. In the loop body, we compute the AV strong closure among three variables V i , V k , V j (by enumerating 8 orthants due to the signs of 3 variables), and then update the tightened constraints over V i , V k , V j in the original DBM. Note that WeakCloVia3Sign() gives AV strong closure for AV octagons involving only 3 variables. However, in general, WeakCloVia3Sign() does not guarantee to result in the AV strong closure for more than 3 variables.

Weak closure by enumerating the sign of one variable each time. In Fig. 7, we show the WeakCloVia1Sign() algorithm. Rather than enumerating the signs of 3 variables, in the loop body of WeakCloVia1Sign() we enumerate only the sign of the intermediate variable V k . For each case of the sign of V k , we call TightenIJviaK() which is shown in Fig. 6 to tighten the constraints over {±V i , ±|V i |, ±V j , ±|V j |} by combining the constraints over {±V i , ±|V i |, ±V k } and those over {±V k , ±|V j |, ±V j }. We now explain how TightenIJviaK() works by considering the case where

V k ≥ 0. When V k ≥ 0, we have |V k | = V k . Hence, it holds that V ′′ -|V k | ≤ c =⇒ V ′′ -V k ≤ c where V ′′ ∈ {0, ±V i , ±|V i |, ±V j , ±|V j |}. Then, we use V ′′ -|V k | ≤ c to tighten the upper bound // V k -V ′′ n ≤ c ∧ V ′′ m -V k ≤ d =⇒ V ′′ m -V ′′ n ≤ c + d where V ′′ n , V ′′ m ∈ V ′′ \ {0} 18
return M ′ ; } Fig. 6. A algorithm to tighten AV constraints between V i and V j through V k .

for

V ′′ -V k . E.g., if we have -V k ≤ c 1 and -|V k | ≤ c 2 in the input DBM, we can derive a upper bound for -V k as -V k ≤ min(0, c 1 , c 2 )
, which corresponds to line 5 in TightenIJviaK(). After line 14, the information over the rows and columns corresponding to ±|V k | in the DBM becomes redundant. Hence, from line 14 to line 16, we only need to consider the propagation through ±V k (without need through ±|V k |). Overall, WeakCloVia1Sign() is less precise but cheaper than WeakCloVia3Sign().

1

DBM 4n×4n WeakCloVia1Sign(M : DBM 4n×4n ){ 2 M ′ , M ′|•| , N, N ′ : DBM 12×12 ; 3 for k ← 1 to n 4 for i ← 1 to n 5 for j ← 1 to n { 6 M ′ ← M/{V k , V i , V j }; 7 N ← TightenIJviaK(M ′ , true); // when V k ≥ 0 8 N ′ ← TightenIJviaK(M ′ , f alse); // when V k ≤ 0 9 M ′|•| ← N ⊔ DBM N ′ ; 10 M/{V i , V j } ← M ′|•| /{V i , V j }; } 11 for i ← 1 to 4n 12 for j ← 1 to 4n 13 M i j ← min(M i j , (M iī + M  j )/2);
-z ≤ 164 y + x ≤ 58 y -z ≤ 132 -z ≤ 108 x -|z| ≤ 94 AV strong closure -|x| -z ≤ 86 x -z ≤ 112 WeakCloVia3Sign -|x| -z ≤ 86 x -z ≤ 142 WeakCloVia1Sign -|x| -z ≤ 108 x -z ≤ 142
Fig. 8. An example of applying 3 closure algorithms on the same initial constraint set.

Example 1. In Fig. 8, we apply the above 3 closure algorithms on the same initial set of constraints. The AV strong closure finds xz ≤ 112 while WeakCloVia3Sign() and WeakCloVia1Sign() are less precise and can only find xz ≤ 142. Moreover, WeakCloVia1Sign() gives less precise result -|x|z ≤ 108 than WeakCloVia3Sign() which can find -|x|z ≤ 86.

Other domain operations

Closure is a basic operator in the AVO domain. Most abstract operators over AV octagons can be obtained following similar ideas as those over octagons by replacing strong closure with AV strong closure (if necessary). In practice, since our AV strong closure is of exponential-time complexity, we use weak closure instead. When we use weak closure, all the AVO domain operations can be O(n 3 ) in the worst case. However, we do not have a normal form for AV octagons when using weak closure, and most domain operations are not guaranteed to be the best abstraction. E.g., for the inclusion test, we have γ AVO (M) ⊆ γ AVO (N) ⇐⇒ M |•| ⊑ DBM N when using AV strong closure.

If we use any of our weak closures, denoted as

M |•| , it holds that M |•| ⊑ DBM N =⇒ γ AVO (M) ⊆ γ AVO (N) but it may not hold that γ AVO (M) ⊆ γ AVO (N) =⇒ M |•| ⊑ DBM N.
For test transfer functions, first, constraints in the tests are abstracted into AV octagonal constraints, following similar ideas as abstracting arbitrary constraints into octagonal constraints [START_REF] Miné | The octagon abstract domain[END_REF]. Moreover, we employ AVO join operation to try to encode disjunctive constraints in tests as conjunctive AV octagonal constraints. E.g., consider the condition that holds at ① in Fig. 1, i.e., |dx| 0 ∨ |dy| 0. The disequality |dx| 0 which itself can be rewritten as a disjunction dx < 0 ∨ -dx < 0, can be encoded as -|dx| < 0 by the AVO join operation. Then, -|dx| < 0 ∨ -|dy| < 0 can be further encoded as -|dx| -|dy| < 0 by the AVO join operation. Hence, even when the original condition test does not involve AV, AV may be introduced during constraint abstraction. After the process of constraint abstraction, the AV octagonal constraints derived from the tests are then used to tighten the current AVO abstract element.

For assignment transfer functions, we allow the right-hand side expression to involve AV, such as x := ±|y| ± c. However, we can simply transform assignments with AV into conditional branches with assignments that do not involve AV. E.g., the assignment x := a * |e| + c where a, e, c are expressions, can be transformed into: if (e ≥ 0) then x := a * e + c; else x := -a * e + c; fi.

Supporting strict inequalities

In practice, strict inequalities (such as |x| + |y| > 0) may appear in branch conditions of a program. To this end, we extend the AVO domain to support strict inequalities. In the domain representation, we maintain a boolean matrix S of the same size as the DBM M that encodes an AV octagon, such that

S i j def = 0 if V ′′ j -V ′′ i < M i j 1 if V ′′ j -V ′′ i ≤ M i j
We define the order over pairs (m, s)'s where m ∈ I and s ∈ {0, 1}, as

(m, s) ⊑ (m ′ , s ′ ) def ⇐⇒ (m < m ′ ) ∨ (m = m ′ ∧ s ≤ s ′ ))
Note that ⊑ is a total order on (I, bool), i.e., at least one of (m, s) ⊑ (m ′ , s ′ ) and (m ′ , s ′ ) ⊑ (m, s) holds. Let DBMS denote the set of all pairs of DBMs and boolean matrices. A lattice over DBMS can be obtained by "lifting" the operations from DBM and the boolean matrices element-wise. In addition, we define the addition over DBMS as:

(M ik , S ik ) + (M k j , S k j ) def = (M ik + M k j , S ik &S k j )
Then in the abstract domain supporting strict inequalities, all domain operations can be adapted from the domain that supports only non-strict inequalities by replacing operations over DBM with operations over DBMS. E.g., in the AVO domain supporting strict inequalities, the emptiness test is to check whether it holds that ∃i, M ii < 0∨(S ii = 0 ∧ M ii = 0). Whereas, in the regular AVO domain, we only need to check whether it holds that ∃i, M ii < 0.

Implementation and experimental results

We have implemented the AVO domain in the APRON abstract domain library [START_REF] Jeannet | Apron: A library of numerical abstract domains for static analysis[END_REF].

Experimental comparison of three closure algorithms

We first compare in precision and efficiency the three closure algorithms proposed in Sect.3.4 for AV octagons. We conduct our experiments on randomly generated DBMs (of dimension 4n but partially initialized) over different numbers of variables (n). The experimental result is shown in Fig . 9. "♯cases" gives the number of test cases for each such number n. "str" denotes the AV strong closure algorithm, "wk3s" denotes WeakCloVia3Sign(), and "wk1s" denotes WeakCloVia1Sign(). "%same results" shows the percentage of test cases where the two compared algorithms give the same resulting DBMs. The column "%different elements" presents the average percentage of the number of different elements in the resulting DBMs to the size of the DBMs, when the two compared algorithms produce different resulting DBMs.

From the result, we can see that WeakCloVia1Sign() is much more efficient than the other two closure algorithms. For those test cases where the two compared algorithms produce different resulting DBMs, the percentage of the number of different elements average time %same results %different elements ♯vars ♯cases str wk3s wk1s str= str= wk3s= str str wk3s wk3s wk1s wk1s wk3s wk1s wk1s 4 10000 2.4ms 7ms 0.19ms 94% 94% 99% 0.94% 0.79% 0.78% 8 1000 380ms 160ms 20ms 36% 28% 74% 0.83% 1.5% 0.26% 10 1000 5.7s 410ms 53ms 10% 5.3% 51% 1.1% 2.1% 0.18% in the resulting DBMs is very low. In other words, the two different resulting DBMs are mostly the same except for very few elements. During our experiments, at the moment, we found no test case for which weak closures give +∞ for an element where the strong closure gives a finite constant in the resulting DBMs.

Experiments on NECLA division-by-zero benchmarks

We have conducted experiments using the Interproc [START_REF] Lalire | Interproc[END_REF] static analyzer on the NECLA Benchmarks: Division-by-zero False Alarms [START_REF] Ghorbal | Donut domains: Efficient non-convex domains for abstract interpretation[END_REF]. The benchmark set is extracted from source code of several open-source projects. These programs illustrate commonly used techniques that programmers use to protect a division-by-zero (e.g., by using the AV function), and are challenging for analysis since they involve non-convex constraints (e.g., disjunctions, constraints involving the AV function) and strict inequalities. Fig. 10 shows the comparison of invariants inferred by AVO (using the weak closure algorithm WeakCloVia1Sign) with those by the octagon domain [START_REF] Miné | The octagon abstract domain[END_REF] and by the donut domain [START_REF] Ghorbal | Donut domains: Efficient non-convex domains for abstract interpretation[END_REF] (the main idea of which is to represent concrete object by the so-called hole that is the set minus of two convex sets). The motiv program corresponds to the motivating example (shown in Fig. 1) with its two branches. The column "WCfS" gives the weakest condition to prove the absence of the division-by-zero error in the program. The results given in the column "donut domain" are taken from [START_REF] Ghorbal | Donut domains: Efficient non-convex domains for abstract interpretation[END_REF] (using boxes to encode holes). From Fig. 10, we can see that the octagon domain fails to prove the absence of division-by-zero error for all programs since it cannot express non-convex properties nor strict inequalities. Our AVO domain succeeds to prove the absence of the division-by-zero errors for all programs including xcor on which the donut domain fails (due to its default heuristic for choosing holes).

0 dy ∈ [-∞, +∞] 1 |dy| > 0 0 motiv(else) dx 0 dx 0 0 dx ∈ [-∞, +∞] 1 |dx| > 0 0 gpc den 0 den [-0.1, 0.1] 0 den ∈ [-∞, +∞] 1 |den| > 0.1 0 goc d 0 d [-0.09, 0.09] 0 d ∈ [-∞, +∞] 1 |d| ≥ 0.1 0 x2 Dx 0 Dx 0 0 Dx ∈ [-∞, +∞] 1 |Dx| > 0 0 xcor usemax 0 usemax [1, 10] 1 usemax ≥ 0 1 usemax > 0 0 Fig.

Experiments on ASTR ÉE

We have also evaluated the scalability of AVO when analyzing large realistic programs, by integrating it into the ASTR ÉE analyzer [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF] and analyzing its dedicated benchmarks: a set of large embedded industrial C codes performing much integer and float computation. ASTR ÉE contains many abstract domains, including octagons and disjunctive domains (such as trace partitioning and decision diagrams) and domains specialized for the analyzed benchmarks; It is carefully tuned to give few alarms and remain efficient. Hence, we did not expect the AVO domain to bring a notable increase in precision (by simply replacing octagons with AVO, a single program featured a reduction of 4 alarms). For a more fair comparison, we evaluated how AVO could replace, by its natural ability to represent disjunctions, the dedicated disjunctive domains in ASTR ÉE. We disabled these disjunctive domains and ran analyses with the regular octagon domain and with AVO. Following the experiments from Fig. 9, we chose to use the more scalable weak closure WeakCloVia1Sign for these large analyses. The results are shown in Fig. 11. The last columns give the number of alarms removed by using AVO and the increase in analysis time. We observe three instances of alarm reductions and an increase of up to +130% of analysis time at worst. Additionally, the majority of codes are composed of a single large synchronous loop running 10 6 iterations, and we provide for those the number of abstract iterations needed to reach a fixpoint. Our experiments show that using the more precise AVO domain can slightly increase the convergence rate and never decrease it. Overall, our results show that, although it cannot compete with domains specifically tailored to analyze a code family, AVO nevertheless brings modest improvements in precision, and keeps the analysis time in the same order of magnitude.

subdomains (including octagons [START_REF] Miné | The octagon abstract domain[END_REF], two variables per inequality (TVPI) [START_REF] Simon | Two Variables per Linear Inequality as an Abstract Domain[END_REF], template polyhedra [START_REF] Sankaranarayanan | Scalable analysis of linear systems using mathematical programming[END_REF], subpolyhedra [START_REF] Laviron | Subpolyhedra: A (more) scalable approach to infer linear inequalities[END_REF], etc.) Until now, only a few numerical abstract domains natively allow representing nonconvex sets, e.g., congruences [START_REF] Granger | Static analysis of arithmetical congruences[END_REF], max-plus polyhedra [START_REF] Allamigeon | Inferring min and max invariants using maxplus polyhedra[END_REF], interval linear abstract domains [START_REF] Chen | Interval polyhedra: An abstract domain to infer interval linear relationships[END_REF][START_REF] Chen | An abstract domain to discover interval linear equalities[END_REF] and quadratic templates [START_REF] Adjé | Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis[END_REF]. To enhance numerical abstract domain with non-convex expressiveness, some work makes use of BDDs [START_REF] Gurfinkel | Boxes: A symbolic abstract domain of boxes[END_REF][START_REF] Howe | Quadtrees as an abstract domain[END_REF] while some makes use of mathematical functions that could express non-convex properties such as max [START_REF] Gulavani | A numerical abstract domain based on expression abstraction and max operator with application in timing analysis[END_REF] and the absolute value function [START_REF] Chen | Linear absolute value relation analysis[END_REF]. The donut domain [START_REF] Ghorbal | Donut domains: Efficient non-convex domains for abstract interpretation[END_REF] utilizes the set difference of two convex sets to express non-convex properties. Recently, [START_REF] Gange | Abstract interpretation over non-lattice abstract domains[END_REF] studies the impact of using non-lattice abstract domains (including non-convex numerical abstract domains) and proposes general remedies for precision and termination.

The AVO domain that we introduce in this paper is closest to the abstract domain of linear AV inequalities [START_REF] Chen | Linear absolute value relation analysis[END_REF] which can infer general linear AV constraints but is of exponential complexity. The AVO domain enjoys abstract operators in cubic time complexity and quadratic memory complexity. Moreover, the AVO domain supports strict inequalities. [START_REF] Péron | An abstract domain extending difference-bound matrices with disequality constraints[END_REF] presents an abstract domain extending DBMs (encoding potential constraints) with disequality constraints of the form "x y" or "x 0", rather than extending the octagon domain. Moreover, disequalities are different from strict inequalities in that a disequality is a disjunction of two strict inequalities, while in this paper we consider the conjunction of strict inequalities. The pentagon domain [START_REF] Logozzo | Pentagons: A weakly relational abstract domain for the efficient validation of array accesses[END_REF] also chooses on purpose to perform the closure in an incomplete (but sound) way, to improve the efficiency in practice at the cost of precision. Our purpose to have weak closure in this paper is similar, but to low down the complexity due to absolute value.

Conclusion

In this paper, we present an analysis to discover octagonal (or UTVPI) relations among the values and the absolute values of variables of a program (±X ± Y ≤ c, ±X ± |Y| ≤ d, ±|X| ± |Y| ≤ e) , which generalizes the octagon abstract domain (±X ± Y ≤ c) [START_REF] Miné | The octagon abstract domain[END_REF]. The analysis explores the absolute value function as a mean to describe non-convex behaviors in the program. First, we present a representation to encode AV octagons via DBMs. Then we propose 3 closure algorithms for AV octagons to offer different time precision tradeoffs. On this basis, we provide algorithms for domain operations such that the new domain still enjoys the cubic time complexity, as octagons. In addition, we present an approach to extend AVO to support strict inequalities over rational or realvalued variables, which also fits for octagons. Experimental results are encouraging on benchmark programs and large embedded C programs: AVO is scalable and able to find useful non-convex invariants, without too much overhead compared with octagons.

It remains for future work to consider the domain of AV integer octagonal constraints (i.e., AV octagonal constraints with integers as constant terms), wherein the key is to have a tight closure algorithm for AV integer octagonal constraints.

Fig. 2 .

 2 Fig. 2. The geometric shape of AV octagonal constraints. (a) depicts an octagon with constraint set C = {x ≤ 4, -x ≤ 4, y ≤ 4, -y ≤ 4, x + y ≤ 7, xy ≤ 7, -x + y ≤ 7, -xy ≤ 7}; (b) depicts -|x| ≤ -1; (c) depicts -|x| + y ≤ 2; (d) depicts -|x|y ≤ 2; (e) depicts -|x| -|y| ≤ -4; (f) depicts an AV octagon with constraint set C ′ = C ∪ {-|x| ≤ -1, -|y| ≤ -1, -|x| + y ≤ 2, -|x|y ≤ 2, x -|y| ≤ 2, -x -|y| ≤ 2, -|x| -|y| ≤ -4}.

yFig. 3 .

 3 Fig. 3. A piecewise linear function with nested AV functions.

Fig. 4 .

 4 Fig. 4. DBMs for AV octagons. (a) shows a constraint set for a planar AV octagon; (b) shows a DBM to encode the constraints.

12 return M; } Fig. 5 .

 12}5 Fig.5. The weak closure algorithm by enumerating the signs of 3 variables in each step. M/{V k , V i , V j } denotes the sub-matrix of M consisting of the rows and columns corresponding to variables in {V k , V i , V j }.

14 for i ← 1 to 4n 15 ifFig. 7 .

 14157 Fig. 7. The weak closure algorithm by enumerating the sign of one variable in each step.

Fig. 9 .

 9 Fig. 9. An experimental comparison of 3 closure algorithms on randomly generated DBMs.

  [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF]. Experimental results on NECLA division-by-zero benchmarks. Fig. 11. Experimental results using ASTR ÉE on large embedded C codes.

	code id	size (KLOC)	octagons time (s) ♯alarm ♯iter. time (s) ♯alarm ♯iter. AV octagons	result comparison ♯ alarm time ♯ iter. reduction increase reduction
	P1	154	6216 881 110 7687 881 110	0	23.66%	0
	P2	186	6460 1114 116 7854 1114 115	0	21.58%	1
	P3	103	1112 403 25 2123 403 25	0	90.92%	0
	P4	493	17195 4912 158 38180 4912 158	0	122.04%	0
	P5	661	18949 7075 105 43660 7070 104	5	130.41%	1
	P6	616	34639 8192 118 70541 8180 108	12	103.65%	10
	P7	2428 99853 10980 317 217506 10959 317	21	117.83%	0
	P8	3	517	0	19	581	0	19	0	12.38%	0
	P9	18	534	16	27	670	16	27	0	25.47%	0
	P10	26	1065 102 42 1133 102 42	0	6.38%	0

http://www.flaterco.com/xtide/

Related workIn abstract interpretation, most existing numerical abstract domains can only express convex sets, such as the classical convex polyhedra domain[START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF] together with all its

⋆ This work is supported by the 973 Program under Grant No. 2014CB340703, the NSFC under Grant Nos. 61120106006, 61202120, 91118007, the NSF under Grant No. CCF-1248069 and an international fellowship by the Chinese Academy of Sciences.


Antoine Miné
email: mine@di.ens.fr

AstréeA: A Static Analyzer for Large Embedded Multi-Task Software

Embedded critical systems, such as planes and cars, cannot be easily fixed during missions and any error can have catastrophic consequences. It is thus primordial to ensure the correctness of their controlling software before they are deployed. At the very least, critical embedded software must be exempt from runtime errors, including ill-defined operations according to the specification of the language (such as arithmetic or memory overflows) as well as failure of programmer-inserted assertions. Sound and approximate static analysis can help, by providing tools able to analyze the large codes found in the industry in a fully automated way and without missing any real error. Sound and scalable static analyzers are sometimes thought to be too imprecise and report too many false alarms to be of any use in the context of verification. This claim was disproved when, a decade ago [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF], the Astrée static analyzer [START_REF] Blanchet | The Astrée static analyzer[END_REF] successfully analyzed the runtime errors in several Airbus control flight software, with few or no false alarm. This result could be achieved by employing abstract interpretation [START_REF] Cousot | Abstract interpretation frameworks[END_REF], a principled framework to define and compose modular sound-by-construction and parametric abstractions, but also by adopting a design-by-refinement development strategy. Starting from an efficient and easy to design, but rather coarse, fully flow-and context-sensitive interval analyzer, we integrated more complex abstractions (carefully chosen from the literature, such as octagons [START_REF] Miné | The octagon abstract domain[END_REF], adapted from it, such as trace partitioning [START_REF] Mauborgne | Trace partitioning in abstract interpretation based static analyzer[END_REF], or specifically invented for our needs, such as digital filter domains [START_REF] Feret | Static analysis of digital filters[END_REF]) to remove large sets of related false alarms, until we reached our precision target.

In this presentation, we discuss our on-going efforts towards a similar goal: the efficient and precise sound verification of the absence of run-time errors, but targeting another, more complex class of software: shared-memory concurrent embedded C software. Such software are already present in critical systems and will likely become the norm with the generalization of multi-core processors in embedded systems, leading to new challenging demands in verification. Our analyzer is named AstréeA [START_REF] Cousot | The AstréeA static analyzer[END_REF], in reference to Astrée on which it takes its inspiration and on the code base of which it elaborates. AstréeA's specialization target is a family of several embedded avionic codes, each featuring a small fixed set of a dozen threads, more than 1.5 Mlines of C code, implicit communication through the shared memory, and running under a real-time OS based on the ARINC 653 specification.

One major challenge is that a concurrent program execution does not follow a fixed sequential order, but one of many interleavings of executions from different tasks chosen by the scheduler. A sound analysis must consider all possible interleavings in order to cover every corner case and race condition. As it is impractical to build a fully flow-sensitive analysis by enumerating explicitly all interleavings, we took inspiration from thread-modular methods: we analyze each thread individually, in an environment consisting of (an abstraction of) the effect of the other threads. This is a form of rely-guarantee reasoning [START_REF] Jones | Tentative steps toward a development method for interfering programs[END_REF], but in a fully automatic static analysis settings formalized as abstract interpretation. Contrary to Jones' seminal rely-guarantee proof method or its more recent incarnations [START_REF] Flanagan | Thread-modular verification for sharedmemory programs[END_REF], our method does not require manual annotations: thread interferences are automatically inferred by the analysis (including which variables are actually shared and their possible values). Following the classic methodology of abstract interpretation [START_REF] Cousot | Abstract interpretation frameworks[END_REF][START_REF] Cousot | Invariance proof methods and analysis techniques for parallel programs[END_REF], a thread-modular static analysis is now viewed as a computable abstraction of a complete concrete thread-modular semantics. This permits a fine control between precision and efficiency, and opens the way to analysis specialization: any given safety property of a given program can be theoretically inferred given the right abstract domain.

Following the design-by-refinement principle of Astrée, our first prototype AstréeA [START_REF] Miné | Static analysis of run-time errors in embedded critical parallel C programs[END_REF] used a very coarse but efficient flow-insensitive and non-relational notion of thread interference: it gathered independently for each variable and each thread an interval abstraction of the values the thread can store into the variable along its execution, and injected these values as non-deterministic writes into other threads. This abstraction allowed us to scale up to our target applications, in efficiency (a few tens of hours of computation) if not in precision (a few tens of thousands alarms). This presentation will describe our subsequent work in improving the precision of AstréeA by specialization on our target applications, and the interesting abstractions we developed along the way. For instance, we developed new interference abstractions enabling a limited but controllable (for efficiency) degree of relationality and flow-sensitivity [START_REF] Miné | Relational thread-modular static value analysis by abstract interpretation[END_REF]. We also designed abstractions able to exploit our knowledge of the real-time scheduler used in the analysis target: i.e., it schedules tasks on a single core and obeys a strict priority scheme. 1 The resulting analysis is less general, but more precise on our target applications, which was deemed necessary as the correctness of the applications relies on these hypotheses on the scheduler. 2 Finally, not all false alarms are caused by our abstraction of concurrency; we also developed numeric and memory domains to handle more precisely some programming patterns which we did not encounter in our previous experience with Astrée and for which no stock abstract domain was available.

The end-result is a more precise analyzer on our target applications, with currently around a thousand alarms. We stress that AstréeA is a work in progress and that its results, although they are not yet as impressive as those of Astrée, are likely to improve through further specialization. We also believe that, thanks to the intrinsic modularity of the abstract interpretation framework, the analysis performed by AstréeA can be adapted to other settings (other families of applications, other schedulers, other concurrency models) by developing new abstractions, while the abstractions we designed along the journey may also be of use in similar or different static analyses.

The scheduler remains fully preemptive: a low-priority thread may be interrupted at any point by a higher-priority thread whose request to an external resource has just been granted, resulting in a large number of possible thread interleavings.

It is important not to confuse here specialization with restriction: the scheduler abstraction is optional and can be omitted to achieve a more general, but less specialized analysis.


Jean-Christophe Dubois
email: jean-christophe.dubois@univ-rennes1.fr

Yolande Le Gall
email: yolande.le-gall@univ-rennes1.fr

Arnaud Martin
email: arnaud.martin@univ-rennes1.fr

Designing a belief function-based accessibility indicator to improve web browsing for disabled people

The purpose of this study is to provide an accessibility measure of webpages, in order to draw disabled users to the pages that have been designed to be accessible to them. Our approach is based on the theory of belief functions, using data which are supplied by reports produced by automatic web content assessors that test the validity of criteria defined by the WCAG 2.0 guidelines proposed by the World Wide Web Consortium (W3C) organization. These tools detect errors with gradual degrees of certainty and their results do not always converge. For these reasons, to fuse information coming from the reports, we choose to use an information fusion framework which can take into account the uncertainty and imprecision of information as well as divergences between sources. Our accessibility indicator covers four categories of deficiencies. To validate the theoretical approach in this context, we propose an evaluation completed on a corpus of 100 most visited French news websites, and 2 evaluation tools. The results obtained illustrate the interest of our accessibility indicator.

Introduction

The Web constitutes today an essential source of information and communication. While users have a growing interest in terms of social, cultural and economic value, and in spite of legislations and recommendations of the W3C community for making websites more accessible, its accessibility remains hardly efficient for some disabled or ageing users. Actually, making websites accessible and usable by disabled people is a challenge [START_REF]European Disability Strategy 2010-20: A Renewed Commitment to a Barrier-Free Europe[END_REF] that society needs to overcome [START_REF] Abascal | The use of guidelines to automatically verify web accessibility[END_REF].

To measure the accessibility of a webpage, several accessibility metrics have been developed [START_REF] Vigo | Automatic web accessibility metrics: where we are and where we can go[END_REF]. Evaluations are based on the failure to comply with the recommendations of standards, using automatic evaluation tools. They often give a final value, continuous or discrete, to represent content accessibility. However, the fact remains that tests on accessibility criteria are far from being trivial [START_REF] Brajnik | Comparing accessibility evaluation tools: a method for tool effectiveness[END_REF]. Evaluation reports of automatic assessors contain errors considered as certain, but also warnings or potential problems which are uncertain. Moreover there are differences between assessor evaluations, even for errors considered as certain.

This work provides a new measure of accessibility and an information fusion framework to fuse information coming from the reports of automatic assessors allowing search engines to re-rank their results according to an accessibility level, as some users would like [START_REF] Ivory | Search result exploration: a preliminary study of blind and sighted users' decision making and performance[END_REF]. This accessibility indicator considers several categories of deficiencies. Our approach is based on the theory of the belief functions adapted to take into account the defects of accessibility given by several automatic assessors seen as information sources, the uncertainty of their results, as well as the possible conflicts between the sources.

In the sections 2 and 3 we will give a description of accessibility tools based on a recent standard and of data provided in their reports. In the 4 th section, we will describe the principles of our indicator and develop how we implement the belief functions. In the 5 th part, we will present an experiment before concluding.

Defect detection of webpage accessibility

Various accessibility standards propose recommendations for improving accessibility of webpages. The Web Content Accessibility Guidelines (WCAG 2.0) [START_REF] Brajnik | Web Accessibility Testing: When the Method is the Culprit[END_REF] proposed by the W3C normalization organization, constitutes an international reference in the field. These guidelines cover a wide range of disabilities (visual, auditory, physical, speech, cognitive, etc.) and several layers of guidance are provided:

• 4 overall principles: perception, operability, understandability & robustness; • testable success criteria: for each guideline, testable success criteria are provided.

Every criterion is associated to one of the 3 defined conformance levels (A, AA and AAA), each representing a requirement of accessibility for users.

Several automatic accessibility assessors, based on various accessibility standards, have been developed [START_REF] Caldwell | Web Content Accessibility Guidelines (WCAG) 2.0, W3C Recommendation[END_REF] for IT professionals. Their limits depend on the automatic tests. Because it is at present not possible to test some criteria about the quality of some pages, some assessor results are given with ambiguity. Consequently, the existing automatic assessors look for the criteria which are not met and give the defects according to 3 levels of validity: the number of errors, which are estimated certain, the number of likely problems (warnings) whose reality is not guaranteed and the number of potential problems (also called generic or non testable) which leads to a complete uncertainty on the tested criterion accessibility.

Finally, even though the results obtained by different assessors match for some tested common criteria, results can differ, even for errors considered as certain.

Proposed accessibility indicator

After a request, the indicator has to supply information describing to users the accessibility level of each webpage proposed by a search engine. Presented simultaneously with these pages, the indicators' information cover two aspects:

• the accessibility for categories of deficiencies: as previously proposed for accessibility estimation [START_REF] Dempster | Upper and Lower probabilities induced by a multivalued mapping[END_REF] we use 4 major categories: visual, hearing, motor and cognitive deficiencies, as defined by [START_REF] Vanderheiden | Accessible design of consumer products: guidelines for the design of consumer products to increase their accessibility to people with disabilities or who are aging[END_REF]. They are called "deficiency frames"; • the level of accessibility for each deficiency frame.

Collecting results from several assessors has allowed us to benefit from each of their performance. In addition, it strengthens accessibility evaluation for similar results and manages conflicts in case of disagreements. Automatic assessors check a set of criteria which correspond to many deficiencies. As our accessibility evaluation varies for every deficiency frame, our method consists in selecting the relevant criteria for each deficiency frame and then balancing each criterion to consider the difficulties met by users in case of failure. This weighting is based on the criterion conformance level (A, AA, AAA), which corresponds to decreasing priorities (A: most important, etc.). The errors and problems detected for every criterion of the accessibility standard affect the accessibility indicator of the Web content tested according to the deficiency frame the criterion belongs to, its weighting within the frame, the number of occurrences when it is analyzed as a defect in the webpage and the defect's degree of certainty (error, likely or potential problem).

Defect detection and accessibility evaluation

After collecting webpage Uniform Resource Locators (URL p ) selected by a search engine from a request, these addresses are supplied to the accessibility assessors and successively for each page, we detect accessibility defects, then estimate accessibility level by deficiency frame for each assessor, before fusing the data by deficiency frame and taking the decision for every deficiency frame [START_REF] Dubois | Software Engineering System for the Analysis of Accessibility Data[END_REF].

Assessor evaluations of selected pages

Each URL p is submitted to the accessibility evaluation tests by each assessor i that tests all the criteria k of the WCAG 2.0 standard, and the following data are collected by a filter that extracts the required data for each deficiency frame:

• N e k,i : errors observed for a criterion k by an assessor i; • N c k,i : correct checkpoints for a criterion k by an assessor i; • T e k,i : tests that can induce errors for a criterion k by an assessor i; • N l k,i : likely problems detected for a criterion k by an assessor i; • T l k,i : tests that can induce likely problems for a criterion k by an assessor i; • N p k,i : potential problems suspected for a criterion k by an assessor i; • T p k,i : tests that can induce potential problems for a criterion k by an assessor i; • T i : total tests by an assessor i, with:

T i = ∑ k (N e k,i + N l k,i + N p k,i + N c k,i ) (1)

Accessibility indicator level of the pages

To model initial information including uncertainties, the reliability of the assessors seen as information sources and their possible conflicts, we use the theory of belief functions [4] [START_REF] Shafer | A mathematical theory of evidence[END_REF]. Our objective is to define if a webpage is accessible (Ac) or not accessible (Ac) and to supply an indication by deficiency frame. Consequently, these questions can be handled independently for every deficiency frame Ω h = {Ac, Ac}. We can consider every power set 2 Ω h = { / 0, Ac, Ac, Ω }. The estimation of the accessibility Ac for a deficiency frame h and a source i (assessor) is estimated from the number of correct tests for each of the criteria k occurring in this frame, and from their conformance level represented by α k :

E(Ac) h,i = ∑ k (N c k,i * α k ) T i (2)
The estimation of the non accessibility Ac for a deficiency frame h and a source i is estimated from the number of errors for each of the criteria k occurring in this frame, and from the α k coefficient. A weakening β e i coefficient is also introduced to model the degree of certainty of the error:

E(Ac) h,i = ∑ k (N e k,i * α k * β e i ) T e k,i (3)
The estimation of the ignorance Ω h for a deficiency frame h and a source i is estimated from the number of likely and potential problem for each of the criteria k occurring in this frame, and from the α k coefficient. The weakening coefficients β l i or β p i are also used to model the degree of certainty of the problem:

E(Ω h,i = ∑ k (N l k,i * α k * β l i + N p k,i * α k * β p i ) ∑ k (T l k,i + T p k,i ) (4)
The mass functions of the subsets of 2 Ω h are computed from the estimations:

m(Ac) h,i = E(Ac) h,i E(Ac) h,i + E(Ac) h,i + E(Ω ) h,i (5)
m(Ac) h,i = E(Ac) h,i E(Ac) h,i + E(Ac) h,i + E(Ω ) h,i (6)
m(Ω ) h,i = E(Ω ) h,i E(Ac) h,i + E(Ac) h,i + E(Ω ) h,i (7)
In addition, the source reliability can be modeled [START_REF] Martin | General combination rules for qualitative and quantitative beliefs[END_REF] with a δ i coefficient, which constitutes a benefit when some assessors are more efficient than others:

         m δ i (Ac) h,i = δ i * m(Ac) h,i m δ i (Ac) h,i = δ i * m(Ac) h,i m δ i (Ω ) h,i = 1 -δ i * (1 -m(Ω ) h,i ) (8)

Merging assessor results and decision-making

Once the masses for each assessor have been obtained, a fusion of the results is conducted by deficiency frame, using the conjunctive rule [START_REF] Smets | Belief Functions: the Disjunctive Rule of Combination and the Generalized Bayesian Theorem[END_REF], to combine them and give information in the form of a mass function. These rule properties, which strengthen common results and manage conflicts between sources, are particularly relevant in this context, to deal with divergences between assessor evaluations. To calculate the final decision D h (URL p ) for a page by deficiency frame, we use the pignistic probability [START_REF] Smets | Belief Functions: the Disjunctive Rule of Combination and the Generalized Bayesian Theorem[END_REF].

There are several ways of presenting the accessibility indicator to users. To visualize the deficiency frames, existing specific pictograms are effective. To present the accessibility level we discretize the decision into 5 levels (very good, good, moderate, bad or very bad accessibility) using thresholds and visualized it by an "arrow":

• if D h < S 1 , the Web content accessibility is very bad (↓), • if S 1 < D h < S 2 , the Web content accessibility is bad (ց), • if S 2 < D h < S 3 , the Web content accessibility is moderate (→), • if S 3 < D h < S 4 , the Web content accessibility is good (ր), • if S 4 < D h , the Web content accessibility is very good (↑).

Experiments

To validate our approach, we present here the results obtained on a set of 100 news Websites, among the most visited ones, all referenced by the OJD1 organization which provides certification and publication of attendance figures for websites. We test their homepages, following a study [START_REF] Nielsen | Homepage Usability: 50 Websites Deconstructed[END_REF] concluding that their usability is predictive of the whole site. We chose two open source assessors AChecker, (source 1) [START_REF] Gay | AChecker: open, interactive, customizable, web accessibility checking[END_REF], and TAW (source 2) from which we extract automatically the accessibility test results. Weight and threshold values given in Table 1 were previously empirically defined from Webpages2 assumed to be accessible. The results of these sources are summarized in Figure 1 for the 3 levels of certainty defects. The box plots present how their defects are distributed: minimum and maximum (whiskers), 1 st (bottom box plot) and 3 rd quartiles (top box plot) and average (horizontal line). We observe similarities between the assessors' results for the errors detected as certain, but also huge differences for the likely (warnings) and potential (non testable) problems. The number of likely problems is almost null for AChecker and the potential one remains always the same for TAW. is not evenly distributed between the 2 sources: their distributions of errors (Figure 2) are comparable even if there is a larger range for AChecker; however the mass function of accessibility is smaller for AChecker compared to TAW. This is due to the more numerous potential problems (non testable criteria) detected by the AChecker assessor, increasing substantially the denominator in the computation of m(Ac) (Eq. 5). By the way, the values of E(Ω ) and of m(Ω ), are more important, as the β p i weight for potential problems is 2 times higher than β l i for the likely problems (warnings). We can also notice that the fusion result obtained by the conjunctive rule strengthens the mass functions of the 2 assessors. In this corpus, visual and cognitive deficiencies have a higher impact on content accessibility than the motor ones. This is logical for news websites, as their homepages include a large number of images. By the way, the motor indicator is less impacted, in particular by the lack of alternatives for images, useful for visual and cognitive deficiencies. Finally, we observe a similarity between the visual and global indicators, as around 80% of all the checkpoints concern visual deficiencies and also because these controls are properly taken into account by assessors. In Table 2 are presented detailed results for several sites with significant indicator result differences. For examples, LePoint.fr and Arte.tv, respectively 19 th and 33 th most consulted websites in France, obtain only 0.627 and 0.686 for the global result, whereas LeParisien.fr, ranked 12 th , reaches 0.971. For Family.fr we observe differences between the deficiencies, nevertheless focus on accessibility generally benefits all deficiencies on the whole corpus.

Conclusion

We present an indicator estimating webpage accessibility levels for distinct categories of deficiencies, in order to supply easily understandable accessibility information to users on pages proposed by a search engine. Our method based on belief function theory fuses results from several automatic assessors and considers their uncertainties. An accurate modelization of the assessor characteristics and of the impact of defect guideline criteria on accessibility is proposed. An experiment performed on a set of 100 news websites validates the method, which benefits from each of the assessor performances on specific criterion tests. Our future research will focus on the implementation of a user's personal weighting to balance the importance of criteria.

Fig. 1 :

 1 Fig. 1: Results of automatic assessors. The detected defects are taken into account in our accessibility indicator results presented in Figure 2. The mass function values of accessibility m(Ac) for the 2 sources, TAW and AChecker, and the fusion result are visualized for 3 deficiency frames among the 4, and globally for all deficiencies. Firstly, we can see that m(Ac)

Fig. 2 :

 2 Fig. 2: Accessibility indicator results.

Table 1 :

 1 Constant values for our accessibility metric.

	Weightings	α 1 ; α 2 ;α 3 β e i ; β l i ;β p i δ 1 ; δ 2 ;α 3	A, AA, AAA conformance levels Certainty levels of errors or problems AChecker and TAW reliabilities (sources)	1 ; 0.8 ; 0.6 1 ; 0.5 ; 1 1 ; 1
	Thresholds S1 ; S2 ; S3 ; S4	Accessibility indicator levels	0.6 ; 0.7 ; 0.8 ; 0.9

Table 2 :

 2 Examples of detailed accessibility results by deficiency frame.

	Web content (URL p )	Visual	Motor	Decision Cognitive Global
	LeParisien.fr	0.972 ↑	0.989 ↑		0.974 ↑	0.971 ↑
	Famili.fr	0.769 →	0.924 ↑		0.838 ր	0.766 ր
	Arte.tv	0.701 →	0.718 →	0.717 →	0.686 ց
	LePoint.fr	0.630 ց	0.725 →	0.673 ց	0.627 ց

OJD: http://www.ojd.com/Chiffres/Le-Numerique/Sites-Web/Sites-Web-GP

Sites labeled by Accessiweb: http://www.accessiweb.org/index.php/galerie.html


Marc Lasson

❡✿ A : Type, a : A, x 1 : C 1 , y 1

published or not. The documents may come

Canonicity of Weak ω-groupoid Laws Using

Parametricity Theory

✇❤❡r❡ 1 a : a = a ❞❡♥♦t❡s t❤❡ r❡✢❡①✐✈✐t②✳ ❚❤✉s ❢♦r ❛♥② ✐♥t❡❣❡r n✱ ∀X : Type, x : X.Ω n (X, x) ✐s ❛ ❣r♦✉♣♦✐❞ •❛✇ ✐♥❤❛❜✐t❡❞ ❜② λX : Type, x : X.ω n (X, x) ✭♥♦t❡ t❤❛t ✉s✐♥❣ ♦♥❡ ✉♥✐✈❡rs❡✱ ✐t ✐s ♣♦ss✐❜•❡ t♦ ✐♥t❡r♥❛•✐③❡ t❤❡ q✉❛♥t✐✜❝❛t✐♦♥ ♦✈❡r n❀ ❡✈❡r②t❤✐♥❣ t❤❛t ✇❡ st❛t❡ ❤❡r❡ ✇✐•• ❜❡ tr✉❡ ✇❤❡t❤❡r ♦r ♥♦t t❤✐s ✐s ✉s❡❞✮✳ ❲❡ ❝❛•• t❤✐s ❣r♦✉♣♦✐❞ •❛✇ t❤❡ n✲t❤ ♣❛r❛♠❡tr✐❝ •♦♦♣ s♣❛❝❡✳ ❚❤❡ 0✲t❤ ♣❛r❛♠❡tr✐❝ •♦♦♣ s♣❛❝❡✱ ✐s t❤❡ ♣♦•②♠♦r♣❤✐❝ t②♣❡ ∀X : Type.X → X ♦❢ ✐❞❡♥t✐t② ❢✉♥❝t✐♦♥s✱ ❛♥❞ ✐ts ❝❛♥♦♥✐❝❛• ✐♥❤❛❜✐t❛♥t ✐s λX : Type, x : X.x✱ ✐❡✳ t❤❡ ✐❞❡♥t✐t② ❢✉♥❝t✐♦♥✳ ❚❤✐s t❡r♠ ✐s t❤❡ ♦♥•② ♦♥❡ ✉♣ t♦ ❢✉♥❝t✐♦♥ ❡①t❡♥s✐♦♥❛•✐t② ✐♥❤❛❜✐t✐♥❣ ✐ts t②♣❡✳ ❚❤❡ st❛♥❞❛r❞ t♦♦• t♦ ♣r♦✈❡ t❤✐s ❦✐♥❞ ♦❢ ♣r♦♣❡rt✐❡s ✐s ❜② ✉s✐♥❣ |❡②♥♦•❞✬s ♣❛r❛♠❡tr✐❝✐t② t❤❡♦r② ❬✼( ✇❤✐❝❤ ✇❛s ✐♥tr♦❞✉❝❡❞ t♦ st✉❞② t❤❡ ❜❡❤❛✈✐♦r ♦❢ t②♣❡ q✉❛♥✲ t✐✜❝❛t✐♦♥s ✇✐t❤✐♥ ♣♦•②♠♦r♣❤✐❝ λ✲❝❛•❝✉•✉s ✭❛✳❦✳❛✳ ❙②st❡♠ ❋✮✳ ■t r❡❢❡rs t♦ t❤❡ ❝♦♥❝❡♣t t❤❛t ✇❡••✲t②♣❡❞ ♣r♦❣r❛♠s ❝❛♥♥♦t ✐♥s♣❡❝t t②♣❡s❀ t❤❡② ♠✉st ❜❡❤❛✈❡ ✉♥✐❢♦r♠•② ✇✐t❤ r❡s♣❡❝t t♦ ❛❜str❛❝t t②♣❡s✳ |❡②♥♦•❞s ❢♦r♠❛•✐③❡s t❤✐s ♥♦t✐♦♥ ❜② s❤♦✇✐♥❣ t❤❛t ♣♦•②✲ ♠♦r♣❤✐❝ ♣r♦❣r❛♠s s❛t✐s❢② t❤❡ s♦✲❝❛

••❡❞ •♦❣✐❝❛• r❡•❛t✐♦♥s ❞❡✜♥❡❞ ❜② ✐♥❞✉❝t✐♦♥ ♦♥ t❤❡ str✉❝t✉r❡ ♦❢ t②♣❡s✳ ❚❤✐s t♦♦• ❤❛s ❜❡❡♥ ❡①t❡♥❞❡❞ ❜② ❇❡r♥❛r❞② ❡t ❛•✳ ❬✷( t♦ ❞❡♣❡♥✲ ❞❡♥t t②♣❡ s②st❡♠s✳ ■t ♣r♦✈✐❞❡s ❛ ✉♥✐❢♦r♠ tr❛♥s•❛t✐♦♥ ♦❢ t❡r♠s✱ t②♣❡s ❛♥❞ ❝♦♥t❡①ts ♣r❡s❡r✈✐♥❣ t②♣✐♥❣ ✭t❤❡ s♦✲❝❛••❡❞ ❛❜str❛❝t✐♦♥ t❤❡♦r❡♠✮✳ ■♥ ✐ts ✉♥❛r② ✈❡rs✐♦♥ ✭t❤❡ ♦♥•② ♥❡❡❞❡❞ ❢♦r t❤✐s ✇♦r❦✮✱ •♦❣✐❝❛• r❡•❛t✐♦♥s ❛r❡ ❞❡✜♥❡❞ ❜② ❛ss♦❝✐❛t✐♥❣ t♦ ❛♥② ✇❡••✲❢♦r♠❡❞ t②♣❡ A : Type ❛ ♣r❡❞✐❝❛t❡ A : A → Type ❛♥❞ t♦ ❛♥② ✐♥❤❛❜✐t❛♥t M : A ❛ ✇✐t
♥ t♦ ♣r♦✈❡ t❤❡ ❝❛♥♦♥✐❝✐t② r❡s✉•t ❢♦r •♦♦♣ s♣❛❝❡s❀ ✇❡ ♣r♦✈❡ t❤❛t ❛•• ✐♥❤❛❜✐t❛♥ts ♦❢ ♣❛r❛♠❡tr✐❝ •♦♦♣ s♣❛❝❡s ❛r❡ ♣r♦♣♦s✐t✐♦♥❛••② ❡q✉❛• ✭❚❤❡♦r❡♠ ✷✮✳ ■♥ ❙❡❝t✐♦♥ ✺✱ ✇❡ ✐♥tr♦❞✉❝❡ t❤❡ ❢r❛❣♠❡♥t ▼▲■❉ ♦❢ t②♣❡ t❤❡♦r② t♦ ❞❡✜♥❡ ♦✉r ♥♦t✐♦♥ ♦❢ ❣r♦✉♣♦✐❞ •❛✇s ❛♥❞ ✇❡ s❤♦✇ t❤❛t t❤❡ r❡s✉•t ♦❢ ❙❡❝t✐♦♥ ✹ ♠❛② ❜❡ ❣❡♥❡r❛•✐③❡❞ t♦ ❛•• ❣r♦✉♣♦✐❞ •❛✇s ✭❚❤❡♦r❡♠ ✹✮✳ ❋✐♥❛••② ❙❡❝t✐♦♥ ✻ ✐s ❞❡✈♦t❡❞ t♦ ✈❛r✐♦✉s ❞✐s❝✉ss✐♦♥s✳ ✷ Pr❡s❡♥t❛t✐♦♥ ♦❢ t❤❡ s②♥t❛① ❲❡ ❣✐✈❡ ❛ ♣r❡s❡♥t❛t✐♦♥ ♦❢ ▼❛rt✐♥✲▲ö❢ t②♣❡ t❤❡♦r② ✇✐t❤ ✐❞❡♥t✐t② t②♣❡s ❛♥❞ ✉♥✐✈❡rs❡s ✇❤✐❝❤ ✐s ❝•♦s❡ t♦ t❤❡ s②♥t❛① ♦❢ ♣✉r❡ t②♣❡ s②st❡♠s ❬✶( ✐♥ ♦r❞❡r t♦ r❡✉s❡ t❤❡ ♣❛r❛✲ ♠❡tr✐❝✐t② t❤❡♦r② ♣r❡s❡♥t❡❞ ✐♥ ❬✷(✳ ■♥ t❤✐s ❢r❛♠❡✇♦r❦✱ ❝♦♠♣✉t❛t✐♦♥ r✉•❡s ❛r❡ tr❡❛t❡❞ ✐♥ ❛♥ ✉♥t②♣❡❞ ✇❛② ❛♥❞ s✉❜t②♣✐♥❣ ♦❢ ✉♥✐✈❡rs❡s ✐s ❛❝❤✐❡✈❡❞ ✉s✐♥❣ ▲✉♦✬s ❝✉♠✉•❛t✐✈✐t② r❡•❛t✐♦♥ ✐♥tr♦❞✉❝❡❞ ❢♦r t❤❡ ❡①t❡♥❞❡❞ ❝❛•❝✉•✉s ♦❢ ❝♦♥str✉❝t✐♦♥s ❬✻(✳ ❚❤❡ r❡❛❞❡r ♠❛② ❜❡ ♠♦r❡ ✉s❡❞ t♦ •✉❞❣❡♠❡♥t❛• ♣r❡s❡♥t❛t✐♦♥s ♦❢ t②♣❡ t❤❡♦r② ✇❤❡r❡ ❡❛❝❤ ❝♦♠♣✉t❛t✐♦♥ st❡♣s ❛r❡ ❝❤❡❝❦❡❞ t♦ ❜❡ ✇❡••✲t②♣❡❞✳ ❚❤✐s ✐s •✉st ❛ ♠❛tt❡r ♦❢ ♣r❡s❡♥t❛t✐♦♥❀ ❛•• t❤❡ ♠❛t❡r✐❛• ♣r❡s❡♥t❡❞ ❤❡r❡ ❝♦✉•❞ ❜❡ ❛❞❛♣t❡❞ ✇✐t❤♦✉t ♠✉❝❤ ❡✛♦rt t♦ s✉✐t t②♣❡ s②st❡♠s ✉s✐♥❣ ❛ •✉❞❣❡♠❡♥t❛• ❡q✉❛•✐t②✳ ❆•s♦✱ t❤❡ ✉s❡ ♦❢ ❝✉♠✉•❛t✐✈✐t② ✐s ♥♦t r❡❛••② ♥❡❡❞❡❞ ❜✉t ♠❛❦❡s ♦✉r r❡s✉•ts ♠♦r❡ ❣❡♥❡r❛• ❛♥❞ ❝•♦s❡r t♦ ✐♠♣•❡♠❡♥t❛t✐♦♥s s✉❝❤ ❛s ❝♦q✳ ❚❤❡ t❡r♠s ♦❢ t❤❡ s②st❡♠ ❛r❡ ❣✐✈❡♥ ❜② t❤❡ ❢♦••♦✇✐♥❣ ❣r❛♠♠❛r✿ A, B, C, M, N, U, V := x | (M N ) | λx : A.M | ∀x : A.B | Type i | M = A N | 1 C M | J ∀x:C,y:M =x.A (B, U, V ) ✇❤❡r❡ ✉♥✐✈❡rs❡s Type i ❛r❡ ✐♥❞❡①❡❞ ❜② i ∈ N✳ ❱❛r✐❛❜•❡s ❛r❡ ❝♦♥s✐❞❡r❡❞ ✉♣ t♦ α✲ ❝♦♥✈❡rs✐♦♥ ❛♥❞ ✇❡ ✇r✐t❡ M [N/x] t♦ ❞❡♥♦t❡ t❤❡ t❡r♠ ♦❜t❛✐♥❡❞ ❜② s✉❜st✐t✉t✐♥❣ ❛•• ❢r❡❡ ♦❝❝✉rr❡♥❝❡s ♦❢ x ✐♥ M ❜② N ✳ ❚♦ ❡❛s❡ t❤❡ r❡❛❞✐♥❣ ♦❢ t❡r♠s✱ ✇❡ ❛••♦✇ ♦✉rs❡•✈❡s t♦ ♦♠✐t s♦♠❡ t②♣✐♥❣ ❛♥♥♦t❛t✐♦♥s ✇❤❡♥ t❤❡② ❝♦✉•❞ ❜❡ ❣✉❡ss❡❞ ❢r♦♠ t❤❡ ❝♦♥t❡①t ✭✐♥ ♣❛rt✐❝✉•❛r M = N ✱ 1 M ❛♥❞ J(B, U, V ) ✇✐•• ❜❡ ✉s❡❞ ♦❢t❡♥ ✐♥ t❤✐s t❡①t✮✳ ❚❤❡ ❣r❛♠♠❛r ♦❢ t❡r♠s ✐s ♦❜t❛✐♥❡❞ ❜② ❛❞❞✐♥❣ t♦ t❤❡ s②♥t❛① ♦❢ ♣✉r❡ t②♣❡ s②st❡♠s✿ • ❚❤❡ t②♣❡ ❝♦♥str✉❝t♦r M = A N ❢♦r ❢♦r♠✐♥❣ ✐❞❡♥t✐t② t②♣❡s✱ • ❚❤❡ ✐♥tr♦❞✉❝t✐♦♥ r✉•❡ ❢♦r ✐❞❡♥t✐t② t②♣❡s✱ 1 C M ✱ t♦ ✇✐t♥❡ss t❤❡ r❡✢❡①✐✈✐t② M = C M ✱ ✸ • ❚❤❡ ❡•✐♠✐♥❛t✐♦♥ r✉•❡ ✭❛•s♦ ❦♥♦✇♥ ❛s ✏♣❛t❤✲✐♥❞✉❝t✐♦♥✑✮ J ∀x:C,y:M =x.A (B, U, V )✳ •✐✈❡♥ ❛♥② ❞❡♣❡♥❞❡♥t t②♣❡ A(x, y) ✇❤✐❝❤ ❞❡♣❡♥❞s ♦♥ ❛ ♣♦✐♥t x ❛♥❞ ❛ ♣❛t❤ y ❢r♦♠ ❛ ❜❛s❡ ♣♦✐♥t M t♦ x✱ ❣✐✈❡♥ ❛ ✇✐t♥❡ss ❢♦r A(M, 1 M ) ✭t❤❡ ❜❛s❡ ❝❛s❡ ♦❢ t❤❡ ✐♥❞✉❝t✐♦♥✮✱ ❣✐✈❡♥ ❛ ♣♦✐♥t U ❛♥❞ ❛ ♣❛t❤ V ✱ t❤❡ ♣❛t❤✲✐♥❞✉❝t✐♦♥ ♣r♦✈✐❞❡s ❛♥ ✐♥✲ ❤❛❜✐t❛♥t ♦❢ A(U, V )✳ ❚❤✐s ❢♦r♠✉•❛t✐♦♥ ♦❢ ♣❛t❤✲✐♥❞✉❝t✐♦♥✱ ❞✉❡ t♦ P❛✉•✐♥✲▼ö❤r✐♥❣ ✭❛•s♦ ❝❛••❡❞ ❜❛s❡❞ ♣❛t❤ ✐♥❞✉❝t✐♦♥✮✱ ✐s ❡q✉✐✈❛•❡♥t t♦ t❤❡ ♦t❤❡r ✈❡rs✐♦♥ ✇❤❡r❡ A ✐s ♣❛r❛♠❡tr✐③❡❞ ❜② t✇♦ ♣♦✐♥ts ❛♥❞ ❛ ♣❛t❤ ❜❡t✇❡❡♥ t❤❡♠✳ ❲❡ ✉s❡ t❤❡ s②♠❜♦• ≡ t♦ ❞❡♥♦t❡ t❤❡ s②♥t❛❝t✐❝ ❡q✉❛•✐t② ✭✉♣ t♦ α✲❝♦♥✈❡rs✐♦♥✮ ❜❡t✇❡❡♥ t❡r♠s✳ ❚❤❡ ❝♦♥✈❡rs✐♦♥ ❜❡t✇❡❡♥ t❡r♠s ✇✐•• ❜❡ ❞❡♥♦t❡❞ ❜② M ≡ β N ✱ ✐t ✐s ❞❡✲ ✜♥❡❞ ❛s t❤❡ s♠❛••❡st ❝♦♥❣r✉❡♥❝❡ ❝♦♥t❛✐♥✐♥❣ t❤❡ ✉s✉❛• β✲r❡❞✉❝t✐♦♥ (λx : A.M ) N ≡ β M [N/x] ❛♥❞ t❤❡ ❝♦♠♣✉t❛t✐♦♥ r✉•❡ ❢♦r ✐❞❡♥t✐t② t②♣❡s✿ J ∀x:c,y:M =x,∆.P (N, M, 1 C M ) ≡ β N ✳ ❆♥❞ t❤❡ ❝✉♠✉•❛t✐✈✐t② ♦r❞❡r ✐s ❞❡✜♥❡❞ ❛s t❤❡ s♠❛••❡st ♣❛rt✐❛• ♦r❞❡r ❝♦♠♣❛t✐❜•❡ ✇✐t❤ ≡ β ❛♥❞ s❛t✐s❢②✐♥❣ ❢♦r i ≤ j✿ ∀x 1 : A 1 , ..., x n : A n .Type i ∀x 1 : A 1 , ..., x n : A n .Type j ▲✐❦❡ ✐♥ t❤❡ ❡①t❡♥❞❡❞ ❝❛•❝✉•✉s ♦❢ ❝♦♥str✉❝t✐♦♥s✱ t❤❡ ❝✉♠✉•❛t✐✈✐t② r✉•❡ ✐s ♥♦t ❢✉••② ❝♦♥tr❛✈❛r✐❛♥t ✇✐t❤ r❡s♣❡❝t t♦ t❤❡ ❞♦♠❛✐♥ ♦❢ ❢✉♥❝t✐♦♥s ✭A ′ A ❛♥❞ B B ′ ❞♦❡s ♥♦t ✐♠♣•② ∀x : A.B ∀x : A ′ .B ′ ✮ ♦t❤❡r✇✐s❡ ✐t ✇♦✉•❞ ❜r❡❛❦ t❤❡ ❞❡❝✐❞❛❜✐•✐t② ♦❢ t②♣❡ ❝❤❡❝❦✐♥❣✳ ❈♦♥t❡①ts ❛r❡ ✜♥✐t❡ •✐sts ♦❢ t❤❡ ❢♦r♠ x 1 : A 1 , • • • , x n : A n ♠❛♣♣✐♥❣ ❛ ✈❛r✐❛❜•❡ t♦ ✐ts t②♣❡✳ ❚❤❡ r✉•❡s ♦❢ t❤❡ t②♣❡ s②st❡♠ ❛r❡ ❣✐✈❡♥ ✐♥ ❋✐❣✉r❡ ✶✳ ❆s ✇❡ ❢♦••♦✇ st❛♥❞❛r❞ •✐♥❡s✱ ✇❡ ❞♦ ♥♦t ❞❡✈❡•♦♣ ✐♥ ❞❡t❛✐•s t❤❡ ♠❡t❛t❤❡♦r② ♦❢ t❤❡ s②st❡♠✳ ❚❤❡ ♥♦♥✲❞❡♣❡♥❞❡♥t ✈❡rs✐♦♥ ♦❢ ♣❛t❤✲✐♥❞✉❝t✐♦♥ ✐s ❝❛••❡❞ tr❛♥s♣♦rt ❛♥❞ ✐s ❞❡✜♥❡❞ ❜② P * x:C.X (M ) ≡ J ∀x:C,y:U =x.X (M, V, P ) Γ ⊢ U : C Γ ⊢ V : M = U Γ ⊢ J ∀x:C,y:M =x.P (B, U, V ) : P [U/x, V /y] ♣❛t❤✲✐♥❞✉❝t✐♦♥ ❋✐❣✳ ✶✳ ❚②♣❡ t❤❡♦r② ✇✐t❤ ✐❞❡♥t✐t② t②♣❡s ✭▼▲❚❚✮✳ ♦r❡♠ ✶✮✳ ∀x : A.B ≡ λf : ∀x : A.B.∀x : A, x R : x ∈ A .(f x) ∈ B Type i ≡ λx : Type i .x → Type i λx : A.M ≡ λx : A, x R : x ∈ A . M M N ≡ M N N x ≡ x R ✇❤❡r❡ M ∈ A s✐♠♣•② st❛♥❞s ❛s ❛ ♥♦t❛t✐♦♥ ❢♦r A M ✭✐t ♠❛❦❡s ❢♦r♠✉•❛s ❛ ❜✐t ❡❛s✐❡r t♦ r❡❛❞✮✳ ❆s s❛✐❞ ✐♥ t❤❡ ✐♥tr♦❞✉❝t✐♦♥✱ t❤❡ ♣r❡❞✐❝❛t❡ ❣❡♥❡r❛t❡❞ ❜② ❛♥ ✐❞❡♥t✐t② t②♣❡ M = C N ✐s ❞❡✜♥❡❞ ❜② t❤❡ t②♣❡ ❢❛♠✐•② ♦✈❡r M = C N s❡•❡❝t✐♥❣ ♣❛t❤s tr❛♥s♣♦rt✐♥❣ M t♦ N ✿ M = C N : M = C N → Type M = C N ≡ λp : M = C N.p * x:C.x∈ C ( M ) = C N N ❚❤❛♥❦s t♦ t❤❡ ❝♦♠♣✉t❛t✐♦♥❛• r✉•❡ 1 C M ∈ M = C M ≡ β 1 C M * x:c.x∈ C ( M ) = M ∈ C M ≡ β M = M ∈ C M t❤❡ tr❛♥s•❛t✐♦♥ 1 C M : 1 C M ∈ M = C M ♦❢ r❡✢❡①✐✈✐t② ✐s ❛ r❡✢❡①✐✈✐t②✿ 1 C M ≡ 1 M ∈ C M ✳ ❆♥❞ ✜♥❛••②✱ t❤❡ ❡•✐♠✐♥❛t✐♦♥ r✉•❡ ✐s tr❛♥s•❛t❡❞ ✐♥ t❡r♠s ♦❢ ♥❡st❡❞ ♣❛t❤✲ ✺ ✐♥❞✉❝t✐♦♥s✿ J ∀x:C,y:M =x.P (B, U, V ) ≡ J ∀x R :U ∈ C ,y R :V * ( M )=x R .J ∀x:C,y:M =x.P (B,U,V )∈ P [U/x,V /y] (J ∀x:C,y:M =x.J ∀x:C,y:M =x.P (B,x,y)∈ P [y * ( M )/x R ,1 y * ( M ) /y R ] ( B , U, V ), U , V ) ❚❤❡ tr❛♥s•❛t✐♦♥ ♦❢ t❤❡ ♣r❡❞✐❝❛t❡ ♦❢ ♣❛t❤ ✐♥❞✉❝t✐♦♥s ❛r❡ q✉✐t❡ ✈❡r❜♦s❡ ❛♥❞ ♠❛❦❡ t❤❡ tr❛♥s•❛t✐♦♥ ❤❛r❞ t♦ r❡❛❞✳ ❍♦✇❡✈❡r ✐❢ ✇❡ ✐❣♥♦r❡ t❤❡ ❛♥♥♦t❛t✐♦♥✱ ✇❡ s❡❡ t❤❛t t❤❡ tr❛♥s•❛t✐♦♥ J(B, U, V ) ≡ J(J( B , U, V ), U , V ) ✐s s✐♠♣•② ❛ ❞✉♣•✐❝❛t✐♦♥ ♦❢ ♣❛t❤ ✐♥❞✉❝t✐♦♥ ✇❤✐❝❤ s❤♦✉•❞ ❜❡ ❝♦♠♣❛r❡❞ t♦ t❤❡ ❞✉♣•✐❝❛t✐♦♥ ✐♥ ❛❜str❛❝t✐♦♥s ❛♥❞ ❛♣♣•✐❝❛✲ t✐♦♥s✳ ❲❡ ❝❛♥ ❝❤❡❝❦ t❤❛t t❤✐s tr❛♥s•❛t✐♦♥ ❜❡❤❛✈❡s ✇❡•• ✇✐t❤ r❡s♣❡❝t t♦ s✉❜st✐t✉t✐♦♥ ❛♥❞ ❝♦♥✈❡rs✐♦♥ ✿ ▲❡♠♠❛ ✶ ✭❙✉❜st✐t✉t✐♦♥ ❛♥❞ ❝♦♥✈❡rs✐♦♥ •❡♠♠❛✮✳ ❲❡ ❤❛✈❡ ✿ ✭✐✮ M [N/x] ≡ M [N/x, N /x R ]✱ ✭✐✐✮ ■❢ M ≡ β M ′ ✱ t❤❡♥ M ≡ β M ′ ✳ ✭✐✐✐✮ ■❢ M M ′ ✱ t❤❡♥ M M ′ ✳ Pr♦♦❢✳ ❚❤❡ ♣r♦♦❢ ♦❢ ✭✐✮ ✐s ❛ r♦✉t✐♥❡ ♣r♦♦❢ ❜② ✐♥❞✉❝t✐♦♥ ♦♥ M ✳ ❆♥❞ ✭✐✐✐✮ ✐s ❛ r❛t❤❡r ❞✐r❡❝t ❝♦♥s❡q✉❡♥❝❡ ♦❢ ✭✐✐✮✳ ❚♦ ♣r♦✈❡ ✭✐✐✮✱ ✇❡ ♦♥•② ❞♦ ❤❡r❡ t❤❡ ♦♥•② ❝❤❡❝❦ t❤❛t ✐s ♥♦t ✐♥ ❇❡r♥❛r❞②✬s tr❛♥s•❛t✐♦♥ ✿ J(N, M, 1 C M ) ≡ J(J( N , M, 1 C M ), M , 1 C M ) ≡ J(J( N , M, 1 C M ), M , 1 M ∈ C M ) ≡ β J( N , M , 1 M ∈ C M ) ≡ β N ◆♦✇ ✇❡ ❝❛♥ ❝❤❡❝❦ t❤❛t t❤✐s ❡①t❡♥s✐♦♥ ♣r❡s❡r✈❡ t②♣✐♥❣ ✿ ❚❤❡♦r❡♠ ✶ ✭❆❜str❛❝t✐♦♥✮✳ ■❢ Γ ⊢ M : A✱ t❤❡♥ Γ ⊢ M : A (a) Γ ⊢ M : M ∈ A (b) ♠♦r❡♦✈❡r ✐❢ Γ wf t❤❡♥ Γ wf ✭❝✮✳ Pr♦♦❢✳ ❚❤❡ ❛❜str❛❝t✐♦♥ t❤❡♦r❡♠ ✐s ♣r♦✈❡❞ ❜② ✐♥❞✉❝t✐♦♥ ♦♥ ❞❡r✐✈❛t✐♦♥s✳ ■♥ ❡❛❝❤ ❝❛s❡s✱ ♣r♦✈✐♥❣ t❤❡ st❛t❡♠❡♥t ✭❛✮ ✐s str❛✐❣❤t❢♦r✇❛r❞✳ ❙✐♥❝❡ t❤❡ tr❡❛t♠❡♥t ♦❢ ♦t❤❡r r✉•❡s ✐s ♥♦✇ st❛♥❞❛r❞✱ ✇❡ ♦♥•② ❞❡❛• ❤❡r❡ ✇✐t❤ t❤❡ r✉•❡s ❝♦♥❝❡r♥✐♥❣ ✐❞❡♥t✐t② t②♣❡s✳ ❊✈❡♥ t❤♦✉❣❤ ✇❡ ❞♦ ♥♦t ❞❡t❛✐•❡❞ ✐t ❤❡r❡✱ t❤❡ tr❡❛t♠❡♥t ♦❢ ❝♦♥✈❡rs✐♦♥ ✉s❡s ♣r❡✈✐♦✉s •❡♠♠❛✳ • ✐❞❡♥t✐t②✿ ❚❤❡ ✐♥❞✉❝t✐♦♥ ❤②♣♦t❤❡s✐s ❣✐✈❡s ✉s Γ ⊢ M : M ∈ C ✭✶✮✱ Γ ⊢ N : N ∈ C ✭✷✮ ❛♥❞ Γ , x : C ⊢ x ∈ C : Type i ✭✸✮✳ ❯s✐♥❣ tr❛♥s♣♦rt ✇❡ ❞❡r✐✈❡ ❢r♦♠ ✭✶✮ ❛♥❞ ✭✸✮✱ t❤❛t Γ , p : M = C N ⊢ p * λx:C.x∈C ( M ) : N ∈ C ✳ ❚❤❡♥✱ ✉s✐♥❣ ✐❞❡♥t✐t② ❛♥❞ ✭✷✮ ✇❡ ❜✉✐•❞ ❛ ❞❡r✐✈❛t✐♦♥ ❢♦r Γ , p : M = C N ⊢ ✻ p * λx:C.x∈C ( M ) = N ∈ C N ❛♥❞ ✜♥❛••② ✇❡ ❝♦♥❝•✉❞❡ Γ ⊢ M = C N : M = C N → Type i ✇✐t❤ ❛❜str❛❝t✐♦♥✳ • r❡❢•❡①✐✈✐t②✿ ❇② ✐♥❞✉❝t✐♦♥ ❤②♣♦t❤❡s✐s✱ ✇❡ ❤❛✈❡ Γ ⊢ M : M ∈ C ✭✶✮✳ ❯s✐♥❣ ✭✶✮ ✇❡ ❝❛♥ ❝❤❡❝❦ t❤❛t Γ ⊢ 1 M ∈ C M : M = M ∈ C M ✇❤✐❝❤ ✐s ❝♦♥✈❡rt✐❜•❡ t♦ Γ ⊢ 1 M ∈ C M : 1 C ✇❤✐❝❤ ♠❡❛♥s✱ ✉s✐♥❣ ♣❛t❤✲✐♥❞✉❝t✐♦♥✱ ❝❤❡❝❦✐♥❣ ✿ • ❚❤❡ ♣r❡❞✐❝❛t❡ ✐s ✇❡••✲❢♦r♠❡❞ ✿ Γ , x : C, y : M = x ⊢ J(B, x, y) ∈ P [y * ( M )/x R , 1 y * ( M ) /y R ] : Type ❚❤✐s ✐s ♦❜t❛✐♥❡❞ ❜② s✉❜st✐t✉t✐♥❣ x R ❛♥❞ y R ✐♥ ✭✷✮ ✉s✐♥❣ ❛ ❞❡r✐✈❛t✐♦♥ ♦❢ Γ , x : C, y : M = x ⊢ y * ( M ) : x ∈ C ❛♥❞ ♦❢ Γ , x : C, y : M = x ⊢ 1 y * ( M ) : y * ( M ) = y * ( M ) ✇❤✐❝❤ ❛r❡ ❡❛s✐•② ❞❡r✐✈❡❞ ❢r♦♠ ✭✶✮ ❛♥❞ ❜② ❛♣♣•②✐♥❣ Γ , x : C, y : M = x ⊢ J(B, x, y) : P t♦ t❤❡ s✉❜st✐t✉t❡❞ ❞❡r✐✈❛t✐♦♥✳ • ❚❤❡ ❛r❣✉♠❡♥ts ❛r❡ ❝♦rr❡❝t ✿ ❲❡ ❞❡r✐✈❡ Γ ⊢ B : J(B, M, 1 M ) ∈ P [y * ( M )/x R , 1 y * ( M ) /y R , M/x, 1 M /y] ❜② ♥♦t✐❝✐♥❣ ✉s✐♥❣ ❝♦♠♣✉t❛t✐♦♥ r✉•❡s t❤❛t ✿ J(B, M, 1 M ) ∈ P [y * ( M )/x R , 1 y * ( M ) /y R , M/x, 1 M /y] ≡ β B ∈ P [M/x, M /x R , 1 M /y, 1 y * ( M ) /y R ] ✼ ❛♥❞ t❤❡r❡❢♦r❡ ❝♦♥✈❡rs✐♦♥ ❛♥❞ ✭✸✮ ❛••♦✇ ✉s t♦ ❝♦♥❝•✉❞❡✳ ❋✐♥❛••②✱ ✇❡ ❤❛✈❡ t♦ ❝❤❡❝❦ t❤❛t t❛r❣❡t ♣♦✐♥t ❛♥❞ ♣❛t❤ ❛r❡ ❝♦rr❡❝t ✐❡✳ Γ ⊢ U : C ❛♥❞ Γ ⊢ V : M = U ✇❤✐❝❤ ❛r❡ ❣✐✈❡♥ ❜② ✭✾✮ ❛♥❞ ✭✶✵✮✳ ▲❡t K ❜❡ t❤❡ ❢♦••♦✇✐♥❣ t❡r♠✿ J ∀x R :U ∈ C ,y R :V * ( M )=x R .J ∀x:C,y:M =x.P (B,U,V )∈ P [U/x,V /y] (T, U , V ) ❲❡ ♥♦✇ ✇❛♥t t♦ ❝❤❡❝❦ t❤❛t ✿ Γ ⊢ K : J ∀x:C,y:M =x.P (B, U, V ) ∈ P [U/x, V /y] ✉s✐♥❣ ♣❛t❤✲✐♥❞✉❝t✐♦♥✱ ✇❡ ❤❛✈❡ t♦ s❤♦✇ t❤❛t ✿ • ❚❤❡ ♣r❡❞✐❝❛t❡ ✐s ✇❡••✲❢♦r♠❡❞ ✿ Γ , x R : U ∈ C , y R : V * ( M ) = x R ⊢ J ∀x:C,y:M =x.P (B, U, V ) ∈ P [U/x, V /y] : Type i ✇❤✐❝❤ ✐s ♦❜t❛✐♥❡❞ ❜② s✉❜st✐t✉t✐♥❣ x ❛♥❞ y ✐♥ ✭✷✮ ✉s✐♥❣ ✭✾✮ ❛♥❞ ✭✶✵✮ ❛♥❞ ❜② ❛♣✲ ♣•②✐♥❣ Γ ⊢ J ∀x:C,y:M =x.P (B, U, V ) : P [U/x, V /y] t♦ t❤❡ s✉❜st✐t✉t❡❞ ❞❡r✐✈❛t✐♦♥✳ • ❚❤❡ ❛r❣✉♠❡♥ts ❛r❡ ❝♦rr❡❝t ✿ ❲❡ ✉s❡ ✭✯✮ ❢♦r t②♣❡ ❝❤❡❝❦✐♥❣ ❚ ❛♥❞ ✇❡ ✉s❡ ✭✹✮ ❛♥❞ ✭✺✮ ❢♦r t②♣❡ ❝❤❡❝❦✐♥❣ U ❛♥❞ V ✳ ✹ ❈❛♥♦♥✐❝✐t② ✐♥ ♣❛r❛♠❡tr✐❝ •♦♦♣ s♣❛❝❡s ❚❤❡ ❣♦❛• ♦❢ t❤✐s s❡❝t✐♦♥ ✐s t♦ ♣r♦✈❡ ❚❤❡♦r❡♠ ✷✳ ❚❤❡ ❢♦••♦✇✐♥❣ •❡♠♠❛ ✐s ♥❡❡❞❡❞ t♦ ♣❡r❢♦r♠ t❤❡ ♠❛✐♥ ✐♥❞✉❝t✐♦♥ ✐♥ ▲❡♠♠❛ ✸✳ ❚❤❡ ♣r♦♦❢s t❡r♠s ❛r❡ ❞❡s❝r✐❜❡❞ ✐♥ ❛ s❡♠✐✲❢♦r♠❛• st②•❡ ❢♦r r❡❛❞✐♥❣ ♣✉r♣♦s❡✱ t❤❡② ❝♦✉•❞ ❜❡ ❡❛s✐•② ❝♦♥str✉❝t❡❞ ❢r♦♠ t❤❡ ♣r♦s❡✳ ❍♦✇❡✈❡r✱ ❛s ❛ ❝♦♥s❡q✉❡♥❝❡ ♦❢ ❚❤❡r❡♦♠ ✷✱ t❤❡ ♣r❡❝✐s❡ s❤❛♣❡ ♦❢ t❤❡s❡ t❡r♠s ✐s ♥♦t ✐♠♣♦rt❛♥t✳ ■♥ t❤✐s s❡❝t✐♦♥✱ ✇❡ ✉s❡ p q ❛♥❞ p -1 t♦ ❞❡♥♦t❡ r❡s♣❡❝t✐✈❡•② t❤❡ ❝♦♥❝❛t❡♥❛t✐♦♥ ♦❢ ♣❛t❤s ❛♥❞ t❤❡ ✐♥✈❡rs❡✳ ▲❡♠♠❛ ✷✳ ▲❡t P : A → Type ❜❡ ❛ t②♣❡ ❢❛♠✐•② ❛♥❞ u : P a ❢♦r s♦♠❡ a : A ❛♥❞ ❛ss✉♠❡ ✇❡ ❤❛✈❡ φ : ∀x : A.P x → a = x✳ ❚❤❡♥✱ ❢♦r ❛•• p : a = a s✉❝❤ t❤❛t p * (u) = u✱ ✇❡ ❤❛✈❡ 1 = p✳ Pr♦♦❢✳ ❇② ❛♣♣•②✐♥❣ t❤❡ ❢✉♥❝t♦r✐❛• ❛❝t✐♦♥ ♦❢ ♣❛t❤ ♦♥ p * (u) = u ✉s✐♥❣ φ a ✇❡ ♦❜t❛✐♥ ❛ t✇♦ ❞✐♠❡♥s✐♦♥❛• ♣❛t❤ φ a (p * (u)) = φ a (u) ❛♥❞ ❜② t❤❡ ♥❛t✉r❛•✐t② ♦❢ tr❛♥s♣♦rt ✭▲❡♠♠❛ ✷✳✸✳✶✶ ✐♥ ❬✽(✮✱ ✇❡ ♦❜t❛✐♥ ❛ ♣❛t❤ p * (φ a (u)) = φ a (u)✳ ❚❤❡ •❡❢t✲❤❛♥❞ s✐❞❡ ♣❛t❤ p * (φ a (u)) ✐s tr❛♥s♣♦rt ♦✈❡r ❛♥ ✐❞❡♥t✐t② t②♣❡✱ ✇❡ t❤❡r❡❢♦r❡ ❤❛✈❡ p * (φ a (u)) = φ a (u) p ❛♥❞ t❤❡r❡❢♦r❡ φ a (u) p = φ a (u)✳ ❙♦✱ ✇❡ ❝♦♥❝•✉❞❡ 1 = p ❜② ❝❛♥❝❡••✐♥❣ ❜② φ a (u) ❛♥❞ ❜② s②♠♠❡tr②✳ ❍❡r❡ ✐s t❤❡ ♠❛✐♥ ✐♥❞✉❝t✐♦♥ ✇❤✐❝❤ ❛••♦✇s ✉s t♦ ❞❡r✐✈❡ ❚❤❡♦r❡♠ ✷✿ ▲❡♠♠❛ ✸✳ ▲❡t A✱ P ✱ a✱ u ❛♥❞ φ ❞❡✜♥❡❞ ❛s ✐♥ ♣r❡✈✐♦✉s •❡♠♠❛✳ ❚❤❡♥ ❢♦r ❛•• n✲ ❞✐♠❡♥s✐♦♥❛• •♦♦♣ p : Ω n (A, a)✱ t❤❡ t②♣❡ ❢❛♠✐•② Ω n (A, P, a, u) : Ω n (A, a) → Type s❛t✐s✜❡s ✿ ∀p : Ω n (A, a). Ω n (A, P, a, u) p → ω n (A, a) = p✳ Pr♦♦❢✳ ❇② ✐♥❞✉❝t✐♦♥ ♦♥ n✱ t❤❡ ❜❛s❡ ❝❛s❡ ✐s ❡①❛❝t•② ✇✐t♥❡ss ❜② φ✳ ❋♦r t❤❡ ✐♥❞✉❝t✐✈❡ st❡♣✱ ✇❡ ♥❡❡❞ t♦ ♣r♦✈❡ ∀p : Ω n+1 (A, a).p ∈ Ω n+1 (A, P, a, u) → ω n+1 (A, a) = p ✽ ✇❤✐❝❤ ✐s ❝♦♥✈❡rt✐❜•❡ t♦ ✿ ∀p : Ω n (a = a, 1).p ∈ Ω n (a = a, λq : a = a.q * (u) = u, 1, 1) → ω n (a = a, 1) = p ❲❡ ♠❛② t❤❡r❡❢♦r❡ ❛♣♣•② t❤❡ ✐♥❞✉❝t✐♦♥ ❤②♣♦t❤❡s✐s ❜② ♣r♦✈✐❞✐♥❣ ❛ ♣r♦♦❢ t❤❛t ∀q : a = a.q * (u) = u → 1 = q ✇❤✐❝❤ ✐s ❣✐✈❡♥ ❜② ♣r❡✈✐♦✉s •❡♠♠❛✳ ❲❡ ❝❛♥ ❞❡❞✉❝❡ ✿ ❚❤❡♦r❡♠ ✷ ✭❈❛♥♦♥✐❝✐t② ❢♦r •♦♦♣ s♣❛❝❡s✮✳ ■❢ ⊢ M : ∀A : Type, a : A.Ω n (A, a) t❤❡♥ t❤❡r❡ ✐s ❛ t❡r♠ π s✉❝❤ t❤❛t ⊢ π : ∀A : Type, a : A.ω n (A, a) = M A a✳ Pr♦♦❢✳ ❚❤❡ ❛❜str❛❝t✐♦♥ t❤❡♦r❡♠ ❣✐✈❡s ✉s ❛ ♣r♦♦❢ M t❤❛t ∀A : Type, A R : A → Type, a : A, a R : A R a.(M A a) ∈ Ω n (A, A R , a, a r ) ❜② ✐♥st❛♥t✐❛t✐♥❣ A R ✇✐t❤ λx : A.a = x ✇❡ ❝❛♥ ❝♦♥❝•✉❞❡ ❜② ❛♣♣•②✐♥❣ ♣r❡✈✐♦✉s •❡♠♠❛✳ ◆♦t❡ t❤❛t ❛s ❛ ❝♦r♦••❛r②✱ t❤❡ ♣r♦♦❢ π ✐s ✉♥✐q✉❡ ✉♣ t♦ ♣r♦♣♦s✐t✐♦♥❛• ❡q✉❛•✐t② ✭❛♥❞ s♦ ♦♥✮✳ ■❢ ✇❡ ❤❛✈❡ t✇♦ s✉❝❤ ♣r♦♦❢s π ❛♥❞ π ′ t❤❡♥ (π A a) (π ′ A a) -1 ✐s ♦❢ t②♣❡ ω n (A, a) = ω n (A, a) ✇❤✐❝❤ ✐s Ω n+1 (A, a)✳ ❚❤❡r❡❢♦r❡✱ ❜② ❛♣♣•②✐♥❣ t❤❡ ♣r❡✈✐♦✉s t❤❡♦r❡♠ ✇❡ ♦❜t❛✐♥ ❛ ♣r♦♦❢ ♦❢ (π A a) (π ′ A a) -1 = ω n+1 (A, a) ✇❤✐❝❤ ✐s ❛•s♦ (π A a) (π ′ A a) -1 = 1 ωn(A,a) ✳ ❚❤❡r❡❢♦r❡ ✇❡ ❝♦♥❝•✉❞❡ (π A a) = (π ′ A a)✳ ✺ •r♦✉♣♦✐❞ •❛✇s ■♥ t❤✐s s❡❝t✐♦♥✱ ✇❡ st❛rt ❜② ❞❡s❝r✐❜✐♥❣ ❛ ❢r❛❣♠❡♥t ▼▲■❉ ♦❢ t❤❡ ♣r❡✈✐♦✉s t②♣❡ s②s✲ t❡♠ ▼▲❚❚✳ ❚❤✐s s✉❜✲s②st❡♠ ✐s ✉s❡❞ t♦ ❝❤❛r❛❝t❡r✐s❡ ❣r♦✉♣♦✐❞ •❛✇s✳ ■♥❢♦r♠❛••②✱ ✐t ✐s ♦❜t❛✐♥❡❞ ❢r♦♠ ▼▲❚❚ ❜② r❡♠♦✈✐♥❣ t❤❡ r✉•❡s ❛❜str❛❝t✐♦♥✱ ❛♣♣•✐❝❛t✐♦♥ ❛♥❞ ✉♥✐✲ ✈❡rs❡s ❛♥❞ ❜② r❡str✐❝t✐♥❣ ✈❛•✐❞ s❡q✉❡♥ts t♦ t❤❡ ❝♦♥tr❛❝t✐❜•❡ ❝♦♥t❡①ts ❞❡✜♥❡❞ ✐♥ t❤❡ ✐♥tr♦❞✉❝t✐♦♥✳ ■♥ t❤❡ ❛❜s❡♥❝❡ ♦❢ ❢✉♥❝t✐♦♥ s♣❛❝❡s✱ t❤❡ r✉•❡ ♣❛t❤✲✐♥❞✉❝t✐♦♥ ❤❛s t♦ ❜❡ str❡♥❣t❤❡♥❡❞ ✐♥ ♦r❞❡r t♦ ❜❡ ❛❜•❡ t♦ ♠❛❦❡ ❛ ♣❛t❤ ✐♥❞✉❝t✐♦♥ ❛•♦♥❣ ❛ ♣❛t❤ ✇❤✐❝❤ ✐s ♥♦t t❤❡ •❛st ♦♥❡ ♦❢ t❤❡ ❝♦♥t❡①t✳ ❚❤❡r❡❢♦r❡✱ ✇❡ ♥❡❡❞ t♦ ❡①t❡♥❞ t❤❡ ❣r❛♠♠❛r ♦❢ t❡r♠s ✐♥ ▼▲■❉ ✇✐t❤ t❡r♠s ♦❢ t❤❡ s❤❛♣❡ J ∀x:C,y:M =x,∆.P (B, U, V, -→ W ) ✇❤❡r❡ ∆ ✐s ❛ ❝♦♥t❡①t ❛♥❞ ✇❤❡r❡ t❤❡ ✈❡❝t♦r✐❛• ♥♦t❛t✐♦♥ -→ W ❞❡♥♦t❡s ❛ t✉♣•❡ (W 1 , ..., W n ) ♦❢ t❡r♠s✳ ❚❤❡ t②♣✐♥❣ r✉•❡s ❛r❡ ❣✐✈❡♥ ✐♥ ❋✐❣✉r❡ ✷✳ ❋♦r♠❛••② ❛ ❝♦♥t❡①t Γ ✐s s❛✐❞ t♦ ❜❡ ❝♦♥✲ tr❛❝t✐❜•❡ ✐❢ Γ contr ✐s ❞❡r✐✈❛❜•❡❀ t❤❡ r❡❛❞❡r s❤♦✉•❞ ♥♦t✐❝❡ t❤❛t ❛•• ❝♦♥t❡①ts ♦❝❝✉rr✐♥❣ ✐♥ ❞❡r✐✈❛t✐♦♥s ♦❢ ▼▲■❉ ❛r❡ ❝♦♥tr❛❝t✐❜•❡✳ ■♥ t❤❡ t②♣✐♥❣ r✉•❡s✱ ✇❡ ✇r✐t❡ Γ ⊢ -→ W : ∆ t♦ ❞❡♥♦t❡ t❤❡ ❝♦♥•✉♥❝t✐♦♥ ❢♦r k = 1, • • • , n ♦❢ Γ ⊢ W k [A 1 /y 1 , • • • , A k-1 /y k-1 ] : A k ✇❤❡♥ ∆ ✐s ♦❢ t❤❡ s❤❛♣❡ y 1 : A 1 , • • • , y n : A n ✳ ▼♦r❡♦✈❡r✱ [ -→ W /∆] ❞❡♥♦t❡s t❤❡ ✐t❡r❛t❡❞ s✉❜st✐t✉t✐♦♥ [W 1 /y 1 , • • • , W n [A 1 /y 1 , • • • , A n-1 /y n-1 ]/y n ]✳ ■♥ ♦r❞❡r t♦ ❡♠❜❡❞ ▼▲■❉ ✐♥t♦ ▼▲❚❚✱ ✇❡ tr❛♥s•❛t❡ ❡①t❡♥❞❡❞ ♣❛t❤ ✐♥❞✉❝t✐♦♥s ✐♥t♦ ♥♦r♠❛• ♦♥❡s ❛❝❝♦r❞✐♥❣ t♦ t❤❡ ❢♦••♦✇✐♥❣ tr❛♥s•❛t✐♦♥ ✿ J ∀x:C,y:M =x,∆.P (B, U, V, -→ W ) ≡ λ - → x : ∆.(J ∀x:C,y:M =x.∀∆.P (λx : ∆[M/x, 1 C M /y].B, U, V ) - → x ) ✇❤❡r❡ - → y : ∆ ♠❡❛♥s t❤❛t y 1 , • • • , y n ❛r❡ t❤❡ ✈❛r✐❛❜•❡s ❛ss✐❣♥❡❞ ✐♥ ∆✱ ❛♥❞ ✇❤❡r❡ ∀∆✱ λ∆✱ ❛♥❞ (J - → x ) ❞❡♥♦t❡ r❡s♣❡❝t✐✈❡•② ✐t❡r❛t❡❞ ♣r♦❞✉❝ts✱ ❛❜str❛❝t✐♦♥s ❛♥❞ ❛♣♣•✐✲ ✾ A : Type 0 , x : A contr ✐♥✐t Γ contr Γ ⊢ id B : Type 0 Γ ⊢ id M : B Γ, x : B, p : M = B x contr ❝♦♥tr Γ ⊢ id M : C Γ ⊢ id N : C Γ ⊢ id C : Type 0 Γ ⊢ id M = C N : Type 0 ✐❞❡♥t✐t② Γ ⊢ id M : C Γ ⊢ id 1 C M : M = C M r❡❢•❡①✐✈✐t② Γ contr (x : A) ∈ Γ Γ ⊢ id x : A ✈❛r✐❛❜•❡ Γ ⊢ id M : A ′ Γ ⊢ id A ′ : Type 0 A ′ ≡ β A Γ ⊢ id M : A ❝♦♥✈❡rs✐♦♥ Γ ⊢ id M : C Γ, x : C, y : M = x, ∆ ⊢ id P : Type 0 Γ, ∆[M/x, 1 C M /y] ⊢ id B : P [M/x, 1 C M /y] Γ ⊢ id U : C Γ ⊢ id V : M = U Γ ⊢ id -→ W : ∆ Γ ⊢ id J ∀x:C,y:M =x,∆.P (B, U, V, -→ W ) : P [U/x, V /y, -→ W /∆] ❡①t❡♥❞❡❞✲♣❛t❤✲✐♥❞✉❝t✐♦♥ ❋✐❣✳ ✷✳ ❚❤❡ ♠✐♥✐♠❛• ❢r❛❣♠❡♥t ▼▲■❉ ♦❢ t②♣❡ t❤❡♦r② ✇✐t❤ ✐❞❡♥t✐t② t②♣❡s✳ ❝❛t✐♦♥s✳ ■t ✐s t❤❡♥ str❛✐❣❤t❢♦r✇❛r❞ t♦ ❝❤❡❝❦ t❤❛t ❡①t❡♥❞❡❞✲♣❛t❤✲✐♥❞✉❝t✐♦♥ ✐s ❛♥ ❛❞♠✐ss✐❜•❡ r✉•❡ ♦❢ ▼▲❚❚✳ •r♦✉♣♦✐❞ •❛✇s ❛r❡ ❝❤❛r❛❝t❡r✐③❡❞ ❜② ❛ ❝♦♥tr❛❝t✐❜•❡ ❝♦♥t❡①t ❛♥❞ ❛ ❞❡r✐✈❛❜•❡ t②♣❡ ✐♥ ▼▲■❉ ✭❋✐❣✉r❡ ✸ ❝♦♥t❛✐♥s s♦♠❡ ❡①❛♠♣•❡s ♦❢ ❣r♦✉♣♦✐❞ •❛✇s✮✿ ❉❡✜♥✐t✐♦♥ ✭•r♦✉♣♦✐❞ •❛✇✮✳ ❆ ❣r♦✉♣♦✐❞ •❛✇ ✐s ❛ t❡r♠ ♦❢ t❤❡ s❤❛♣❡ ∀Γ.C s✉❝❤ t❤❛t Γ ⊢ id C : Type 0 ✳ ❚❤❡ ♦♥•② ❣r♦✉♣♦✐❞ •❛✇s ✐♥ t❤❡ ✏✐♥✐t✐❛•✑ ❝♦♥tr❛❝t✐❜•❡ ❝♦♥t❡①t A : Type, a : A ❛r❡ •♦♦♣ s♣❛❝❡s✳ ❙✐♥❝❡ ✇❡ ❞♦ ♥♦t ❝❤❛♥❣❡ t❤❡ ❜❛s❡ t②♣❡ ❛♥❞ t❤❡ ❜❛s❡ ♣♦✐♥t ♦❢ •♦♦♣ s♣❛❝❡s ✐♥ t❤✐s s❡❝t✐♦♥ ✇❡ s✐♠♣•② ❞❡♥♦t❡ ❜② ω n ✭r❡s♣✳ Ω n ✮ t❤❡ t❡r♠s ω n (A, a) ✭r❡s♣✳ Ω n (A, a)✮✳ ❯s✐♥❣ t❤❡s❡ ♥♦t❛t✐♦♥s ✇❡ ❤❛✈❡ ✿ ▲❡♠♠❛ ✹✳ ■❢ A : Type, a : A ⊢ id T : Type 0 ✱ t❤❡♥ ✭✐✮ t❤❡r❡ ❡①✐sts |T | ∈ N s✉❝❤ t❤❛t T ≡ β Ω |T | ✱ ✭✐✐✮ ♠♦r❡♦✈❡r✱ ✐❢ A : Type, a : A ⊢ id W : T t❤❡♥ W ≡ β ω |T | ✳ Pr♦♦❢✳ ❲❡ ♣r♦❝❡❡❞ ❜② ✐♥❞✉❝t✐♦♥ ♦♥ t❤❡ ❞❡r✐✈❛t✐♦♥ ♦❢ A : Type, a : A ⊢ id T : Type 0 ✳ ❲❡ ♥♦t✐❝❡ t❤❛t t❤❡ ♦♥•② t✇♦ ♣♦ss✐❜•❡ •❛st ✉s❡❞ r✉•❡s ❛r❡ ✐❞❡♥t✐t② ❛♥❞ ✈❛r✐❛❜•❡ s✐♥❝❡ Type 0 ❞♦❡s ♥♦t ✐♥❤❛❜✐t Type 0 ✐t ✐s ♥♦t ♣♦ss✐❜•❡ t♦ ✐♥✈♦❦❡ ❡①t❡♥❞❡❞✲♣❛t❤✲ ✐♥❞✉❝t✐♦♥ ♥♦r ❝♦♥✈❡rs✐♦♥✳ ✭✐✮ ■♥ t❤❡ ✈❛r✐❛❜•❡ ❝❛s❡✱ ✇❡ ♥❡❝❡ss❛r✐•② ❤❛✈❡ T ≡ A ❛♥❞ t❤❡r❡❢♦r❡ ✇❡ ❝❛♥ ❝♦♥❝•✉❞❡ ❜② t❛❦✐♥❣ |T | = 0✳ ■♥ t❤❡ ✐❞❡♥t✐t② ❝❛s❡✱ T ✐s ♦❢ t❤❡ s❤❛♣❡ M = C N ❛♥❞ ❜② ✐♥❞✉❝t✐♦♥ ❤②♣♦t❤❡s✐s M ≡ β ω |C| ✱ N ≡ β ω |C| ❛♥❞ C ≡ β Ω |C| ✳ ❙♦ ✇❡ ❝♦♥❝•✉❞❡ ❜② t❛❦✐♥❣ |T | = |C| + 1✳ ✭✐✐✮ ❲✐t❤♦✉t •♦ss ♦❢ ❣❡♥❡r❛•✐t② ✭▼▲❚❚ ✐s ♥♦r♠❛•✐③✐♥❣✮ ✇❡ ❝❛♥ ❛ss✉♠❡ t❤❛t W ✐s ✐♥ ♥♦r♠❛• ❢♦r♠✳ ❲❡ ♣r♦❝❡❡❞ ❜② ❛ ✭♥❡st❡❞✮ ✐♥❞✉❝t✐♦♥ ♦♥ t❤❡ ❞❡r✐✈❛t✐♦♥ A :
✶✵ refl : ∀X : Type, x : X.x = x sym : ∀X : Type, x : X.x = y → y = x concat : ∀X : Type, x : X, y : X.x = y → ∀z : X.y = z → x = z assoc : ∀X : Type, x : X, y : X, p : x = y, z : X, q : y = z, t : X, r : z = t.

concat X x z (concat X x y p z q) t r = concat X x y p t (concat X y z q t r)

neutral : ∀X : Type, x : X, y : X, p : x = y.(concat X x y p y (refl X y)) = p idem : ∀X : Type, x : X, y : X, p : x = y.sym X y x (sym X x y p) = p horizontal : ∀X : Type, x : X, y : X, p : x = y, p ′ : x = y.p = p ′ → ∀z : X, q : x = z, q ′ : x = z.q = q ′ → concat X x y p z q = concat X x y p ′ z q

′ ❋✐❣✳ ✸✳ ❊①❛♠♣•❡s ♦❢ ❣r♦✉♣♦✐❞ •❛✇s ✇✐t❤ ❛•✐❛s❡s ❢♦r ❝❛♥♦♥✐❝❛• ✐♥❤❛❜✐t❛♥ts Type, a : A ⊢ id W : T ✱ ✇❡ tr❡❛t ❡❛❝❤ ♣♦ss✐❜•❡ ❝❛s❡ ✭✐❞❡♥t✐t② ❛♥❞ ❝♦♥✈❡rs✐♦♥ ❛r❡ ♦❜✈✐♦✉s•② ✐♠♣♦ss✐❜•❡ s✐♥❝❡ T ❝❛♥♥♦t ❜❡ Type 0 ✮✿ • ✈❛r✐❛❜•❡✿ ■♥ t❤✐s ❝❛s❡✱ ✇❡ ♥❡❝❡ss❛r✐•② ❤❛✈❡ W ≡ a ❛♥❞ T ≡ A✳ ❙♦ ✇❡ ❤❛✈❡ |T | = 0 ❛♥❞ W ≡ ω 0 ✳ • r❡❢•❡①✐✈✐t②✿ ■♥ t❤✐s ❝❛s❡✱ W ❛♥❞ T ❛r❡ r❡s♣❡❝t✐✈❡•② ♦❢ t❤❡ s❤❛♣❡ 1 C M ❛♥❞ M = C M ✳ ❇② ✐♥❞✉❝t✐♦♥ ❤②♣♦t❤❡s✐s✱ ✇❡ ❤❛✈❡ M ≡ β ω |C| ✳ ❚❤❡r❡❢♦r❡ |T | = |C| + 1 ❛♥❞ W ≡ β ω |C|+1 ✳ • ❡①t❡♥❞❡❞✲♣❛t❤✲✐♥❞✉❝t✐♦♥✿ ❚❤✐s ✐s ✐♥ ❢❛❝t ❛♥ ✐♠♣♦ss✐❜•❡ ❝❛s❡✳ ❲❡ ✇♦✉•❞ ❤❛✈❡ W ♦❢ t❤❡ s❤❛♣❡ J ∀x:C,y:M =x,∆.P (B, U, V, - → Z ) ❛♥❞ ❜② ✐♥❞✉❝t✐♦♥ ❤②♣♦t❤❡s✐s✱ ✇❡ ✇♦✉•❞ ❤❛✈❡ M ≡ β ω |C| ≡ β U ❛♥❞ V ≡ β ω |C|+1 ✳ ❚❤❡r❡❢♦r❡ V ✐s ❛ r❡✢❡①✐✈✐t② ❛♥❞ s♦ W ✐s ♥♦t ✐♥ ♥♦r♠❛• ❢♦r♠✳ ❚❤❡ ♣r❡✈✐♦✉s •❡♠♠❛ ❛••♦✇ ✉s t♦ ✜♥❞ ❛ ❝❛♥♦♥✐❝ ✐♥st❛♥t✐❛t✐♦♥ ♦❢ ❛♥② ❝♦♥tr❛❝t✐❜•❡ ❝♦♥t❡①t ❣✐✈❡♥ ❜② ✿ (A : Type, a : A) + = (A, a) (Γ, x : A, y : M = C x) + = (Γ + , ω |C[Γ + /Γ]| , ω |C[Γ + /Γ]|+1 ) ❚❤❡ ❢♦••♦✇✐♥❣ •❡♠♠❛ st❛t❡ t❤❛t t❤✐s ✐♥st❛♥t✐❛t✐♦♥ ✐s ❝♦rr❡❝t ✿ ▲❡♠♠❛ ✺✳ Γ contr ✐♠♣•✐❡s A : Type 0 , a : A ⊢ id Γ + : Γ ✭✶✮ Γ ⊢ id T : Type 0 ✐♠♣•✐❡s T [Γ + /Γ] ≡ β Ω |T [Γ + /Γ]| ✭✷✮ Γ ⊢ id T : Type 0 ❛♥❞ Γ ⊢ id M : T ✐♠♣•✐❡s M ≡ β ω |T [Γ + /Γ]| ✭✸✮ Pr♦♦❢✳ ❲❡ ♣r♦❝❡❡❞ ❜② ✐♥❞✉❝t✐♦♥ ♦♥ s✐③❡ ♦❢ ❞❡r✐✈❛t✐♦♥s ✐♥ ▼▲■❉✳ ❲❡ ♣r♦✈❡ ✭✶✮ ❜② ✐♥s♣❡❝t✐♥❣ t❤❡ •❛st ♣♦ss✐❜•❡ r✉•❡ ✿ • ✐♥✐t✐❛•✿ Γ ✐s ♦❢ t❤❡ s❤❛♣❡ A : Type 0 , a : A ❛♥❞ Γ + = (A, a)✳ ❇② ✉s✐♥❣ t✇♦ t✐♠❡s ✈❛r✐❛❜•❡✱ ✇❡ ❝❤❡❝❦ t❤❛t ✿ (A : Type 0 , a : A) ⊢ id (A, a) : (A : Type 0 , a : A)✳ • ❝♦♥tr❛❝t✐❜•❡✿ Γ ✐s ♦❢ t❤❡ s❤❛♣❡ ∆, x : B, p : M = B x ✇✐t❤ ∆ ⊢ id B : Type 0 ❛♥❞ Γ ⊢ id M : B✳ ❇② ✐♥❞✉❝t✐♦♥ ❤②♣♦t❤❡s✐s✱ ✇❡ ❤❛✈❡ A : Type 0 , a : A ⊢ id ∆ + : ∆✱ B[∆ + /∆] ≡ β Ω |B[∆ + /∆]| ❛♥❞ M [∆ + /∆] ≡ β ω |B[∆ + /∆]| ✳ ■t ✐s t❤❡♥ ❡❛s② t♦ ❝❤❡❝❦ ✉s✲ ✐♥❣ ❝♦♥✈❡rs✐♦♥ t❤❛t ✇❡ ❤❛✈❡ (A : Type 0 , a : A) ⊢ id (∆ + , ω |C[Γ + /Γ]| , ω |c[Γ + /Γ]|+1 ) : ✶✶ (∆, x : B, p : M = B x)✳ ❚♦ ♣r♦✈❡ ✭✷✮ ❛♥❞ ✭✸✮✱ ✇❡ ♥♦t✐❝❡ t❤❛t ✇✐t❤✐♥ t❤❡ ❞❡r✐✈❛t✐♦♥ ♦❢ Γ ⊢ id T : Type 0 t❤❡r❡ ✐s ❛ str✐❝t•② s♠❛••❡r ❞❡r✐✈❛t✐♦♥ ♦❢ Γ contr s♦ ✇❡ ❝❛♥ ✉s❡ t❤❡ ✐♥❞✉❝t✐♦♥ ❤②♣♦t❤❡s✐s t♦ ♦❜t❛✐♥ A : Type 0 , a : A ⊢ id Γ + : Γ✳ ◆♦✇ ❜② s✉❜st✐t✉t✐♦♥✱ ✇❡ ❞❡r✐✈❡ t❤❛t A : Type 0 , a : A ⊢ id T [Γ + /Γ] : Type 0 ❛♥❞ A : Type 0 , a : A ⊢ id M [Γ + /Γ] : T [Γ + /Γ]✳ ❲❡ ❝♦♥❝•✉❞❡ t❤❛t T [Γ + /Γ] ≡ β Ω |T [Γ + /Γ]| ❛♥❞ M ≡ β ω |T [Γ + /Γ]| ❜② ♣r❡✈✐♦✉s •❡♠♠❛✳ ▲❡♠♠❛ ✻ ✭❆•• ❣r♦✉♣♦✐❞ •❛✇s ❛r❡ ✐♥❤❛❜✐t❡❞✮✳ ■❢ Γ ⊢ id T : Type 0 ✱ t❤❡♥ t❤❡r❡ ❡①✐sts θ Γ.T s✉❝❤ t❤❛t Γ ⊢ id θ Γ.T : T ✳ Pr♦♦❢✳ ❚❤❡ ❝♦♥tr❛❝t✐❜•❡ ❝♦♥t❡①t Γ ✐s ♦❢ t❤❡ s❤❛♣❡ A : Type 0 , a : A, x 1 : C 1 , y 1 : M 1 = x 1 , . . . , x n : C n , y n : M n = x n ✇❡ ❝♦♥str✉❝t θ Γ.c ❜② n s✉❝❝❡ss✐✈❡ ❡①t❡♥❞❡❞ ♣❛t❤✲✐♥❞✉❝t✐♦♥s ✭❢r♦♠ •❡❢t t♦ r✐❣❤t✮✳ ❆❢t❡r ❛•• t❤❡ ✐♥❞✉❝t✐♦♥s✱ ✐t r❡♠❛✐♥s t♦ ✜♥❞ ❛♥ ✐♥❤❛❜✐t❛♥t ♦❢ T [Γ + /Γ] ✐♥ t❤❡ ❝♦♥t❡①t A : Type 0 , a : A✳ ❇✉t t❤❛♥❦s t♦ t❤❡ ♣r❡✈✐♦✉s •❡♠♠❛✱ ✇❡ ❦♥♦✇ t❤❛t T [Γ + /Γ] ≡ β Ω |T [Γ + /Γ]| ✱ t❤❡r❡❢♦r❡ ✉s✐♥❣ ❝♦♥✈❡rs✐♦♥ ✇❡ ❝❛♥ ✉s❡ ω |T [Γ + /Γ]| ✳ ❙♣❡••❡❞ ♦✉t✱ t❤❡ t❡r♠ θ Γ.T ✐s ✿ θ Γ.T ≡ J ∀x 1 :C 1 ,y 1 :M 1 =x 1 ,...,xn:Cn,yn:Mn=xn.T ( J ∀(x 2 :C 2 ,y 2 :M 2 =x 2 ,...,xn:Cn,yn:Mn=xn.T )[ω |C 1 | /x 1 ,ω |C 1 |+1 /y 1 ] ( • • • J ∀(xn:Cn,yn:Mn=xn.T )[∆ + /∆] (ω |T [Γ + /Γ]| , x n , y n ) • • • , x 2 , y 2 ), x 1 , y 1 ) ✇❤❡r❡ ∆ ✐s t❤❡ ❝♦♥t❡①t s✉❝❤ t❤❛t Γ = ∆, x n : C n , y n : M n = x n ✳ ❆s ❛ ❝♦r♦••❛r②✱ ✇❡ ♦❜t❛✐♥ t❤❡ ❢♦••♦✇✐♥❣ t❤❡♦r❡♠ ✿ ❚❤❡♦r❡♠ ✸ ✭❈❛♥♦♥✐❝✐t② ❢♦r ❣r♦✉♣♦✐❞ •❛✇s ✐♥ ▼▲■❉✮✳ ■❢ Γ ⊢ id T : Type ❛♥❞ ✐❢ ✇❡ ❤❛✈❡ t✇♦ t❡r♠s M ❛♥❞ N s✉❝❤ t❤❛t Γ ⊢ id M : T ❛♥❞ Γ ⊢ id N : T ✱ t❤❡♥ t❤❡r❡ ✐s ❛ ♣r♦♦❢ π s✉❝❤ t❤❛t Γ ⊢ π : M = N ✳ Pr♦♦❢✳ ❙✐♠♣•② ♥♦t✐❝❡ t❤❛t Γ ⊢ M = N : Type 0 ❛♥❞ ❛♣♣•② ♣r❡✈✐♦✉s •❡♠♠❛✳ ❚❤❡ r❡❛❞❡r s❤♦✉•❞ r❡♠❛r❦ ❤❡r❡ t❤❛t t❤❡ ♣r♦♦❢ π ✐s ❛•s♦ ✉♥✐q✉❡ ✉♣ t♦ ❡q✉❛•✐t② ✭❜② ❛♣♣•②✐♥❣ t❤❡ t❤❡♦r❡♠ t♦ M = N ✦✮✳ ❲❡ ❛r❡ ♥♦✇ r❡❛❞② t♦ s❤♦✇ t❤❛t ♣r❡✈✐♦✉s t❤❡♦r❡♠ ♠❛② ❜❡ ❣❡♥❡r❛•✐③❡❞ t♦ t❤❡ ✇❤♦•❡ s②st❡♠ ▼▲❚❚ ❜② ✉s✐♥❣ ♣❛r❛♠❡tr✐❝✐t② t❤❡♦r②✳ ❚❤❡♦r❡♠ ✹ ✭❈❛♥♦♥✐❝✐t② ♦❢ ✐♥❤❛❜✐t❛♥ts ♦❢ ❣r♦✉♣♦✐❞ •❛✇s ✐♥ ▼▲❚❚✮✳ ■❢ Γ ⊢ id T : Type✱ ⊢ M : ∀Γ.T ❛♥❞ ⊢ N : ∀Γ.T ✱ t❤❡♥ t❤❡r❡ ✐s ❛ ♣r♦♦❢ π s✉❝❤ t❤❛t - → γ : Γ ⊢ π : (M - → γ ) = (N - → γ )✳ Pr♦♦❢✳ ❇② s✉❝❝❡ss✐✈❡ ❡①t❡♥❞❡❞ ♣❛t❤✲✐♥❞✉❝t✐♦♥s ✭❢r♦♠ •❡❢t t♦ r✐❣❤t✮✱ ✇❡ ❝❛♥ ❞❡r✐✈❡ - → γ : Γ ⊢ (M - → γ ) = (N - → γ ) ❢r♦♠ ❛ ❞❡r✐✈❛t✐♦♥ ♦❢ A : Type 0 , a : A ⊢ (M Γ + ) = (N Γ + )✳ ❲❡ ♥♦t✐❝❡ t❤❛t t❤❡ t②♣❡ ♦❢ (M Γ + ) ✐s T [Γ + /Γ] ✇❤✐❝❤ ✐s t②♣❛❜•❡ ✐♥ ▼▲■❉❀ ❜② s✉❜st✐t✉t✐♦♥ ✇❡ ❤❛✈❡ A : Type 0 , a : A ⊢ id T [Γ + /Γ] : Type 0 ✳ ❚❤❡r❡❢♦r❡ ▲❡♠♠❛ ✺ ❣✐✈❡s ✉s t❤❛t T [Γ + /Γ] ≡ β Ω n ❢♦r s♦♠❡ n ∈ N✳ ❯s✐♥❣ ❝♦♥✈❡rs✐♦♥✱ ✇❡ ❤❛✈❡ A : Type 0 , a : A ⊢ (M Γ + ) : Ω n ✳ ❚❤❡r❡❢♦r❡ (M Γ + ) ✐s ❛♥ ✐♥❤❛❜✐t❛♥t ♦❢ ❛ ♣❛r❛♠❡tr✐❝ •♦♦♣ s♣❛❝❡❀ t❤❡r❡❢♦r❡ ✇❡ ❝❛♥ ✐♥✈♦❦❡ ❚❤❡♦r❡♠ ✷ t♦ ♦❜t❛✐♥ ♦❢ ♣r♦♦❢ t❤❛t (M Γ + ) = ω n ✳ ❙✐♠✐•❛r•② ✶✷ ✇❡ ❤❛✈❡ ❛ ♣r♦♦❢ ♦❢ (N Γ + ) = ω n ❛♥❞ ❜② ❝♦♥❝❛t❡♥❛t✐♥❣ t❤❡♠ ✇❡ ♦❜t❛✐♥ ❛ ♣r♦♦❢ ♦❢ (M - → γ ) = (N - → γ )✳ ❋✐♥❛••②✱ ✉s✐♥❣ t❤❡ s❛♠❡ ❛r❣✉♠❡♥ts ❛s ❛t t❤❡ ❡♥❞ ♦❢ ❙❡❝t✐♦♥ ✹ ✇❡ ❝❛♥ ♣r♦✈❡ t❤❛t π ✐s ✉♥✐q✉❡ ✉♣ t♦ ♣r♦♣♦s✐t✐♦♥❛• ❡q✉❛•✐t② ✭❛♥❞ s♦ ♦♥✮✳ ✻ ❉✐s❝✉ss✐♦♥s ✻✳✶ ❚❤❡ ❞❡✜♥✐t✐♦♥ ♦❢ ❣r♦✉♣♦✐❞ •❛✇s ❖✉r ❞❡✜♥✐t✐♦♥ ♦❢ ▼▲■❉ ✐s ✐♥s♣✐r❡❞ ❜② ❛♥ ✉♥♣✉❜•✐s❤❡❞ ♥♦t❡ ✇r✐tt❡♥ ❜② ❇r✉♥❡r✐❡ ❬✸(✳ ❖✉r s②♥t❛① ❢♦r ❝♦♥tr❛❝t✐❜•❡ ❝♦♥t❡①ts ✐s ❛ ❜✐t ♠♦r❡ ❣❡♥❡r❛•✿ ✐♥ ❇r✉♥❡r✐❡✬s ❞❡✜♥✐t✐♦♥ t❤❡ st❛rt✐♥❣ ♣♦✐♥t ♦❢ ♣❛t❤s ♦❝❝✉rr✐♥❣ ❛t ♦❞❞ ♣♦s✐t✐♦♥s ❛r❡ ❛•✇❛②s ✈❛r✐❛❜•❡ ✭✐❡✳ M k ✐s ❛•✇❛②s ❛ ✈❛r✐❛❜•❡✮ ❛♥❞ t❤❡r❡ ✐s ♥♦ ❝♦♠♣✉t❛t✐♦♥ r✉•❡s ✐♥ ❤✐s s②♥t❛①✳ ❇r✉♥❡r✐❡ ❞❡✜♥❡s ω✲❣r♦✉♣♦✐❞s ❛s ♠♦❞❡•s ♦❢ ✐ts s②♥t❛①✱ s✐♥❝❡ t❤❡ ❛❜s❡♥❝❡ ♦❢ ❝♦♠♣✉t❛t✐♦♥ r✉•❡s ♠❛❦❡s ❤✐s ❢r❛♠❡✇♦r❦ ♠♦r❡ ❢r❡❡ ❛❜♦✉t ❤♦✇ ❝♦❤❡r❡♥❝❡ ✐ss✉❡s ❛r❡ ❞❡❛•t ✇✐t❤✳ ❍♦✇❡✈❡r✱ t❤❡ ❣♦❛• ♦❢ ♦✉r s②♥t❛① ✐s ♥♦t ❣✐✈❡ t❤❡ ❣❡♥❡r❛• s②♥t❛① ❢♦r ✇❡❛❦ ω✲❣r♦✉♣♦✐❞s ❜✉t r❛t❤❡r t♦ st✉❞② ♦♥•② t❤❡ ❣r♦✉♣♦✐❞ str✉❝t✉r❡ ✐♥ t❤❡ ♣❛rt✐❝✉•❛r ❝❛s❡ ♦❢ t②♣❡ t❤❡♦r② ✇❤❡r❡ ❝♦♠♣✉t❛t✐♦♥ r✉•❡s ❛r❡ t❤❡ ♥❛t✉r❛• ✇❛② t♦ ❞❡❛• ✇✐t❤ ❝♦❤❡r❡♥❝❡✳ ◆❡✈❡rt❤❡•❡ss✱ ✐t ✇♦✉•❞ ❜❡ ❛♥ ✐♥t❡r❡st✐♥❣ ❢✉t✉r❡ ✇♦r❦ t♦ ♠❛❦❡ ❛ ♣r❡❝✐s❡ ❝♦♠♣❛r✐s♦♥ ❜❡t✇❡❡♥ ♦t❤❡r ❞❡✜♥✐t✐♦♥s ♦❢ ω✲❣r♦✉♣♦✐❞s ❛♥❞ ♠♦❞❡•s ♦❢ ▼▲■❉✳ ❚❤❡ s❡♠❛♥t✐❝❛• ♥❛t✉r❡ ♦❢ •❛r♥❡r ❛♥❞ ✈❛♥ ❞❡♥ ❇❡r❣ ❬✾( ♠❛❦❡s ✐t q✉✐t❡ ❞✐✣❝✉•t t♦ r❡•❛t❡ t♦ ♦✉r ✇♦r❦✱ ❤♦✇❡✈❡r ✇❡ ❜❡•✐❡✈❡ t❤❛t ▲✉♠s❞❛✐♥❡✬s ❝♦♥str✉❝t✐♦♥ ❬✺( ♦❢ ❛ ❝♦♥tr❛❝t✐❜•❡ ❣•♦❜✉•❛r ♦♣❡r❛❞ ♠❛② ❜❡ ❞❡s❝r✐❜❡❞ ✐♥ ♦✉r ❢r❛♠❡✇♦r❦✳ ✻✳✷ ❚❤❡ n✲❛r② ❝❛s❡ ❚❤r♦✉❣❤♦✉t t❤✐s ❛rt✐❝•❡✱ ✇❡ ♦♥•② ✉s❡ t❤❡ ✉♥❛r② ❝❛s❡ ♦❢ ♣❛r❛♠❡tr✐❝✐t② t❤❡♦r②✱ ❜✉t ✐t ❝♦✉•❞ ❜❡ ❡❛s✐•② ❣❡♥❡r❛•✐③❡❞ t♦ t❤❡ ❜✐♥❛r② ❝❛s❡ ❜② tr❛♥s♣♦rt✐♥❣ ❛•♦♥❣ t✇♦ ♣❛t❤s ✿ x = y 2 ≡ λ(p : x = y)(q : x ′ = y ′ ).p * (q * (x R )) = y R ✳ ❚❤✐s tr❛♥s•❛t✐♦♥ ✐s ✇❡••✲t②♣❡❞ ✉♥❞❡r t❤❡ ❜✐♥❛r② tr❛♥s•❛t✐♦♥ α : Type i , x : α, y : α 2 ❣✐✈❡♥ ❜② α α ′ : Type i , α R : α → α ′ → Type i , x : α, x ′ : α ′ , x R : α R x x ′ , y : α, y ′ : α ′ , y R : α R y y ′ ❚❤❡ tr❛♥s•❛t✐♦♥ 1 α x 2 : 1 α x * 1 α x ′ * (x R ) = x R ♦❢ 1 α x ✐s ❣✐✈❡♥ ❜② 1 α x 2 ≡ 1 α R x x x R ✇❤✐❝❤ ✐s ❞❡✜♥❡❞ ✉♥❞❡r t❤❡ tr❛♥s•❛t❡❞ ❝♦♥t❡①t α : Type, x : α 2 ✳ ❙✐♠✐•❛r•②✱ t❤❡ tr❛♥s•❛t✐♦♥ ♦❢ ♣❛t❤✲✐♥❞✉❝t✐♦♥ ✐s ♦❜t❛✐♥❡❞ ❜② ♥❡st✐♥❣ ✷✰✶ ♣❛t❤✲✐♥❞✉❝t✐♦♥✿ J(B, U, V ) 2 ≡ J(J(J( B 2 , U, V ), U ′ , V ′ ), U 2 , V 2 ) ■t ✐s ❛ r♦✉t✐♥❡ ❝❤❡❝❦ t♦ ❣❡♥❡r❛•✐③❡ t❤❡ ❛❜str❛❝t✐♦♥ t❤❡♦r❡♠ ♦❢ ❙❡❝t✐♦♥ ✸✱ ✐♥ ♦r❞❡r t♦ ❛ ❤❛✈❡ ❛ ❜✐♥❛r② ✈❡rs✐♦♥ ♦❢ ♣❛r❛♠❡tr✐❝✐t②✳ ▲✐❦❡✇✐s❡✱ t❤❡ n✲❛r② ❝❛s❡✱ ✐s ♦❜t❛✐♥❡❞ ❜② tr❛♥s♣♦rt✐♥❣ ❛•♦♥❣ n ♣❛t❤ ❛♥❞ t❤❡ tr❛♥s•❛t✐♦♥ ♦❢ ♣❛t❤✲✐♥❞✉❝t✐♦♥ ✐s ♦❜t❛✐♥❡❞ ❜② ♥❡st✐♥❣ n + 1 ♣❛t❤✲✐♥❞✉❝t✐♦♥s✳ ✶✸ ✻✳✸ ❊♥❝♦❞✐♥❣ ✐❞❡♥t✐t② t②♣❡s ✇✐t❤ ✐♥❞✉❝t✐✈❡ ❢❛♠✐•✐❡s✳ ■♥ ❞❡♣❡♥❞❡♥t t②♣❡ s②st❡♠s t❤❛t s✉♣♣♦rt ✐♥❞✉❝t✐✈❡ ❢❛♠✐•✐❡s✱ ✐t ✐s ♣♦ss✐❜•❡ t♦ ❡♥❝♦❞❡ ✐❞❡♥t✐t② t②♣❡s ❜② ❛♥ ✐♥❞✉❝t✐✈❡ ♣r❡❞✐❝❛t❡ ❬✹(✳ ❋♦r ✐♥st❛♥❝❡✱ ✐♥ t❤❡ ❝♦q ♣r♦♦❢ ❛ss✐st❛♥t✿ ■♥❞✉❝t✐✈❡ ♣❛t❤s ✭❆ ✿ ❚②♣❡✮ ✭❛ ✿ ❆✮ ✿ ❆ → ❚②♣❡ ✿❂ ✐❞♣❛t❤ ✿ ♣❛t❤s ❆ ❛ ❛✳ ❆s ❡①♣•❛✐♥❡❞ ✐♥ ❬✷( ✭❙❡❝t✐♦♥ ✺✳✹✮✱ t❤❡ ♣❛r❛♠❡tr✐❝✐t② tr❛♥s•❛t✐♦♥ ❡①t❡♥❞s ✇❡•• t♦ ✐♥❞✉❝t✐✈❡ ❢❛♠✐•✐❡s✳ ❚❤❡ ✐❞❡❛ ✐s t♦ tr❛♥s•❛t❡ ❛♥ ✐♥❞✉❝t✐✈❡ t②♣❡ I ❜② ❛ ♥❡✇ ✐♥❞✉❝t✐✈❡ I R ✇❤♦s❡ ❝♦♥str✉❝t♦rs ❛r❡ t❤❡ tr❛♥s•❛t✐♦♥ ♦❢ ❝♦♥str✉❝t♦rs ♦❢ I✳ ▲✐❦❡✇✐s❡✱ t❤❡ ❡•✐♠✐♥❛t✐♦♥ s❝❤❡♠❡ ❢♦r I R ✐s t❤❡ tr❛♥s•❛t✐♦♥ ♦❢ t❤❡ ♦♥❡ ♦❢ I✳ ■♥❞✉❝t✐✈❡ ♣❛t❤s❴| ✭❆ ✿ ❚②♣❡✮ ✭❆❴| ✿ ❆ → ❚②♣❡✮ ✭❛ ✿ ❆✮ ✭❛❴| ✿ ❆❴| ❛✮ ✿ ❢♦r❛•• ①✱ ❆❴| ① → ♣❛t❤s ❆ ❛ ① → ❚②♣❡ ✿❂ ✐❞♣❛t❤❴| ✿ ♣❛t❤s❴| ❆ ❆❴| ❛ ❛❴| ❛ ❛❴| ✭✐❞♣❛t❤ ❆ ❛✮✳ ❚❤❡r❡ ✐s ❛♥ ❡q✉✐✈❛•❡♥❝❡ ♦❢ t②♣❡s ✭✐♥ t❤❡ ❤♦♠♦t♦♣② t❤❡♦r② s❡♥s❡✱ s❡❡ ❬✽(✮ ❜❡t✇❡❡♥ t❤✐s ✐♥❞✉❝t✐✈❡ t②♣❡ ❛♥❞ ♦✉r tr❛♥s•❛t✐♦♥ ♦❢ ✐❞❡♥t✐t②✳ ■t ✐s ♦❜t❛✐♥❡❞ ❜② ✉s✐♥❣ t❤❡ ✐♥❞✉❝t✐♦♥ ♣r✐♥❝✐♣•❡ ❛ss♦❝✐❛t❡❞ ✇✐t❤ paths R ✐♥ ♦♥❡ ❞✐r❡❝t✐♦♥❀ ❛♥❞ ❜② ♥❡st❡❞ ♣❛t❤✲ ✐♥❞✉❝t✐♦♥s ♦♥ p ❛♥❞ ♦♥ t❤❡ ♣r♦♦❢ ♦❢ tr❛♥s♣♦rt ❛•♦♥❣ p ✐♥ t❤❡ ♦t❤❡r ❞✐r❡❝t✐♦♥✳ ❚❤✐s ✐♥❞✐❝❛t❡s t❤❛t t❤❡② ❛r❡ ♠♦r❛••② t❤❡ s❛♠❡❀ ✐t ♠❛② ❝♦♥✈✐♥❝❡ t❤❡ r❡❛❞❡r t❤❛t t❤❡ r❡s✉•ts ♦❢ t❤❡ •❛st t✇♦ s❡❝t✐♦♥s ❝♦✉•❞ ❤❛✈❡ ❜❡❡♥ ❝❛rr✐❡❞ ♦✉t ✉s✐♥❣ t❤❡ ❡♥❝♦❞✐♥❣ ✐♥st❡❛❞ ♦❢ t❤❡ ♣r✐♠✐t✐✈❡ ♥♦t✐♦♥ ♦❢ ✐❞❡♥t✐t② t②♣❡s✳ ✻✳✹ ❉❡❛•✐♥❣ ✇✐t❤ ❛①✐♦♠s ❲❤✐•❡ ❢♦r♠❛•✐③✐♥❣ ♣r♦♦❢s t❤❛t ♥❡❡❞ ❛①✐♦♠s ✇❤✐❝❤ ❛r❡ ✐♥❞❡♣❡♥❞❡♥t✱ ✐t ✐s ❛ ❝♦♠♠♦♥ ♣r❛❝t✐❝❡ t♦ s✐♠♣•② ❛❞❞ t❤❡♠ ✐♥ t❤❡ ❝♦♥t❡①t✳ ❚❤❡♥✱ ✐❢ ♦♥❡ ✇❛♥t t♦ ✉s❡ t❤❡ ♣❛r❛✲ ♠❡tr✐❝✐t② tr❛♥s•❛t✐♦♥✱ ❤❡ ❛•s♦ ♥❡❡❞s t♦ ♣r♦✈✐❞❡ ❛ ✇✐t♥❡ss ♦❢ t❤❡ ♣❛r❛♠❡tr✐❝✐t② ♦❢ t❤❡ ❛①✐♦♠✳ ❚❤❡r❡❢♦r❡ ❛①✐♦♠s t❤❛t ❝❛♥ ♣r♦✈❡ t❤❡✐r ♦✇♥ ♣❛r❛♠❡tr✐❝✐t② ❛r❡ ✇❡••✲❜❡❤❛✈❡❞ ✇✐t❤ r❡s♣❡❝t t♦ t❤❡ tr❛♥s•❛t✐♦♥✳ ▼♦r❡ ❢♦r♠❛••②✱ ✇❡ s❛② t❤❛t ❛ ❝•♦s❡❞ t②♣❡ P : Type ✐s ♣r♦✈❛❜•② ♣❛r❛♠❡tr✐❝ ✐❢ t❤❡ t②♣❡ ∀h : P, h ∈ P ✐s ✐♥❤❛❜✐t❡❞✳ ❲❡ ✇✐•• ♥♦✇ ❣✐✈❡ t✇♦ ❡①❛♠♣•❡s ♦❢ ❛①✐♦♠s ✉s✐♥❣ ✐❞❡♥t✐t② t②♣❡s ✇❤✐❝❤ ❛r❡ ♣r♦✈❛❜•② ♣❛r❛♠❡tr✐❝✳ • ✉♥✐q✉❡♥❡ss ♦❢ ✐❞❡♥t✐t② ♣r♦♦❢s ✭❯■P✮ ✿ ▲❡t uip ❜❡ t❤❡ ❢♦••♦✇✐♥❣ t②♣❡ uip ≡ ∀X : Type, x y : X, p q : x = y.p = q✳ ❲❡ ✇❛♥t t♦ ✜♥❞ ❛♥ ✐♥❤❛❜✐t❛♥t ♦❢ ∀f : uip.f ∈ uip ✳ ❚❤❡ st❛t❡♠❡♥t f ∈ uip ✉♥❢♦•❞s ✐♥t♦ ∀ X : Type, x y : X, p q : x = y .(f A x y p q) * (p R ) = q R ✳ ❚❤❡ ❝♦♥❝•✉s✐♦♥ ✐s ❛♥ ❡q✉❛•✐t② ❜❡t✇❡❡♥ ♣❛t❤s✱ s♦ ✐t ✐s ♣r♦✈❛❜•❡ ✉s✐♥❣ f ✳ • ❢✉♥❝t✐♦♥ ❡①t❡♥s✐♦♥❛•✐t② ✿ ▲❡t funext ❜❡ t❤❡ ❢♦••♦✇✐♥❣ t②♣❡ funext ≡ ∀A : Type, B : A → Type, f g : ∀x : A.Bx.(∀x : A.f x = g x) → f = g✳ ■♥ ❤✐s ♦r✐❣✐♥❛• ❞❡✈❡•♦♣♠❡♥t✱ ❱♦❡❞✈♦❡s❦② s❤♦✇❡❞ t❤❛t funext ✐s •♦❣✐❝❛••② ❡q✉✐✈❛•❡♥t ✭t❤❡r❡ ✐s ❛ ❢✉♥❝t✐♦♥ ✐♥ ❜♦t❤ ❞✐r❡❝t✐♦♥s✮ t♦ t❤❡ s♦✲❝❛••❡❞ ✇❡❛❦ ❡①t❡♥s✐♦♥❛•
A.x = y ✐s t❤❡ ♣r❡❞✐❝❛t❡ ❢♦r ❝♦♥tr❛❝t✐❜•❡ t②♣❡s ❀ ✐❡✳ t②♣❡s ✇❤✐❝❤ ❛r❡ ❡q✉✐✈❛•❡♥t t♦ t❤❡ s✐♥❣•❡t♦♥ t②♣❡✳ ❲❡ ♥♦✇ s❦❡t❝❤ t❤❡ ♣r♦♦❢ t❤❛t weakext ✐s ♣r♦✈❛❜•② ♣❛r❛♠❡tr✐❝ ✭❛♥❞ t❤✉s s♦ ✐s funext✮✳ ❚❤❡ ♠❛✐♥ ✐❞❡❛ ✐s t♦ ♥♦t✐❝❡ t❤❛t M ∈ Contr A ✐s •♦❣✐❝❛••② ❡q✉✐✈❛•❡♥t t♦ Contr ( A M 1 ) ✶✹ ✇❤❡r❡ M 1 ✐s t❤❡ ✜rst ♣r♦•❡❝t✐♦♥ ♦❢ M ✳ ❚❤❡ ✉♥❢♦•❞✐♥❣ ♦❢ k ∈ weakext ✐s✿ ∀A : Type, A R : A →

  ♥❡ssM : A M t❤❛t t❤❡ M s❛t✐s✜❡s t❤❡ ♣r❡❞✐❝❛t❡✳ ❚❤✐s tr❛♥s•❛t✐♦♥ ♠❛② ❜❡ ❡①t❡♥❞❡❞ t♦ ❝♦♣❡ ✇✐t❤ ✐❞❡♥t✐t② t②♣❡s ❜② s❡tt✐♥❣ a = b : a = b → Type t♦ ❜❡ t❤❡ ♣r❡❞✐❝❛t❡ λp : a = b.p * ( a ) = b ✇❤❡r❡ p * ✐s t❤❡ tr❛♥s♣♦rt ❛•♦♥❣ p ♦❢ t❤❡ ♣r❡❞✐❝❛t❡ ❣❡♥❡r✲ ✷ ❛t❡❞ ❜② t❤❡ ❝♦♠♠♦♥ t②♣❡ ♦❢ a ❛♥❞ b✳ ❚❤❡♥✱ ✐t ✐s ❡❛s② ✲❛•t❤♦✉❣❤ q✉✐t❡ ✈❡r❜♦s❡✲ t♦ ✜♥❞ ❛ tr❛♥s•❛t✐♦♥ ♦❢ ✐♥tr♦❞✉❝t✐♦♥ ❛♥❞ ❡•✐♠✐♥❛t✐♦♥ r✉•❡s ♦❢ ✐❞❡♥t✐t② t②♣❡s ❛s ✇❡•• ❛s ❝❤❡❝❦✐♥❣ t❤❛t t❤❡s❡ tr❛♥s•❛t✐♦♥s ♣r❡s❡r✈❡ ❝♦♠♣✉t❛t✐♦♥ r✉•❡s✳ ❚❤✐s ❛••♦✇s t♦ ❡①t❡♥❞ ❇❡r♥❛r❞②✬s ❛❜str❛❝t✐♦♥ t❤❡♦r❡♠ t♦ ✐❞❡♥t✐t② t②♣❡s✳ ❯s✐♥❣ t❤✐s ❢r❛♠❡✇♦r❦✱ ✇❡ ❛r❡ ❛❜•❡ t♦ ❣❡♥❡r❛•✐③❡ t❤❡ ✉♥✐q✉❡♥❡ss ♣r♦♣❡rt② ♦❢ t❤❡ ♣♦•②♠♦r♣❤✐❝ ✐❞❡♥t✐t② t②♣❡ t♦ ❛♥② ♣❛r❛♠❡tr✐❝ •♦♦♣ s♣❛❝❡✳ ❚❤❡ ♣r♦♦❢ ♣r♦❝❡❡❞ ❜② ✐♥❞✉❝t✐♦♥ ♦♥ t❤❡ ✐♥❞❡① ♦❢ t❤❡ •♦♦♣ s♣❛❝❡ ❛♥❞ ✉s❡s ❛•❣❡❜r❛✐❝ ♣r♦♣❡rt✐❡s ♦❢ tr❛♥s♣♦rt✳ ❖✉t•✐♥❡ ♦❢ t❤❡ ♣❛♣❡r✳ ■♥ ❙❡❝t✐♦♥ ✷✱ ✇❡ ✐♥tr♦❞✉❝❡ t❤❡ t②♣❡ t❤❡♦r❡t✐❝❛• s❡tt✐♥❣ t❤❛t ✐s ✉s❡❞ ✐♥ t❤❡ ❛rt✐❝•❡✳ ❙❡❝t✐♦♥ ✸ ✐s ❞❡✈♦t❡❞ t♦ t❤❡ ♣r♦♦❢ t❤❛t❇❡r♥❛r❞②✬s ♣❛r❛♠❡tr✐❝✐t② ♠❛② ❜❡ ❡①t❡♥❞❡❞ t♦ ❝♦♣❡ ✇✐t❤ ✐❞❡♥t✐t② t②♣❡s✳ ■♥ ❙❡❝t✐♦♥ ✹✱ ✇❡ ✉s❡ t❤✐s tr❛♥s•❛t✐♦

  Type, P : A → Type, P R : (∀x : A, x R : A R x.P x → Type), φ : (∀x : A.Contr (P x)), φ R : (∀x : A, x R : A R x.(φ x) ∈ Contr P x ).(k A P φ) ∈ Contr (∀x :A.P x) ❚❤❡r❡❢♦r❡✱ ✉s✐♥❣ t❤❡ •♦❣✐❝❛• ❡q✉✐✈❛•❡♥❝❡ ✐♥ ♦♥❡ ❞✐r❡❝t✐♦♥ ✇❡ ❝❛♥ ❞❡❞✉❝❡ t❤❡ ❝♦♥❝•✉✲ s✐♦♥ ❢r♦♠ Contr (k A P φ) 1 ∈ ∀x : A.P x) )✳ ❚❤❡♥ ✉s✐♥❣ k : weakext t✇♦ t✐♠❡s✱ ✐t ✐s ❡♥♦✉❣❤ t♦ ♣r♦✈❡ t❤❛t ∀x : A, x R : A R x.Contr ((k A P φ) 1 x) ∈ P x ) ✭✶✮✳ ◆♦t✐❝❡ t❤❛t (k A P φ) 1 x = A (φ x) 1 ❜❡❝❛✉s❡ A ✐s ❝♦♥tr❛❝t✐❜•❡✳ ❙♦ ✇❡ ❝❛♥ tr❛♥s✲ ♣♦rt ❛•♦♥❣ t❤✐s ♣❛t❤ ✐♥ ✭✶✮ t♦ ♦❜t❛✐♥ ∀x : A, x R : A R x.Contr ((φx) 1 ∈ P x ) ✭✷✮✳ ◆♦✇✱ ✉s✐♥❣ t❤❡ ♦t❤❡r ❞✐r❡❝t✐♦♥ ♦❢ •♦❣✐❝❛• ✐♠♣•✐❝❛t✐♦♥✱ ✭✷✮ ✐s ✐♠♣•✐❡❞ ❜② ∀x : A, x R : A R x.(φx) ∈ Contr (P x) ) ✇❤✐❝❤ ✐s ❡①❛❝t•② t❤❡ t②♣❡ ♦❢ φ R ✳ ✼ ❈♦♥❝•✉s✐♦♥ ❚❤✐s ✇♦r❦ s❤♦✇s t❤❛t ♣❛r❛♠❡tr✐❝✐t② t❤❡♦r② ♠❛② ❜❡ ✉s❡❞ t♦ ❞❡❞✉❝❡ ♣r♦♣❡rt✐❡s ❛❜♦✉t t❤❡ ❛•❣❡❜r❛✐❝ str✉❝t✉r❡ ♦❢ ✐❞❡♥t✐t② t②♣❡s✳ ■t ❛••♦✇s t♦ ❣✐✈❡ ❢♦r♠❛• ❛r❣✉♠❡♥ts t♦ ♣r♦✈❡ ❝❛♥♦♥✐❝✐t② r❡s✉•ts ❛❜♦✉t ❞❡✜♥✐t✐♦♥s ✐♥ ❛ ♣r♦♦❢✲r❡•❡✈❛♥t s❡tt✐♥❣✳ ❚❤❡ ♠♦st ✐♠♣♦rt❛♥t q✉❡st✐♦♥ t❤❛t r❡♠❛✐♥s ♦♣❡♥ ✐s ✇❤❡t❤❡r ♦r ♥♦t ✇❡ ❝❛♥ ❡①t❡♥❞ t❤❡ tr❛♥s•❛t✐♦♥ ❛♥❞ t❤❡ ✉♥✐q✉❡♥❡ss ♣r♦♣❡rt② ♦❢ ❣r♦✉♣♦✐❞ •❛✇s t♦ ❞❡❛• ✇✐t❤ ❱♦❡✈♦❞✲ s❦②✬s ✉♥✐✈❛•❡♥❝❡ ❛①✐♦♠✳ ❖♥❡ ✇❛② t♦ s♦•✈❡ t❤✐s q✉❡st✐♦♥ ✇♦✉•❞ ❜❡ t♦ ♣r♦✈❡ t❤❛t ✉♥✐✈❛•❡♥❝❡ ❛①✐♦♠ ✐s ♣r♦✈❛❜•② ♣❛r❛♠❡tr✐❝ ✇❤✐❝❤ ✇♦✉•❞ ②✐❡•❞ t♦ ❛ ♣♦s✐t✐✈❡ ❛♥s✇❡r t♦ t❤❡ q✉❡st✐♦♥ ♦❢ t❤❡ ❝♦♠♣❛t✐❜✐•✐t② ♦❢ ♣❛r❛♠❡tr✐❝✐t② t❤❡♦r② ❛♥❞ ✉♥✐✈❛•❡♥❝❡✳ |❡❣❛r❞✲ •❡ss ♦❢ t❤❡ ❛♥s✇❡r t♦ t❤✐s ♣r♦❜•❡♠✱ s♦•✈✐♥❣ ✐t ✇♦✉•❞ ❣✐✈❡ ❛ ❜❡tt❡r ✉♥❞❡rst❛♥❞✐♥❣ ♦❢ ♣♦•②♠♦r♣❤✐❝ t②♣❡ q✉❛♥t✐✜❝❛t✐♦♥s ✐♥ ✉♥✐✈❛•❡♥t ✉♥✐✈❡rs❡s✳ |❡❢❡r❡♥❝❡s ❬✶( ❍❡♥❦ ❇❛r❡♥❞r❡❣t✳ ▲❛♠❜❞❛ ❈❛•❝✉•✐ ✇✐t❤ ❚②♣❡s✳ ■♥ ❍❛♥❞❜♦♦❦ ♦❢ ▲♦❣✐❝ ✐♥ ❈♦♠♣✉t❡r ❙❝✐❡♥❝❡✱ ♣❛❣❡s ✶✶✼✕✸✵✾✳ ❖①❢♦r❞ ❯♥✐✈❡rs✐t② Pr❡ss✱ ✶✾✾✷✳ ❬✷( ❏❡❛♥✲P❤✐•✐♣♣❡ ❇❡r♥❛r❞②✱ P❛tr✐❦ ❏❛♥ss♦♥✱ ❛♥❞ |♦ss P❛t❡rs♦♥✳ Pr♦♦❢s ❢♦r ❢r❡❡ ✲ ♣❛r❛♠❡tr✐❝✐t② ❢♦r ❞❡♣❡♥❞❡♥t t②♣❡s✳ ❏✳ ❋✉♥❝t✳ Pr♦❣r❛♠✳✱ ✷✷✭✷✮✿✶✵✼✕✶✺✷✱ ✷✵✶✷✳ ❬✸( •✉✐••❛✉♠❡ ❇r✉♥❡r✐❡✳ ❙②♥t❛❝t✐❝ ❣r♦t❤❡♥❞✐❡❝❦ ✇❡❛❦ ∞✲❣r♦✉♣♦✐❞s✳ ❆✈❛✐•❛❜•❡ ❛s ❤tt♣✿✴✴✉❢✲✐❛s✲✷✵✶✷✳ ✇✐❦✐s♣❛❝❡s✳❝♦♠✴❢✐•❡✴✈✐❡✇✴❙②♥t❛❝t✐❝■♥❢✐♥✐t②•r♦✉♣♦✐❞s|❛✇❉❡❢✐♥✐t✐♦♥✳♣❞❢✳ ❬✹( P❡t❡r ❉②❜•❡r✳ ■♥❞✉❝t✐✈❡ ❢❛♠✐•✐❡s✳ ❋♦r♠❛• ❆s♣✳ ❈♦♠♣✉t✳✱ ✻✭✹✮✿✹✹✵✕✹✻✺✱ ✶✾✾✹✳ ❬✺( P❡t❡r ▲❡❋❛♥✉ ▲✉♠s❞❛✐♥❡✳ ❲❡❛❦ ♦♠❡❣❛✲❝❛t❡❣♦r✐❡s ❢r♦♠ ✐♥t❡♥s✐♦♥❛• t②♣❡ t❤❡♦r②✳ ■♥ P✐❡rr❡✲▲♦✉✐s ❈✉r✐❡♥✱ ❡❞✐t♦r✱ ❚▲❈❆✱ ✈♦•✉♠❡ ✺✻✵✽ ♦❢ ▲❡❝t✉r❡ ◆♦t❡s ✐♥ ❈♦♠♣✉t❡r ❙❝✐❡♥❝❡✱ ♣❛❣❡s ✶✼✷✕✶✽✼✳ ❙♣r✐♥❣❡r✱ ✷✵✵✾✳ ❬✻( )❤❛♦❤✉✐ ▲✉♦✳ ❊❝❝✱ ❛♥ ❡①t❡♥❞❡❞ ❝❛•❝✉•✉s ♦❢ ❝♦♥str✉❝t✐♦♥s✳ ■♥ ▲■❈❙✱ ♣❛❣❡s ✸✽✻✕✸✾✺✳ ■❊❊❊ ❈♦♠♣✉t❡r ❙♦❝✐❡t②✱ ✶✾✽✾✳ ❬✼( ❏♦❤♥ ❈✳ |❡②♥♦•❞s✳ ❚②♣❡s✱ ❆❜str❛❝t✐♦♥ ❛♥❞ P❛r❛♠❡tr✐❝ P♦•②♠♦r♣❤✐s♠✳ ■♥ ■❋■P ❈♦♥❣r❡ss✱ ♣❛❣❡s ✺✶✸✕✺✷✸✱ ✶✾✽✸✳ ❬✽( ❚❤❡ ❯♥✐✈❛•❡♥t ❋♦✉♥❞❛t✐♦♥s Pr♦❣r❛♠✳ ❍♦♠♦t♦♣② ❚②♣❡ ❚❤❡♦r②✿ ❯♥✐✈❛•❡♥t ❋♦✉♥❞❛t✐♦♥s ♦❢▼❛t❤❡♠❛t✐❝s✳ ❤tt♣✿✴✴❤♦♠♦t♦♣②t②♣❡t❤❡♦r②✳♦r❣✴❜♦♦❦✱ ■♥st✐t✉t❡ ❢♦r ❆❞✈❛♥❝❡❞ ❙t✉❞②✱ ✷✵✶✸✳ ❬✾( ❇❡♥♥♦ ✈❛♥ ❞❡♥ ❇❡r❣ ❛♥❞ |✐❝❤❛r❞ •❛r♥❡r✳ ❚②♣❡s ❛r❡ ✇❡❛❦ ω✲❣r♦✉♣♦✐❞s✳ Pr♦❝❡❡❞✐♥❣s ♦❢ t❤❡ ▲♦♥❞♦♥ ▼❛t❤❡♠❛t✐❝❛• ❙♦❝✐❡t②✱ ✶✵✷✭✷✮✿✸✼✵✕✸✾✹✱ ✷✵✶✶✳ ✶✺

✇❤❡r❡ y ❞♦❡s ♥♦t ♦❝❝✉r ✐♥ X✳ ■t ✐s ♦❢t❡♥ ✉s❡❞ t♦ ❝♦❡r❝❡ ❜❡t✇❡❡♥ t②♣❡ ❢❛♠✐•✐❡s✿ ❣✐✈❡♥ ❛ t②♣❡ ❢❛♠✐•② X : C → Type i ✱ ❛ ♣❛t❤ P :U = V ❜❡t✇❡❡♥ t✇♦ ♣♦✐♥ts U, V : C✱ ❛♥❞ ❛ t❡r♠ M ✐♥ X U ✱ t❤❡ tr❛♥s♣♦rt P * x:C.X (M ) ♦❢ M ❛•♦♥❣ P ✐♥❤❛❜✐ts X V ✳ ■t s❛t✐s✜❡s t❤❡ ❢♦••♦✇✐♥❣ ❞❡r✐✈❛❜•❡ r✉•❡ ✿ Γ, x : C ⊢ X : Type j Γ ⊢ P : U = C V Γ ⊢ M : X[U/x] Γ ⊢ P * x:C.X (M ) : X[V /x] tr❛♥s♣♦rt ❲❡ s♦♠❡t✐♠❡s ❛•s♦ ♦♠✐t t❤❡ t②♣❡ ❢❛♠✐•② ✇❤❡♥ ✐t ❝❛♥ ❜❡ ❣✉❡ss❡❞ ❢r♦♠ t❤❡ ❝♦♥t❡①t✳ ❚❤❡ ❝♦♠♣✉t❛t✐♦♥ r✉•❡ t❡••s ✉s t❤❛t tr❛♥s♣♦rt✐♥❣ ❛•♦♥❣ ❛ r❡✢❡①✐✈✐t② ✐s s❛♠❡ ❛s ❞♦✐♥❣ ♥♦t❤✐♥❣ ✿ 1 U * (M ) ≡ β M ✳ ✸ ❊①t❡♥❞✐♥❣ |❡•❛t✐♦♥❛• P❛r❛♠❡tr✐❝✐t② t♦ ■❞❡♥t✐t② t②♣❡s ■♥ t❤✐s s❡❝t✐♦♥✱ ✇❡ ❡①♣•❛✐♥ ❤♦✇ t♦ ❡①t❡♥❞ ❇❡r♥❛r❞②✬s ♣❛r❛♠❡tr✐❝✐t② tr❛♥s•❛t✐♦♥ ❜❡•♦✇ t♦ ♣r✐♠✐t✐✈❡ ✐❞❡♥t✐t② t②♣❡s✳ ❚❤❡♥ ✇❡ ♣r♦✈❡ t❤❛t t❤✐s ❡①t❡♥s✐♦♥ ♣r❡s❡r✈❡s t②♣✐♥❣ ✭❚❤❡✲ ✹ wf ✇❢✲❡♠♣t② Γ wf Γ ⊢ B : Type i Γ, x : B wf ✇❢ Γ wf Γ ⊢ Type i : Type i+1 ✉♥✐✈ Γ wf (x : A) ∈ Γ Γ ⊢ x : A ✈❛r✐❛❜•❡s Γ, x : A ⊢ M : B Γ ⊢ λx : A.M : ∀x : A.B ❛❜str❛❝t✐♦♥ Γ ⊢ M : ∀x : A.B Γ ⊢ N : A Γ ⊢ (M N ) : B[N/x] ❛♣♣•✐❝❛t✐♦♥ Γ ⊢ M : A ′ Γ ⊢ A : Type i A ′ A Γ ⊢ M : A ❝♦♥✈❡rs✐♦♥ Γ ⊢ A : Type i Γ, x : A ⊢ B : Type i Γ ⊢ ∀x : A.B : Type i ♣r♦❞✉❝t Γ ⊢ M : C Γ ⊢ N : C Γ ⊢ C : Type i Γ ⊢ M = C N : Type i ✐❞❡♥t✐t② Γ ⊢ M : C Γ ⊢ 1 C M : M = C Mr❡❢•❡①✐✈✐t② Γ ⊢ M : C Γ, x : C, y : M = x ⊢ P : Type i Γ ⊢ B : P [M/x, 1 C M /y]

M * ( M ) = M ∈ C M ✳ ❙♦✱ ✇❡ ❝♦♥❝•✉❞❡ Γ ⊢ 1 C M : 1 C M ∈ C ✳ • ♣❛t❤✲✐♥❞✉❝t✐♦♥✿ ❚❤❡ ✐♥❞✉❝t✐♦♥ ❤②♣♦t❤❡s✐s ❢♦r ✭❜✮ ❛r❡ ✿ Γ ⊢ M : M ∈ C (1) Γ, x : C, y : M = x ⊢ P : P → Type i (2) Γ ⊢ B : B ∈ P [M/x, 1 C M /y] (3) Γ ⊢ U : U ∈ C (4) Γ ⊢ V : V ∈ M = U (5) ❛♥❞ t❤❡ ✐♥❞✉❝t✐♦♥ ❤②♣♦t❤❡s✐s ❢♦r ✭❛✮ ❛r❡ ✿ Γ ⊢ M : C (6) Γ, x : C, y : M = x ⊢ P : Type i (7) Γ ⊢ B : P [M/x, 1 C M /y] (8) Γ ⊢ U : C (9) Γ ⊢ V : M = U (10) ▲❡t T ❜❡ t❤❡ ❢♦••♦✇✐♥❣ t❡r♠ ✿ J ∀x:C,y:M =x.J(B,x,y)∈ P [y * ( M )/x R ,1 y * ( M ) /y R ] ( B , U, V ) ❋✐rst✱ ✇❡ ❤❛✈❡ t♦ t②♣❡❝❤❡❝❦ T ❜② s❤♦✇✐♥❣ t❤❛t Γ ⊢ T : J(B, U, V ) ∈ P [y * ( M )/x R , 1 y * ( M ) /y R , U/x, V /y] ( * )