Advertisement

Constructive Proofs of Heterogeneous Equalities in Cubical Type Theory

  • Maksym Sokhatskyi
  • Pavlo Maslianko
Conference paper
Part of the Advances in Intelligent Systems and Computing book series (AISC, volume 836)

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 cubicaltt2 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 repository3. Brief list of base library modules is given in Conclusion.
Fig. 1.

Base library and its dependencies used in article

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 assistant4. 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

Types are the analogues of sets in ZFC, or objects in topos theory, or spaces in analysis. Types contains elements, or points, or inhabitants and it’s denoted a : A and there is definitional equality which is usually built into type checker and compare normal forms.
$$\begin{aligned} \qquad \qquad \qquad \qquad \qquad \qquad a : A\qquad \qquad \qquad \qquad \qquad \qquad \,\,\, \text {(terms and types)} \end{aligned}$$
$$\begin{aligned} \qquad \qquad \qquad \qquad x = [ y : A ]\qquad \qquad \qquad \qquad \qquad \qquad \,\,\, \text {(definitional equality)} \end{aligned}$$
MLTT type theory with 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.
$$\begin{aligned} \qquad \qquad \qquad \dfrac{(A: U_i)\ (B: A \rightarrow U_j)}{(x: A) \rightarrow B(x): U_{max(i,j)}}\qquad \qquad \qquad \qquad \,\,\, \text {(natural deduction)} \end{aligned}$$
Equivalent definition in cubicaltt (which is inconstend U : U but this won’t affect correctness of our proof). Here we consider \(\varPi \) and Pi synonimically identical.
$$\begin{aligned} \qquad \qquad Pi\ (A: U)\ (B: A \rightarrow U): U = (x: A) \rightarrow B(x)\qquad \qquad \qquad \,\, \text {(cubicaltt)} \end{aligned}$$
In article we will use the latter notation, the cubical syntax. The function name in cubical syntax is an inference rule name, everything from name to semicolon is context conditions, and after semicolon is a new construction derived from context conditions. From semicolon to equality sign we have type and after equ sign we have the term of that type. If the types are treated as spaces then terms are points in these spaces.

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].
$$\begin{aligned} Pi(A,B) = \prod _{x:A} B(x) : U,\ \ \ \lambda x . b : \prod _{x:A} B(x) \end{aligned}$$
$$\begin{aligned} \prod _{f:\prod _{x:A}B(x)}\prod _{a:A} f a : B (a) \end{aligned}$$
Here we formulate the math formula of 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].
$$\begin{aligned} Sigma(A,B) = \sum _{x:A} B(x) : U,\ \ \ (a,b) : \sum _{x:A} B(x) \end{aligned}$$
$$\begin{aligned} \pi _1 : \prod _{f:\sum _{x:A}B(x)}A\ ,\ \ \ \pi _2 : \prod _{f:\sum _{x:A}B(x)}B(\pi _1(f)) \end{aligned}$$
As 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

For modeling propositional equality later in 1984 was introduced Equ type. [2] However unlike Pi and Sigma the eliminator J of Equ type is not derivable in MLTT [3, 4, 5].
$$\begin{aligned} Equ(x,y) = \prod _{x,y:A} x =_A y : U,\ \ \ reflect : \prod _{a:A} a =_A a \end{aligned}$$
$$\begin{aligned} D : \prod _{x,y:A}^{A:U_i} x =_A y \rightarrow U_{i+1},\ \ \ J : \prod _{C: D} \prod _{x:A} C(x,x,reflect(x)) \rightarrow \prod _{y:A} \prod _{p:x=_A y} C(x,y,p) \end{aligned}$$
Eliminator of Equality has complex form and underivable in MLTT. Here we can see the formulation of Equ in cubical syntax as Equ:
Starting from MLTT until cubicaltt there was no computational semantics for J rules and in Agda and Coq it was formulated using inductive data types wrapper around built-in primitives (J) in the core:
Heterogeneous equality is needed for computational rule of 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.
E.g. we can define Setoid specification [7] as not-MLTT basis for equality types. These signatures are also underivable in MLTT.
$$\begin{aligned} symm : \prod _{a,b:A} \prod _{p:a =_A b} b =_A a,\ \ \ transitivity : \prod _{a,b,c: A} \prod _{p: a =_A b} \prod _{q: b =_A c} a =_A c \end{aligned}$$

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.

So we can build LF for MLTT inside MLTT. Specification could be formulated as a single Sigma chain holding the computation system and its theorems in one package. Carrying object along with its properties called type refinement, so this type represents a refined MLTT:
Even more complex challenges on Equ type was introduced such as heterogeneous equality 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.

Here we give LALR specification of BNF notation of Cubicat Syntax as implemented in our Github repository5. It has only 5 keywords: data, split, where, module, and import.

3.2 Contractability and Higher Equalities

A type 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 xy : A are equals. A type is a Set if all equalities in A form a prop. It is defined as recursive definition.
$$\begin{aligned} isContr = \sum _{a:A}\prod _{x:A} a =_A x,\ \ isProp(A) = \prod _{x,y:A} x =_A y,\ \ isSet = \prod _{x,y:A} isProp\ (x =_A y),\ \ \end{aligned}$$
$$\begin{aligned} isGroupoid = \prod _{x,y:A} isSet\ (x =_A y),\ \ PROP = \sum _{X:U}isProp(X),\ \ SET = \sum _{X:U}isSet(X),... \end{aligned}$$
The following types are inhabited: isSet PROP, isGroupoid SET. All these functions are defined in 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

The very basic ground of type checker is heterogeneous equality PathP and constructive implementation of reflection rule as lambda over interval [0, 1] that return constant value a on all domain.
$$\begin{aligned} trans : \prod _{p:A=_U B}^{A,B:U} \prod _{a:A} B,\ \ \ singleton : \prod _{x:A}^{A:U} \sum _{y:A} x =_A y \end{aligned}$$
$$\begin{aligned} subst : \prod _{a,b:A}^{A:U,B:A\rightarrow U} \prod _{p: a =_A b} \prod _{e:B(a)} B(b), \ \ \ congruence : \prod _{f:A\rightarrow B}^{A,B:U} \prod _{a,b:A} \prod _{p:a =_A b} f(a) =_B f(b) \end{aligned}$$
Transport transfers the element of type to another by given path equality of the types. Substitution is like transport but for dependent functions values: by given dependent function and path equality of points in the function domain we can replace the value of dependent function in one point with value in the second point. Congruence states that for a given function and for any two points in the function domain, that are connected, we can state that function values in that points are equal.
Then we can derive J using contrSingl and subst as defined in HoTT [5]:

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

3.4 Functional Extensionality

Function extensionality is another example of underivable theorems in MLTT, it states if two functions with the same type and they always equals for any point from domain, we can prove that these function are equal. funExt as functional property is placed in pi module.
$$\begin{aligned} funExt: \prod _{[f,g: (x:A) \rightarrow B(x)]}^{A: U,B:A\rightarrow U}\prod _{[x:A,p:A\rightarrow f(x) =_{B(x)} g(x)]} f =_{A\rightarrow B(x)} g \end{aligned}$$

3.5 Fibers and Equivalence

The fiber of a map \(f : A \rightarrow B\) over a point y : B is family over x of Sigma pair containing the point x and proof that \(f(x)=_B y\).
$$\begin{aligned} fiber : \prod _{f:A->B}^{A,B:U}\prod _{x:A,y:B}\sum f(x) =_B y,\ \ \ isEquiv : \prod _{f:A->B}^{A,B:U}\prod _{y:B} isContr(fiber(f,y)) \end{aligned}$$
$$\begin{aligned} equiv : \sum _{f:A->B}^{A,B:U} isEquiv(f) \ \ \ pathToEquiv: \prod _{p: X =_U Y}^{X,Y:U} equiv_U(X,Y) \end{aligned}$$
.
Contractability of fibers called is Equiv predicate. The Sigma pair of a function and that predicate called equivalence, or equiv. Now we can prove that singletons are contractible and write a conversion function \(X=_U Y \rightarrow equiv(X,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

The general idea to build path between values of different type is first to build isomorphism between types, defined as decode and encode functions (f and g), such that \(f \circ g = id_A, g \circ f = id_B\).
$$\begin{aligned} Iso(A,B) = \sum _{[f:A\rightarrow B]}\sum _{[g:B\rightarrow A]}\Biggl ( \prod _{x:A} [ g(f(x)) =_A x ] \times \prod _{y:B} [ f(g(y) =_B y ] \Biggr ) \end{aligned}$$
$$\begin{aligned} isoToEquiv(A,B) : Iso(A,B) \rightarrow Equiv(A,B) \end{aligned}$$
$$\begin{aligned} isoToPath(A,B) : Iso(A,B) \rightarrow A =_U B \end{aligned}$$
lemIso proof is a bit longread, you may refer to Github repository6. The by proof of isoToEquiv using lemIso we define isoToPath as Glue of A and B types, providing equiv(AB). 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 Equality7 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(NatFix(Maybe)). And then we prove the HeteroEqu(NatFix(Maybe)).

4.2 Problem Example. Nat = Fix Maybe

Now we can prove Iso(NatFix(Maybe)) and \(Nat =_U Fix(Maybe)\). First we need to introduce datatypes NatFixMaybe 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.
The result term of equality between two zeros of Nat and Fix Maybe is given by isomorphism.
We admit that normalized (expanded) term has the size of one printed page. Inside it contains the encode and decode functions and identity proofs about their composition. So we can reconstruct everything up to homotopical primitives or replace the isomorphic encoding with arbitrary code.
Fig. 2.

Full base library dependencies

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. 1.
    Martin-Löf, P., Sambin, G.: The theory of types. Studies in proof theory (1972)Google Scholar
  2. 2.
    Martin-Löf, P., Sambin, G.: Intuitionistic type theory. Studies in proof theory (1984)Google Scholar
  3. 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. 4.
    Cohen, C., Coquand, T., Huber, S., Mörtberg, A.: Cubical type theory: a constructive interpretation of the univalence axiom (2017)Google Scholar
  5. 5.
    The Univalent Foundations Program: Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study (2013)Google Scholar
  6. 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. 7.
    Bishop, E.: Foundations of Constructive Analysis. McGraw-Hill Series in Higher Mathematics. McGraw-Hill, New York City (1967)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Igor Sikorsky Kyiv Polytechnical InstituteKyivUkraine

Personalised recommendations