Computer Science Speaking Skills Talk

Tuesday, May 7, 2019 - 12:00pm to 1:00pm


McWilliams Classroom 4303 Gates Hillman Centers



Cubical Type Theory and Higher Inductive Types

Cubical type theory is a system for describing mathematical constructions and theorems that takes a novel approach to equality. In this system, a proof that two objects are equal is an algorithm that converts proofs of theorems about one to proofs about the other. This means that proof of an equality is a kind of data---carrying computational content---and in particular, that two objects can be equal in many different ways. Cubical type theory gives a formal justification for the informal mathematical practice of treating isomorphic objects as equal. For example, one can establish an equality between two groups by exhibiting a group isomorphism between them.

With a new notion of equality in place, it also becomes necessary to rethink quotients. In standard mathematics, a group might be presented by a set of generators and equations: it is obtained by starting with the set of generators, closing it under the group operations, and then identifying elements according to the equations. When equalities are data, all of these steps are better thought of as one and the same kind of process: to quotient is to close under equality-producing operations. This intuition is crystallized in the concept of a higher inductive type: an object specified by operations that may generate equalities as well as elements. In this talk, I'll describe my work with Robert Harper on a language for specifying and computing with higher inductive types in cubical type theory.

Presented in Partial Fulfillment of the CSD Speaking Skills Requirement

For More Information, Contact:


Speaking Skills