{'fraction_non_alphanumeric': 0.056005034160373966, 'fraction_numerical': 0.012068500539374326, 'mean_word_length': 3.943561826463726, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 7, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Cubical informal type theory: the higher groupoid structure

Following a project of developing conventions and notations for informal type theory carried out in the homotopy type theory book for a framework built out of an augmentation of constructive type theory with axioms governing higher-dimensional constructions via Voevodsky's univalance axiom and higher-inductive types, this paper proposes a way of doing informal type theory with a cubical type theory as the underlying foundation instead. To that end, we adopt a cubical type theory recently proposed by Angiuli, Hou (Favonia) and Harper, a framework with a cumulative hierarchy of univalent Kan universes, full univalence and instances of higher-inductive types. In the present paper we confine ourselves to some elementary theorems concerning the higher groupoid structure of types.


Introduction
Higher-dimensional type-theoretic foundations is gaining wider acceptance in the mathematical community since the emergence of homotopy type theory [14], a young but promising research field and foundational language for mathematics that moves conventional type theory to higher dimensions by interpreting types as spaces, terms as points, equalities as paths and functions as continuous maps. One of the reasons (but certainly not the only one) for this growing interest among mathematicians can be attributed to the collective efforts of the authors of the book homotopy type theory [14] to develop an informal but rigorous style of doing mathematics in natural language assuming higher-dimensional type theory as the underlying foundation.
This 'informal type theory' project, originally proposed by Peter Aczel [12], was carried out in the homotopy type theory book [14] for a framework built out of an augmentation of ordinary (one-dimensional) constructive type theory [11] with axioms governing higher-dimensional constructions via Voevodsky's univalance axiom and higher-inductive types (henceforth 'conventional homotopy type theory'). Unfortunately, however, the use of univalence and higherinductive types as axioms is quite problematic computationally speaking, since using axioms in a type theory amounts to introducing new canonical terms without saying exactly how to compute with them. Simply put, the presence of the univalence and higher-inductive types as axioms in constructive type theory blocks computation, meaning that conventional homotopy type theory lacks all the desirable computational properties of a type theory such as canonicity [14].
In response to that, Bezem et al. [6] have constructed a model of constructive type theory that validates the univalence axiom using cubical sets (a constructive mathematical concept due to Kan [9]) and many cubical type theories (type-theoretic paraphrases of the cubical interpretation) have been developed since then. 1 Cohen et al. [8] have proposed a cubical type theory which proves univalence and has possible extensions with some higher inductive types. Licata and Brunerie [10] have introduced a cubical type theory with instances of higher-inductive types and, very recently, Angiuli et al. [4] have presented a cubical type theory with a cumulative hierarchy of univalent universes, full univalence and instances of higher-inductive types.
The aim of this paper is to offer a cubical perspective to the informal type theory of the homotopy type theory book by adopting not conventional homotopy type theory but a cubical type theory as the implicit basis of our informal reasoning. Our approach is based on the framework of Angiuli et al. [4], which we shall refer to as 'computational cubical type theory'. Thus, although this paper is intended to be self-contained, the reader may find it helpful to refer to [4,3,2] for further clarification.

Computational cubical type theory
As usual in type theory, the language of computational cubical type theory is composed of ordinary terms from an extended lambda calculus with constants for the constructors and eliminators of type formers, such as However, computational cubical type theory features a very unique sort of terms, called dimension terms, which can be combined with ordinary terms to provide an explicit higher-dimensional treatment of the terms of the language.

Dimension terms
What are exactly dimension terms? Syntactically, a dimension term is either 0 or 1 (which we sometimes abbreviate as ǫ) or a dimension name: x, y, z, ...

1.
Degeneration. This allows one to trivially regard a construction at any dimension as a higher construction at the next dimension. For instance, any (x 1 , ..., x n )-cube M can be degenerated into an (x 1 , ..., x n , x)-cube M with a trivial x face, that is, we have A 0/x ≡ A 1/x ≡ A. When drawing Kan composition diagrams, we shall always use double lines (===) to indicate degenerate faces.

2.
Coercion. This can be seen as a cubical generalization of the transport operation from the homotopy type theory book [14,Lem 2.3.1]. Essentially, coercion states that, given any x-type A and any term M ∈ A r/x , we have a term of the type A r ′ /x , called the coercion of M in A, and denoted by coe r r ′ x.A (M ). 3. Homogeneous Kan composition. Simply put, homogeneous Kan composition ensures that any open box has a lid. The simplest composition scenario can be illustrated as follows: The above diagram states that given any x-line M in a type A and two ylines N 0 and N 0 in A such that (i) the left boundary of M is strictly equal to the left boundary of N 0 and (ii) the right boundary of M is strictly equal to the left boundary of N 0 , there exists an x-line in A from the right boundary of N 0 to the right boundary of N 1 (the dotted line in the diagram). The resulting new line is called the homogeneous Kan composite of M with N 0 and N 1 and denoted by hcom 0 1 . Crucially, homogeneous Kan composition also asserts the existence of an (x, y)-square in A with the x-lines M and hcom 0 1 A (M )( 0 x ⊲ y.N 0 , 1 x ⊲ y.N 1 ) respectively at the top and bottom, and the y-lines N 0 and N 1 respectively at the left and right (this is the square depicted in the above diagram). We call the resulting square the filler of the Kan composition scenario.
It is worth mentioning that homogeneous Kan composition need not be limited to two-dimensional open boxes. In fact, its general form is The constructs from items 2 and 3 are called the Kan conditions, and together they can be seen as a higher-dimensional representation of the elimination rule of the identification type of constructive type theory known in the homotopy type book as path induction [14, §1.12.1] (see Section 4.1).

Identification type
Given any x-type A and any two terms M ∈ A 0/x and N ∈ A 1/x we can construct the type M = x.A N of identifications between the terms M and N in the type A indexed by x. It is important to emphasize that, unlike in conventional homotopy type theory [14], the identification type of computational cubical type theory is always indexed by a particular dimension term.
The introduction, elimination, computation and uniqueness rules of the identification type are the following: 1. Introduction. The identification type is inhabited by identifications, which are constructed by dimension abstraction. Given any x-line P in A from M to N , we write x P to indicate the identification of M and N in A obtained by abstracting x in the x-line P . Consequently, all occurrences of x in P are binded in the identification x P , and, because the resulting identification does not depend on the dimension term x, as a general rule, identifications formed by abstracting lines (n + 1-cubes) in a type can be seen as points (n-cubes) in their corresponding identification types.
2. Elimination. Given any identification P ∈ M 0 = x.A M 1 and a dimension term r, we can apply the identification P to r to obtain an r-line from M 0 to N 1 in A r/x , denoted P @r. We also require that P @ǫ ≡ M ǫ ∈ A ǫ/x .

Computation.
We allow bound dimension names to be used interchangeably and require that all terms obtained by dimension abstraction always lead to certain lines when applied to a certain dimension terms. It is often convenient to express those verbose conditions with the following α-and β-rules:

Uniqueness.
We also endorse an extensional view of identifications, which is to say that we require the following η-rule to hold: It goes without saying that this type has many similarities with the function type (except that it deals with dimension names and the function type variables). It worth noting, however, that this type introduces an heterogeneous approach to equality that is fundamentally different from the homogeneous account found in conventional homotopy type theory. This is because the terms M ∈ A 0/x and N ∈ A 1/x from any identification type M = x.A N need not share the same type, since we have A 0/x ≡ A 1/x in general (but not when A is a degenerate x-type). We shall investigate heterogeneous equality in more details in Section 3.4.

Higher groupoid structure
We begin our account with the central idea of higher type theory, namely, that types can be regarded as (weak) higher groupoids, a category in which all morphisms are isomorphisms up to a higher morphism. When types are regarded as higher groupoids, identifications can be seen as morphisms. This means that we need to define reflexivity, inversion and composition operators for identifications and show that they are well-behaved in a sense that will be explained in Section 3.2.

Homogeneous groupoid operations
We start with the definition of our identity element, the cubical counterpart of the reflexivity identification from conventional homotopy type theory [14]: Proof. By assumption, A is a degenerated x-type, so we have A 0/x ≡ A 1/x . Thus, we have both a ∈ A 0/x and a ∈ A 1/x and the type a = x.A a is wellformed. Because degeneracy allow us to regard a as an x-line from a ∈ A 0/x to a ∈ A 1/x at A (a degenerated line), we simply define refl a :≡ x a. Now that we have a well-defined notion of our identity element we start our cubical constructions with our preliminary definitions of symmetry (inversion) and transitivity (composition) of identifications. Let us first consider the former: Lemma 3.1.2 (Inversion) For every degenerated x-type A and every a ∈ A 0/x and b ∈ A 1/x , there is a function called the inverse function and denoted p → p −1 .
Proof. As before, we have A 0/x ≡ A 1/x . Suppose that y is a dimension term. Degeneracy allows us to regard A as an (x, y)-type and to infer that A 0/y ≡ A 1/y as x-types (since A is an x-type by assumption). Moreover, the types A 0/x 0/y , A 0/x 1/y , A 1/x 0/y , A 1/x 1/y are all strictly equal, so we may use them interchangeably in all contexts.
The idea of the following proof is to observe that, since p ∈ a = x.A b, we have that p@y is a y-line from a ∈ A 0/x 0/y to b ∈ A 0/x 1/y in A, now trivially regarded as an (x, y)-type. Similarly, refl a ∈ a = x.A a gives us a (degenerated) x-line refl a @x from a ∈ A 0/x to a ∈ A 1/x in A and a (degenerated) y-line refl a @y from a ∈ A 0/y to a ∈ A 1/y in A.
Now we note that the left boundaries of p@y and refl a @x are both strictly equal, and that the right boundary refl a @x and the left boundary of refl a @y are both strictly equal as well (all those boundaries are a). In other words, we have an open square whose faces are formed by the lines p@y (right), refl a @x (top) and refl a @y (left). By homogeneous Kan composition, this open square must have a lid (bottom), so we have an x-line from b ∈ A 0/x 1/y to a ∈ A 1/x 1/y in A, as illustrated as the dotted line in the diagram below: Thus, we define p −1 :≡ x hcom 0 1 A (refl a @x)( 0 x ⊲ y.p@y, 1 x ⊲ y.refl a @y).
Recall that since p −1 @x, that is, hcom 0 1 A (refl a @x)( 0 x ⊲ y.p@y, 1 x ⊲ y.refl a @y), represents the homogeneous Kan composition of the diagram depicted above, the (x, y)-square in the diagram above is witnessed by the filler hcom 0 y A (refl a @x)( 0 x ⊲ y.p@y, 1 x ⊲ y.refl a @y).
Because not only Kan compositions but also their corresponding fillers will be extremely relevant to our constructions later on, it is useful to have a special symbolism to talk about them in a more convenient way. This motivates the following notation: if M stands for the Kan composition of an open box, then fill y (M ) will stand for the filler of the Kan composition scenario in the dimension y. For example, in our above proof of Lemma 3.1.2 where p −1 @x refers to the Kan composition of the open box, the filler that witnesses the above (x, y)-square can be denoted by fill y (p −1 @x). Just as we constructed our inversion operation using homogeneous Kan composition, we can define our preliminary notion of composition of identifications in a similar way: Lemma 3.1.3 (Composition) For every degenerated x-type A and every a ∈ A 0/x , b ∈ A 1/x and c ∈ A 1/x , there is a function denoted p → q → p q. We call p q the composition of p and q.
Proof. Once again, we assume that y is a dimension term so that the types A 0/x 0/y , A 0/x 1/y , A 1/x 0/y , A 1/x 1/y are all strictly equal.
Given the identifications p ∈ a = x.A b and q ∈ b = x.A c, we can construct three lines in A: an x-line p@x from a ∈ A 0/x 0/y to b ∈ A 1/x 0/y , a y-line q@y from b ∈ A 1/x 0/y to c ∈ A 1/x 1/y and a (degenerate) y-line refl a @y. It is easy to see that the left boundaries of refl a @y and p@x and that the right boundary of p@x and the left boundary of q@y are all strictly equal. Thus, again, we have an open square, as indicated in the following diagram: a c x y p@x refla@y q@y Since we can construct an x-line from a ∈ A 0/x 1/y to c ∈ A 1/x 1/y by homogeneous Kan composition, the construction gives us the required identification of a and c in A.
We shall try to make our propositions as explicit as possible throughout the remainder of this paper, but, for the sake of readability, we shall often omit labels for degenerated lines when drawing filling diagrams from now on: this information is always irrelevant since the reader should be able to correctly guess the label of any given degenerated line by checking its endpoints. We may also often omit assumptions about dimension terms and treat α-, β-and ηconversions of identifications implicitly (for example, since refl M @r :≡ ( x M )@r always induces a β-conversion, we shall often use the terms refl M @r and M interchangeably without further comment). When proving a proposition we may also generally refer to previous propositions (writing e.g. 'by Lemma X') if we trust that the reader is able to insert the correct instances of it.

Homogeneous groupoid structure
Now that we have a well-defined reflexivity element and inverse and composition operations we need to know if they are well-behaved in the sense that they respect the (weak) higher groupoid structure (up to a higher identification). 3 More specifically, we need to make sure that the reflexivity element is a unit for inversion and composition, that inversion indeed provides inverses and that composition is associative. For now we shall focus on the first claim (the other ones will be made fully precise later).
What does it mean to say that the reflexivity element is a unit for inversion? The higher groupoid structure only holds up to higher identification, so this means that the reflexivity element should equal its inverse up to higher identification. What is the most general non-trivial higher identification in this case? Recall that the reflexivity element can be regarded as a one-dimensional identification, so we can think of this higher identification as a two-dimensional identification that simultaneously identifies two pairs of one-identifications. Given these points, it becomes clear that the answer is in a very particular higher identification that not only identifies the reflexivity element with its inverse but also simultaneously identifies two degenerate lines (which is merely another word for reflexivity).
In this case, this very special sort of identification (henceforth, 'globular identification') can be pictured as an (x, y)-square that has the two particular lines (the reflexivity element and its inverse) identified vertically as x-lines and two degenerate lines on the other two y-sides (intuitively, globular identifications are just generalized lines). Accordingly, the following lemma can be stated as follows: Proof. We construct an (x, y)-square that simultaneously identify refl a @x with refl a −1 @x as x-lines and refl a @y with refl a @y as y-lines. This, however, follows immediately from Lemma 3.1.2, since the filler of the inverse of refl a −1 witnesses the (x, y)-square a a a a x y refla@x fill y (refl a −1 @x) We let iu(a) :≡ y x fill y (refl a −1 @x) be the required identification.
Similarly, composition has no effect on the reflexivity element either, for the reflexivity elements equals the composition of the reflexivity element with itself up to globular identification.

Lemma 3.2.2 (Composition unit)
For every degenerate x-type A and every a ∈ A 0/x , we have an identification cu a ∈ refl a = y.a=x.Aa refl a refl a .
Proof. The proof is straightforward using the filler of the composition of reflexivity refl a with refl a from Lemma 3.1.3.
We now wish to show that the reflexivity element is a right and left unit for composition up to globular identification. Because the proof is simpler for the right unit, we shall consider it first.

Lemma 3.2.3 (Right unit)
For every degenerate x-type A and every a ∈ A 0/x and b ∈ A 1/x we have an identification Proof. We need to construct an identification of p and p refl b in the identification type a = x.A b, or, in other words, an (x, y)-square having p@x and (p refl b )@x as x-lines and refl a @y and refl b @y as degenerate y-lines. But the existence of this square follows from Lemma 3.1.3: The required identification follows by (double) dimension abstraction on the above square.
We still need a few lemmas to show that the left unit property is true too, so we shall postpone it to the end of this section. One very useful proposition that can be proven at this point, however, is that the composition of any identification with its inverse equals the reflexivity element up to globular identification. But the proof is a little more involved than those of the preceding lemmas. So far we have only encountered one-extent Kan composition problems, which means that we have only considered open squares. Even when we were explicitly required to construct a two-dimensional identification (as in Lemmas 3.2.1 to 3.2.3), we were able to found alternative ways to deal with the constructions without having to appeal to higher-dimensional Kan composition scenarios.
It is now time to tackle truly higher-dimensional problems. From now on we will often work with more complex (two-extent) Kan composition scenarios. We start with the following lemma: Lemma 3.2.4 (Right cancellation) For every degenerate x-type A and every a ∈ A 0/x and b ∈ A 1/x we have an identification Proof. We shall construct the required identification by a two-extent homogeneous Kan composition. In the one-dimensional case, it is enough to form an open square to perform a homogeneous Kan composition, while in the twodimensional case we are required to form an open cube. In other words, we are expected to form an open (x, y, z)-cube by finding one (x, z)-square (top), two (z, y)-squares (left and right) and two (x, y)-squares (back and front) whose faces all agree up to strict equality before we can obtain its lid: the composite (x, z)-square that forms the bottom face of the cube.
For this particular lemma this means that we must construct an open cube whose composite is an (x, z)-square with refl a @x and p p −1 @x as x-lines and a in both degenerate z-lines. Now consider the following open (x, y, z)-cube (its composite is illustrated as the shaded face in the diagram below) where refl p ∈ p = y.a=x.Ab p, left and right faces are respectively the (z, y)-squares a a a a z y refl refl a @z@y ≡ a p −1 @y refl p −1 @z@y ≡ p −1 @y p −1 @y and back and front are respectively the (x, y)-squares both of which are given by the fillers of the homogeneous Kan composition scenarios from Lemmas 3.1.2 and 3.1.3, respectively. Now we note that the bottom (x, z)-square of the open cube described above is the homogeneous Kan composite As we shall see in details next section, our inversion and composition operations have a very limited applicability. Recall that both are only well-defined for degenerate one-dimensional types, so we cannot, in general, invert an arbitrary identification α ∈ p = y.r@y=x.As@y q because the y-type r@y = x.A s@y need not be degenerate (in fact, r@y and s@y need not be degenerate lines either). However, it seems natural to expect that α could somehow be 'swapped' into an identification inhabiting the type (q = y.r −1 @y=x.As −1 @y p) as long as A is a degenerate (x, y)-type. This is indeed the case, but requires another proof.
Proof. The idea of the proof is to define a function that maps any (x, y)-square In order to obtain swap α @y@x we perform a two-extent homogeneous Kan composition on the open (x, y, z)-cube formed by p@z at the top, α@y@z at the left, p@z at the right, fill y (r −1 @x) at the back and fill y (s −1 @x) at the front. We thus define swap α by One application of the square swap lemma is in the following proof that a double inverted identification equals the original identification up to globular identification (to put it another way, double inversion is essentially redundant).
(the remaining sides of the open cube will be composed of degenerate squares.) Note that R basically states that the lemma is true when p is refl a , that is to say, it represents the identification refl a = y.a=x.Aa (refl −1 a ) −1 .
We x y to obtain the required (x, y)-square Y . Now that we have R, X and Y , we can define inv p by formed by R at the top, p −1 @y and (p −1 p)@y respectively at the left and right and X and Y respectively at the back and front.
We hope that the reader is starting to get a feel for proofs by Kan composition and the interplay between two-dimensional identifications and squares at this point. Next we want to show that that left cancellation property holds as well (whose right counterpart is Lemma 3.2.4), but for this we will need the following lemma.
Proof. Both proofs use homogeneous Kan composition.
(i) By Lemma 3.1.3 we have an (x, z)-square fill z ((p p −1 )@x) formed from the filler of the composition of p and p −1 . By applying Lemma 3.2.4 to p we obtain an (x, y)-square rc p @y@x. We now construct an open (x, y, z) cube as follows: we put fill z ((p p −1 )@x) at the top (x, z)-square, a and p −1 @z at the left and right (z, y)-squares, respectively, and p@x and the square formed by inversion of rc p , that is, (rc p ) −1 @y@x at the back and front (x, y)-squares, respectively. (ii) This may be verified by a similar argument as above.
We are now able to prove the left cancellation property, which states that the composition of an identification with its inverse equals the reflexivity element up to globular identification. x z y p −1 @x

So our desired identification is
where the (x, y)-square op1 p −1 @y@x is obtained by Lemma 3.2.7 (i).
We are now finally ready to show that the left counterpart of the unit property from Lemma 3.2.3 is the case, or, put differently, that the reflexivity element is a left unit for composition. (fill x (p −1 @z))( 0 x ⊲ y.a, 1 x ⊲ y.op2 p @y@z, 0 z ⊲ y.p@x, 1 z ⊲ y.fill y ((refl a p)@x)), where the (x, z)-square op2 p @y@z is obtained by Lemma 3.2.7 (ii).
The curious reader may wonder why our proof of the left unit property from Lemma 3.2.9 is significantly harder than the right unit one (Lemma 3.2.3). Why the property is so much simpler to demonstrate in the right? If we look attentively at the filler of, say, p q from Lemma 3. we can see that it forms a simultaneous identification: an identification of p@x and p q@x as x-lines modulo an identification of q@y and refl a @y as y-lines. Consequently, if we set q :≡ refl a , then we immediately have a globular identification of p and p q. We can thus compare our composition operation with one defined in conventional homotopy type theory [14] by path induction on the second argument q [14][ §1.12.1], since we let p q be p just in case q is refl a . The same remark applies to inversion as well: in this case p −1 is related to an inversion operation defined by path induction on p by letting p −1 be refl a just in case p is refl a (in fact, we will see in Section 4 that path induction is just a particular case of the Kan conditions.) Last but not least, we want to show that composition of identifications is associative up to globular identification. For this we use the following lemma, which basically states that any two squares with strictly equal top, right and left faces must have the same bottom up to globular identification. Lemma 3.2.10 (The three-out-of-four bottom identification) For every degenerate (x, y)-type A and every α ∈ p = y.r@y=x.As@y q, β ∈ p = y.r@y=x.As@y q ′ we have an identification Proof. By assumption, we have two (x, y)-squares α@y@x and β@y@x with strictly equal top faces p@x, left faces r@y and right faces s@y. We want to show that the bottom faces of α@y@x and β@y@x, which are respectively q@x and q ′ @x, are equal up to globular identification.
We do this by finding an (x, y)-square This open cube is formed by p@x as the top (x, z)-square, r and s as respectively the left and right (z, y)-squares and α@y@x and β@y@x as respectively the back and front (x, y)-squares. Now we can show that associativity holds up to globular identification: Lemma 3.2.11 (Associativity) For every degenerate x-type A and every a ∈ A 0/x , b ∈ A 1/x , c ∈ A 1/x , d ∈ A 1/x , we have an identification assoc p,q,r ∈ (p q) r = y.a=x.Ad p (q r) for any p ∈ a = x.A b, q ∈ b = x.A c, r ∈ c = y.A d.

Heterogeneous groupoid operations
A careful reader will probably wonder why we insisted in describing both the inversion function from Lemma 3.1.2 and the composition function from Lemma 3.1.3 as preliminary (but not definitive) definitions. This is because they share a fundamental limitation: they can only be applied to degenerate types, types that do not depend on the dimension name which is being abstracted in the identification type in consideration. We expressed this limitation explicitly by confining the applicability of our propositions to degenerate x-types whenever we were dealing with an identification type a = x.A b, for this condition guarantees that a = x.A b is a homogeneous identification type (which means that the abstracted dimension name x does not occur in A).
Let us consider the limitations of our preliminary notion of inversion first. Assuming that a = x.A b is a well-formed type, where a ∈ A 0/x and b ∈ A 1/x , in general the type b = x.A a will not be well-formed unless it is also the case that b ∈ A 0/x and a ∈ A 1/x . In other words, the (homogeneous) inversion function from Lemma 3.1.2 fails to be well-defined for every possible well-formed identification type a = x.A b, because its inversion operation needs to be subjected to the condition that both a, b ∈ A 0/x and a, b ∈ A 1/x . To put it simply, inverting in the x direction is an operation that only makes sense when A is a degenerate x-type, that is, when x does not occur in the type A.
Fortunately, there is a way to deal with this problem using type universes. 4 Suppose we are given an x-type A. By dimension abstraction, we have an identification of the types A 0/x and A 1/x in a type universe U with By assumption, the universe U must at least be an x-type too, nevertheless, we require that U be degenerate with respect to x, i.e. U 0/x ≡ U 1/x . Now it can be shown that the following inverse exists: In particular, we have a construction that gives us an x-type ( x A) −1 @x (which we shall often abuse notation and write A −1 ). Intuitively, this type corresponds precisely to the 'inverse' of the x-type A. This is because the − 0/x and − 1/x faces of A −1 are respectively

and (similarly)
which means that we have two inferences that hold top/bottom and bottom/top Under the assumption that a = x.A b is a well-formed type, it is now easy to see that the type b = x.A −1 a will always be well-formed as well regardless of whether A is a degenerate x-type or not: because a = x.A b is well-formed we have a ∈ A 0/x and b ∈ A 1/x , meaning that a ∈ A −1 1/x and b ∈ A −1 0/x must be the case. This motivates the definition of a new (heterogeneous) inversion operation: At this point, one may be tempted to think that we can drop our previous definition of (homogeneous) inverse from Lemma 3.1.2, since we now already possess a more general (heterogeneous) notion of inverse. On second thought, however, it becomes clear that this is not possible on pain of circularity. To put it another way, a preliminary (homogeneous) notion inversion is absolutely necessary in order to define the type A −1 , so that the definition of heterogeneous inversion is not circular.
Just like homogeneous inversion fails to be well-defined for all possible cases, our (homogeneous) composition function suffers from a similar limitation. This can be easily seen in the two-dimensional case where we have identifications of identifications. Consider the two-dimensional identifications α ∈ p = y.p ′ @y=x.Aq ′ @y q and β ∈ q = y.q ′′ @y=x.Ar ′′ @y r which (say) correspond to the following two (x, y)-squares in A: c d e f x y p@x p ′ @y α@y@x q ′ @y q@x q ′′ @y β@y@x r ′′ @y q@x r@x it may seem that we can compose α and β by 'gluing' their common faces together (and composing the other ones) to obtain their composite, as illustrated in the following square: a b e f x y p@x (p ′ q ′′ ) glue α,β @y@x (q ′ r ′′ )@y r@x but this composition is actually ill-defined in general because it need not satisfy two essential requirements of Lemma 3.1.3: first, the target types, p ′ @y = x.A q ′ @y and q ′′ @y = x.A r ′′ @y, must be degenerate y-types; second, those target types must be strictly equal types.
In order to overcome this problem we need a heterogeneous composition operation. Just as with heterogeneous inversion, it be defined with the help of homogeneous composition on types. Once again we assume that A is an x-type so that we can obtain an identification of the types A 0/x and A 1/x in the universe U. We also assume that B is a x-type such that A 1/x ≡ B 0/x and, as before, we require that U be a degenerate x-type. As a result, the following homogeneous composition operation is well-defined: and the composite of x A and x B is the identification which can be seen as the x-type ( x A x B)@x (henceforth written as A B). We also have two important inferences that hold top/bottom and bottom/top, With this we have all we need to define our definitive composition function: written p → q → p * q and called the (heterogeneous) composition function.

Proof. By heterogeneous Kan composition on the open box from Lemma 3.1.3.
Heterogeneous composition does allow us to compose the two-dimensional identifications α and β from our example above, but it is worth noting that the resulting composition is not strictly equal to the operation glue α,β we described (as we shall see in Section 4.3, however, this operation is induced by heterogeneous composition.)

Heterogeneous groupoid structure
In Section 3.2 we showed that types have a higher groupoid structure given in terms of homogeneous inversion and composition. The aim of this subsection is to point out that we can characterize this structure via heterogeneous operations as well. To that end, the propositions from Section 3.2 need some adjustments.
To give an illustration let us examine the inversability property (Lemma 3.2.6), which in the homogeneous case states that for every degenerate x-type A and every a ∈ A 0/x and b ∈ A 1/x the following holds for any identification p ∈ a = x.A b: (p −1 ) −1 = y.a=x.Ab p.
Generalizing inversability to allow for a heterogeneous operation requires us to first drop the restriction that A be a degenerate x-type and then use heterogeneous inversion · −1 * to state something like (p −1 * ) −1 * = y.a= x.?? b p.
At this point, however, we run into a problem: on the left-hand side we have a term of type a = x.(A −1 ) −1 b but, on the right-hand side, we have a term of type a = x.A b. Since, in general, these are not strictly equal x-types, we need to find a way to make sure that the above statement is well-typed. Fortunately, both (A −1 ) −1 and A can be regarded as identifications in a degenerate x-type universe U as we remarked in the previous section, so we can apply homogeneous inversability (Lemma 3.2.6) to obtain a line type from (A −1 ) −1 to A. With this in mind, the heterogeneous inversability property can be stated as follows: The argument is just like the proofs of our heterogeneous generalizations of inversion (Lemma 3.3.1) and composition (Lemma 3.3.2): a straightforward heterogeneous Kan composition on the open cube constructed for the proof of its homogeneous counterpart (Lemma 3.2.6). In fact, all heterogeneous counterparts of the propositions from Section 3.2 follow the same pattern (they can all be stated by using their homogeneous counterparts and proven by a heterogeneous filling of their open cubes), so we will simply omit those results.

General notable properties of identifications
In this section we explore a few notable properties of cubical identifications including path induction, properties of loops and some peculiarities of the groupoid operations applied to identification types.

Path induction
We start with path induction (otherwise known as J), a fundamental property that serves as the elimination rule of the identification type in both standard constructive type theory and conventional homotopy type theory [14, §1.12.1]. Roughly, path induction states that identifications (paths) can be deformed and retracted without changing their essential characteristics.
This can be expressed cubically as follows. Proof. Suppose we are given x ∈ A 1/x , p ∈ a = x.A x and u ∈ P (a, refl a ). The idea of the following proof is to coerce u over a line between the types P (a, refl a ) and P (x, p), so we shall focus on the construction of this type line first. We construct the following (x, y)-square by homogeneous Kan composition a a a x x y is refl p @y@x p@y p@x using the filler from the composites of Lemmas 3.1.3 and 3.2.3 (the argument is similar to the one given in our proof of Lemma 3.2.7 (i)).
Our next step is to observe that is refl p induces an x-line in U P (p@x, is refl p @x) from P (a, refl a ) ∈ U 0/x to P (x, p) ∈ U 0/x (as required), since we have P (p@x, is refl p @x) 0/x ≡ P (p@0, is refl p @0) ≡ P (a, refl a ) and, in a similar fashion, To complete the proof we just need to coerce u ∈ P (a, refl a ) on this line, so gives the required function.
Since the above principle assumes that identifications must always have one of its endpoints predetermined, this property is sometimes regarded as special form of path induction called based path induction in the literature [14][ §1.12.1].

Loops
In conventional homotopy type theory, loops are identifications with the same start and end points (up to strict equality) [14, §2]. This characterization is very convenient because there is no natural way of expressing non-globular (cubical) identifications in conventional homotopy type theory and, consequently, every identification must have exactly two endpoints. Since globular identifications are just a particular sort of cubical identifications, we may view loops as globular identifications with strictly equal endpoints.
Thus, one-dimensional loops are the inhabitants of the type a = x.A a (the loop space of a), as usual [14, §2], but two-dimensional loops, that is, the terms of the type p = y.a=x.Ab p (the loop space of p), are homogeneous degenerate squares and so on. Cubically, the loop space of the loop space of a is represented by the type refl a = y.a=x.Aa refl a just as in conventional homotopy type theory [14, §2.1] and composition of loops is commutative as well: Theorem 4.2.1 (Eckmann-Hilton) Given any degenerate x-type A and term a ∈ A 0/x , the following homogeneous composition is commutative α β = z.a=y.a= x.A a a β α for α, β ∈ refl a = y.a=x.Aa refl a .
Proof. By a cubical simplification of the proof of Theorem 2.1.6 in [14].
Right whiskering is an operation that given a two-dimensional identification α ∈ p = y.a=x.Ab q and a one-dimensional identification r ∈ b = x.A c, returns a term of type p r = y.a=x.Ab q r. In conventional homotopy type theory this is an operation that requires definition [14, §2.1]. Cubically, however, it turns out that right whiskering is just a particular instance of homogeneous composition because degeneration ensures that the composite identification α r will always be a well-formed term, as can be seen below: Naturally, the same holds for left whiskering, which states that for any onedimensional identification p ∈ a = x.A b and two-dimensional identification β ∈ r = y.b=x.Ac s we have an inhabitant of the type p r = y.a=x.Ab p s. It is easy to see by path induction on the abovementioned identifications α, β, p and r that whiskering is commutative, that is, the following is true (α r) (q β) = y.a=x.Ac (p β) (α s).
But now we note that the above proposition already shows that α β = β α always holds when α, β ∈ refl a = y.a=x.Aa refl a because the reflexivity element is both a right and left unit for composition (see Lemmas 3.2.3 and 3.2.9).

Groupoid operations on identification types
We conclude this paper with a few remarks and results about how the groupoid structure holds for identification types (seen not as types but identifications).
How can we view types as identifications? Recall from Section 3.3 that when A is an x-type in a type universe U we have an identification given by the term x A (which to avoid pedantism we simply write as A). Thus, if we consider an identification x-type like p@x = y.A q@x, given the usual assumptions that p ∈ a = x.A 0/y b and q ∈ c = x.A 1/y d and so on (see Theorem 4.3.5 below), then we may see this type as an identification in the universe U between the types In other words, we may view the identification x-type p@x = y.A q@x as an identification of identification types inhabiting the type The moral of the story is that, since identification types may be regarded as identifications, they are also subject to the groupoid operations like all identifications are by default.
In fact, we can show by path induction that inversion can be distributed over the identification type:

(Identification type inversion distribution) Suppose that
A ∈ U is an (x, y)-type and p ∈ a = x.A 0/y b and q ∈ c = x.A 1/y d. We have Proof. The statement of this theorem can be expressed as the expectation of the construction of the following square which we shall call id p,q @y@x. To that end, we proceed by triple path induction.
First we do path induction on A, which allows us to assume that A is refl A (in other words, we can suppose that A is a degenerate (x, y)-type). By induction on p, it suffices to assume that b is a and that p is refl a . Again, by induction on q, it suffices to assume also that d is c and q is refl c .
After all that, the above square reduces to the following: However, recall that the reflexivity element equals its inverse up to globular identification (Lemma 3.2.1), so the term (which we abbreviate by U) iu a @y@x = y.iuA@y@x iu c @y@x is an (x, y)-square since the top (1-2), bottom (3)(4), and left and right (5-6) faces of U are U 0/y ≡ iu a @0@x = y.iuA@0@x iu c @0@x (1) ≡ refl a @x = y.A refl c @x, and Finally, we observe that the top face of U is a degenerate line because (refl a @x = y.A refl c @x) ≡ refl a=y.Ac We complete the proof by letting id p,q be the homogeneous composition of the squares I and U (regarded as identifications).
It is an interesting fact that when (homogeneous) inversion is well-defined for a two-dimensional identification such as α ∈ p = y.r@y=x.As@y q, both the original identification α and its inversion α −1 may be regarded as squares in A. Curiously enough, despite the general applicability of heterogeneous inversion, the same cannot be said for the heterogeneous inversion of α α −1 * ∈ q = y.(r@y=x.As@y) −1 p, which can only be pictured as a line from q to p in the inverted identification type (r@y = x.A s@y) −1 . The reason is clear: after the inversion of an identification type the resulting type stops being an identification type.
Fortunately, because the above theorem tells us that inversion can always be distributed over the identification type, the heterogeneous inversion of any square in A equals a swapped square in A −1 (in the sense of Lemma 3.2.5) up to identification. Corollary 4.3.2 (Heterogeneous square swap) For every (x, y)-type A ∈ U and every p ∈ a = x.A 0/y b, q ∈ c = x.A 1/y d, r ∈ a = y.A 0/x c, s ∈ b = y.A 1/x d, we have Proof. By Theorem 4.3.5 we have an identification between the y-types (r@y = x.A s@y) −1 and r −1 @y = x.A −1 s −1 @y, so p = y.idr,s@x q is an x-line in U from p = y.(r@y=x.As) −1 @y q to p = y.r −1 @y= x.A −1 s −1 @y q.
We can show by path induction that composition can be distributed over the identification type as well. We enunciate this as follows: where a ∈ A 0/x 0/y , b ∈ A 1/x 0/y , c ∈ A 0/x 1/y , d ∈ A 1/x 1/y , e ∈ B 0/x 1/y , f ∈ B 1/x 1/y .
Proof. The proof follows the same idea as the proof of Theorem 4.3.5, so we shall skip the details. We just note that, by path induction, it suffices to find the following square a = y.A 0/x c a = y.A 0/x c a = y.A 0/x c a = y.A 0/x c x y (refla@x =y.A reflc@x) (refla@x =y.A reflc@x)@x ((refla refla)@x =y.A A (reflc reflc)@x)@x which can be easily constructed using Lemma 3.2.2 in a similar way to that of Theorem 4.3.5.
This theorem shows that the gluing operation described in Section 3.3 is closely related to homogeneous composition. Put differently, it shows that the homogeneous composition of two squares induces a gluing operation: Corollary 4.3.4 (Heterogeneous square gluing) Suppose that A, B ∈ U are (x, y)-types such that A 1/y ≡ B 0/y . For every p ∈ a = x.A 0/y b, q ∈ c = x.A 1/y d, r ∈ a = y.A 0/x c, s ∈ b = y.A 1/x d, t ∈ c = y.B 0/x e, u ∈ d = y.B 1/x f , the following holds hglue α ∈ (p = y.(r@y=x.As@y) (t@y=x.B u@y) q) = x.U (p = y.(r t)@y=x.A B (s u)@y q) where a ∈ A 0/x 0/y , b ∈ A 1/x 0/y , c ∈ A 0/x 1/y , d ∈ A 1/x 1/y , e ∈ B 0/x 1/y , f ∈ B 1/x 1/y . Proof. In a manner similar to our proof of Corollary 4.3.2, this can be proven via the identification given by Theorem 4.3.3.
Finally, we note that the distribution of inversion and composition (as in Theorems 4.3.5 and 4.3.3) over the identification type give us a new characterization of the groupoid laws: when identification types are taken as identifications we can characterize the groupoid structure via distribution as follows.
Proof. Routine use of (i) inversability (Lemma 3. In the above corollary the type indexes of the outermost identification type were removed for the sake of brevity (at this point we trust that the reader is able to easily obtain this information by checking the types of the terms involved in the both sides of the expression).

Future work
There is much to be done yet in order to provide a cubical alternative to the informal type theory project of the homotopy type theory book [14]. We view this paper as opening up many possibilities for future work, including informal cubical accounts of the functorality of functions, fibrational aspect of type families, the higher groupoid structure of type formers (including function extensionality and univalence), higher inductive types, homotopy n-types and so on.
Another important area for future work is the mechanization of the proofs presented in this paper using the young proof assistant RedPRL [13]. The type theory of RedPRL contains additional type formers not used in this paper such as line types, which are identification types with arbitrary endpoints. Despite its practical advantages, however, line types have the same expressive power as identification types. Part of the proofs contained in this paper have already been formalized using line types and are available online. 5