# Constructive Proofs of Heterogeneous Equalities in Cubical Type Theory

## Abstract

This paper represents the very small part of the developed base library for homotopical prover based on Cubical Type Theory (CTT) announced in 2017. We demonstrate the usage of this library by showing how to build a constructive proof of heterogeneous equality, the simple and elegant formulation of the equality problem, that was impossible to achieve in pure Martin-Löf Type Theory (MLTT). The machinery used in this article unveils the internal aspect of path equalities and isomorphism, used e.g. for proving univalence axiom, that became possible only in CTT. As an example of complex proof that was impossible to construct in earlier theories we took isomorphism between Nat and Fix Maybe datatypes and built a constructive proof of equality between elements of these datatypes. This approach could be extended to any complex isomorphic data types.

## Keywords

Formal methods Type theory Computer languages Theoretical computer science Applied mathematics Isomorphism Heterogeneous equality Cubical Type Theory Martin-Löf Type Theory## 1 Introduction

After formulating Type Theory to model quantifiers using *Pi* and *Sigma* types in 1972 [1] Per Martin-Löf added *Equ* equality types in 1984 [2]. Later *Equ* types were extended to non-trivial structural higher equalities (\(\infty \)-groupoid model) as was shown by Martin Hofmann and Thomas Streicher in 1996 [3]. However formal constructing of Equ type eliminators was made possible only after introducing Cubical Type Theory in 2017 [4]. CTT extends MLTT with interval \(I=[0,1]\) and its de Morgan algebra: \(0, 1, r, -r, min(r,s), max(r,s)\) allowing constructive proofs of earlier models based on groupoid interpretation.

**The Problem and Tools Used.** In this paper, we want to present the constructive formulation of proof that two values of different types are equal using constructive heterogeneous equality in Cubical Type Checker [4]^{1}. In the end, we will use path isomorphism for that purposes [5].

**Author’s Contribution.** During the story of comparing two zeros, we will show the minimal set of primitives needed for performing this task in the cubical type checker. Most of them were impossible to derive in pure MLTT. We show these primitives in dependency order while constructing our proof. This article covers different topics in type theory, which is the main motivation to show how powerful the notion of equality is: (1) Complete Formal Specification of MLTT; (2) Contractability and n-Groupoids; (3) Constructive J; (4) Functional Extensionality; (5) Fibers and Equivalence; (6) Isomorphism; (7) Heterogeneous equality.

### 1.1 Research Formal Description

As a formal description of the research includes all cubical programs as research object, type theory in general and MLTT and CTT in particular as research subject, direct proof construction as logical method and encoded cubical base library and examples as research results.

**Research Object.** The homotopy type theory base libraries in Agda, Cubical, Lean and Coq. While modern Agda has the cubical mode, Coq lacks of the computational semantics of path primitives while has HoTT library. The real programming language is not enough to develop the software and theorems, the language should be shipped with base library. In this article we unveil the practical implementation of base library for cubical type checkers.

**Research Subject.** We will analyze the base library through the needs of particular features, like basic theorems, heterogeneous path equalities, univalence, basic HITs like truncations, run-time versions of the list, nat, and stream datatypes. We use Martin-Löf Type Theory as a subject and its extension CTT. The main motivation is to have small and concise base library for cubicaltt type checker than can be used in more complex proofs. As an example of library usage we will show the general sketch of the constructive proofs of heterogeneous equality in CTT, concentrating only on homotopical features of CTT.

**Research Results.**Research result is presented as source code repository that can be used by cubicaltt

^{2}language and contains the minimal base library used in this article. These primitives form a valuable part of base library, so this article could be considered as an brief introduction to several modules:

**proto_path**,

**proto_equiv**,

**pi**,

**sigma**,

**mltt**,

**path**,

**iso**. But the library has even more modules, that exceed the scope of this article so you may refer to source code repository

^{3}. Brief list of base library modules is given in Conclusion.

**Research Methods.** The formal definition of MLTT theory and constructive implementation of its instance that supplied with minimal but comprehensive base library that can be used for verifying homotopical and run-time models. The type theory itself is a modeling language, logical framework and research method. The MLTT is a particular type theory with *Universes*, \(\varPi \), \(\varSigma \) and *Equ* types. This is common denominator for a series of provers based on MLTT such as Coq, Agda, Cubicaltt, Idris. In the article we will use Cubical language (Fig. 1).

## 2 MLTT Type Theory

MLTT is considered as contemporary common math modeling language for different parts of mathematics. Thanks to Vladimir Voevodsky this was extended to Homotopy Theory using MLTT-based Coq proof assistant^{4}. Also he formulated the univalence principle \(Iso(A,B)=(A=B)\) [5], however constructive proof that isomorphism equals to equality and equivalences is possible only in Cubical Type Theory [4] (Agda and Cubical type checkers).

In this section we will briefly describe the basic notion of MLTT, then will give a formal description of MLTT and the informal primitives of CTT. Only after that will start the proof of heterogeneous equality ended up with proof term. MLTT consist of \(\varPi \), \(\varSigma \) and *Equ* types living in a Hierarchy of universes \(U_i : U_{i+1}\). We will also give an extended equality *HeteroEqu* which is needed for our proof.

### 2.1 Syntax Notes

*a*:

*A*and there is definitional equality which is usually built into type checker and compare normal forms.

*Pi*and

*Sigma*types was formulated using natural deduction inference rules as a language. The inference rules in that language will be translated to cubicaltt in our article.

*U*:

*U*but this won’t affect correctness of our proof). Here we consider \(\varPi \) and

*Pi*synonimically identical.

According to MLTT each type has 4 sorts of inference rules: Formation, Introduction, Eliminators and Computational rules. Formation rules are formal definition of spaces while introduction rules are methods how to create points in these spaces. Introduction rules increase term size, while eliminators reduce term size. Computational rules always formulated as equations that represents reduction rules, or operational semantics.

### 2.2 Pi Types

*Pi*types represent spaces of dependent functions. With

*Pi*type we have one lambda constructor and one application eliminator. When

*B*is not dependent on

*x*:

*A*the

*Pi*is just a non-dependent total function \(A \rightarrow B\).

*Pi*has one lambda function constructor, and its eliminator, the application [1, 2, 3, 4, 5, 6].

*Pi*and its eliminators in cubical syntax as Pi. Note that backslash ‘\’ in cubical syntax means \(\lambda \) function from math notation and has compatible lambda signature.

### 2.3 Sigma Types

*Sigma*types represents a dependent Cartesian products. With sigma type we have pair constructor and two eliminators, its first and second projections. When

*B*is not dependent on

*x*:

*A*the

*Sigma*is just a non-dependent product \(A \times B\).

*Sigma*has one pair constructor and two eliminators, its projections [1, 2, 3, 4, 5, 6].

*Pi*and

*Sigma*are dual the

*Sigma*type could be formulated in terms of

*Pi*type using Church encoding, thus

*Sigma*is optional. The type systems which contains only

*Pi*types called Pure or PTS. Here we rewrite the math formula of

*Sigma*and its eliminators in cubical syntax as Sigma:

### 2.4 Equ Types

*Equ*type. [2] However unlike

*Pi*and

*Sigma*the eliminator J of

*Equ*type is not derivable in MLTT [3, 4, 5].

*Equ*in cubical syntax as Equ:

*Equ*type. And also this is crucial to our main task, constructive comparison of two values of different types. We leave the definition blank until introduce cubical primitives, here is just MLTT signature of HeteroEqu which is underivable in MLTT.

### 2.5 Complete Formal Specification of MLTT

MLTT needn’t and hasn’t the underlying logic, the Logical Framework could be constructed directly in MLTT. According to Brouwer-Heyting-Kolmogorov interpretation the propositions are types, Pi is an universal quantifier, Sigma is existential quantifier. Implication is given by Pi over types, conjunction is Cartesian product of tpes and disjunction is disjoint sum of types.

*HeteroEqu*needed to formulation of computational rule \(Id\_Comp\) of

*Equ*type. Presheaf model of Type Theory, specifically Cubical Sets with interval [0, 1] and its algebra was introduced to solve derivability issues. So the instance of MLTT is packed with all the type inference rules along with operational semantics:

## 3 Preliminaries

### 3.1 Cubical Type Theory Primitives and Syntax

The path equality is modeled as an interval [0, 1] with its de Morgan algebra 0, 1, *r*, \(\min (r,s)\), \(\max (r,s)\). According to underlying theory it has lambdas, application, composition and gluening of [0, 1] interval and Min and Max functions over interval arguments. This is enough to formulate and prove path isomorphism and heterogeneous equality.

**Heterogeneous Path.** The HeteroPath formation rule defines a heterogeneous path between elements of two types A and B for which Path exists A = B.

**Abstraction Over [0, 1].** Path lambda abstraction is a function which is defined on [0, 1]: \(f: [0,1] \rightarrow A\). Path lambda abstraction is an element of Path type.

**Min, Max and Invert.** In the body of lambda abstraction besides path application de Morgan operation also could be used: \(i \wedge j\), \(i \vee j\), *i*, \(-i\) and constants 0 and 1.

**Application of Path to Element of [0, 1].** When path lambda is defined, the path term in the body of the function could be reduced using lambda parameter applied to path term.

**Path Composition.** The composition operation states that being extensible is preserved along paths: if a path is extensible at 0, then it is extensible at 1.

**Path Gluening.** The path gluening is an operation that allows to build path from equivalences. CTT distinguishes types gluening, value gluening and ungluening.

^{5}. It has only 5 keywords:

**data**,

**split**,

**where**,

**module**, and

**import**.

### 3.2 Contractability and Higher Equalities

*A*is contractible, or a singleton, if there is

*a*:

*A*, called the center of contraction, such that \(a = x\) for all

*x*:

*A*: A type

*A*is proposition if any

*x*,

*y*:

*A*are equals. A type is a Set if all equalities in

*A*form a prop. It is defined as recursive definition.

**path**module. As you can see from definition there is a recurrent pattern which we encode in cubical syntax as follows:

### 3.3 Constructive J

*PathP*and constructive implementation of reflection rule as lambda over interval [0, 1] that return constant value

*a*on all domain.

These function are defined in **proto_path** module, and all of them except singleton definition are underivable in MLTT.

### 3.4 Functional Extensionality

*funExt*as functional property is placed in

**pi**module.

### 3.5 Fibers and Equivalence

*y*:

*B*is family over x of Sigma pair containing the point

*x*and proof that \(f(x)=_B y\).

*equiv* type is compatible with cubicaltt type checker and it instance can be passed as parameter for Glue operation. So all *equiv* functions and properties is placed in separate **equiv** module.

### 3.6 Isomorphism

*lemIso*proof is a bit longread, you may refer to Github repository

^{6}. The by proof of

*isoToEquiv*using

*lemIso*we define

*isoToPath*as Glue of A and B types, providing

*equiv*(

*A*,

*B*). Glue operation first appear in proving transport values of different type across their path equalities which are being constructed using encode and decode functions that represent isomorphism. Also Glue operation appears in constructive implementation of Univalence axiom [4].

Isomorphism definitions are placed in three different modules due to dependency optimization: **iso**, **iso_pi**, **iso_sigma**. Latter two contains main theorems about paths in Pi and Sigma spaces.

## 4 The Formal Specification of the Problem

### 4.1 Class of Theorems. Constructive Proofs of Heterogeneous Equalities

Speaking of core features of CTT that were unavailable in MLTT is a notion of heterogeneous equality that was several attempts to construct heterogeneous equalities: such as John-Major Equality^{7} by Connor McBride (which is included in Coq base library). As an example of library usage we will show the general sketch of the constructive proofs of heterogeneous equality in CTT, concentrating only on homotopical features of CTT.

Let us have two types *A* and *B*. And we have some theorems proved for *A* and functions \(f: A \rightarrow B\) and \(g: B \rightarrow A\) such that \(f \circ g = id_A\) and \(g \circ f = id_B\). Then we can prove \(Iso(A,B) \rightarrow Equ(A,B)\). The result values would be proof that elements of *A* and *B* are equal—*HeteroEqu*. We will go from the primitives to the final proof. As an example we took Nat and Fix Maybe datatype and will prove *Iso*(*Nat*, *Fix*(*Maybe*)). And then we prove the *HeteroEqu*(*Nat*, *Fix*(*Maybe*)).

### 4.2 Problem Example. Nat = Fix Maybe

*Iso*(

*Nat*,

*Fix*(

*Maybe*)) and \(Nat =_U Fix(Maybe)\). First we need to introduce datatypes

*Nat*,

*Fix*,

*Maybe*and then write encode and decode functions to build up an isomorphism. Then by using conversion from

*Iso*to

*Path*we get the heterogeneous equality of values in

*Nat*and

*Fix*(

*Maybe*). We can build transport between any isomorphic data types by providing ecode and decode functions.

## 5 Conclusion

At the moment only two provers that support CTT exists, this is Agda [6] and Cubical [4]. We developed a base library for cubical type checkers and described the approach of how to deal with heterogeneous equalities by the example of proving \(Nat =_U Fix(Maybe)\).

Homotopical core in the prover is essential for proving math theorems in geometry, topology, category theory, homotopy theory. But it also useful for proving with fewer efforts even simple theorems like commutativity of Nat. By pattern matching on the edges to can specify continuous (homotopical) transformations of types and values across paths.

We propose a general-purpose base library for modeling math systems using univalent foundations and cubical type checker.

**MLTT Foundation**: the set of modules with axioms and theorems for Pi, Sigma and Path types, the basis of MLTT theory. Among them: pi, sigma, proto, proto_equiv, proto_path, path, function, mltt. **Univalence Foundation**: the basic theorems about isomorphisms of MLTT types. Useful for proving transport between types, include following modules: iso, iso_pi, iso_sigma, trunc, equiv, univ. **Category Theory**: the model of Category Theory following [5] definitions. It includes: cat, pushout, fun, grothendieck. **Runtime Types**: the models for run-time systems, properties of which could be proved using univalend foundations: binnat, bool, control, either, list, maybe, stream, nat, recursion, cwf, lambek. **Set Theory**: The basic theorems about set theory and higher groupoids: hedberg, girard, prop, set. **Geometry**: Higher Inductive Types: circle, helix, quotient, retract, etc. **Algebra**: Abstract algebra, such as Monoid, Gropop, Semogroupo, Monad, etc: algebra, control.

The amount of code needed for \(Nat =_U Fix(Maybe)\) proof is around 400 LOC in modules (Fig. 2).

The further development of base library implies: (1) extending run-time facilities; (2) making it useful for building long-running systems and processes; (3) implement the inductive-recursive model for inductive types (development of lambek module). The main aim is to bring homotopical univalent foundations for run-time systems and models. Our base library could be used as a first-class mathematical modeling tool or as a sandbox for developing run-time systems and proving its properties, followed with code extraction to pure type systems and/or run-time interpreters.

## Footnotes

## References

- 1.Martin-Löf, P., Sambin, G.: The theory of types. Studies in proof theory (1972)Google Scholar
- 2.Martin-Löf, P., Sambin, G.: Intuitionistic type theory. Studies in proof theory (1984)Google Scholar
- 3.Hofmann, M., Streicher, T.: The groupoid interpretation of type theory. In: In Venice Festschrift, pp. 83–111. Oxford University Press (1996)Google Scholar
- 4.Cohen, C., Coquand, T., Huber, S., Mörtberg, A.: Cubical type theory: a constructive interpretation of the univalence axiom (2017)Google Scholar
- 5.The Univalent Foundations Program: Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study (2013)Google Scholar
- 6.Bove, A., Dybjer, P., Norell, U.: A brief overview of agda—a functional language with dependent types. In: Proceedings of the 22-nd International Conference on Theorem Proving in Higher Order Logics, pp. 73–78. Springer-Verlag (2009)Google Scholar
- 7.Bishop, E.: Foundations of Constructive Analysis. McGraw-Hill Series in Higher Mathematics. McGraw-Hill, New York City (1967)Google Scholar