# Author Archives: Dan Licata

## Abstract Types with Isomorphic Types

Here’s a cute little example of programming in HoTT that I worked out for a recent talk. Abstract Types One of the main ideas used to structure large programs is abstract types. You give a specification for a component, and … Continue reading

## A Simpler Proof that π₁(S¹) is Z

Last year, Mike Shulman proved that π₁(S¹) is Z in Homotopy Type Theory. While trying to understand Mike’s proof, I came up with a simplification that shortens the proof a bunch (100 lines of Agda as compared to 380 lines … Continue reading

## Canonicity for 2-Dimensional Type Theory

A consequence of the univalence axiom is that isomorphic types are equivalent (propositionally equal), and therefore interchangable in any context (by the identity eliminaiton rule J). Type isomorphisms arise frequently in dependently typed programming, where types are often refined to … Continue reading

## Running Circles Around (In) Your Proof Assistant; or, Quotients that Compute

Higher-dimensional inductive types are an idea that many people have been kicking around lately; for example, in An Interval Type Implies Function Extensionality. The basic idea is that you define a type by specifying both what it’s elements are (as … Continue reading

## Just Kidding: Understanding Identity Elimination in Homotopy Type Theory

Several current proof assistants, such as Agda and Epigram, provide uniqueness of identity proofs (UIP): any two proofs of the same propositional equality are themselves propositionally equal. Homotopy type theory generalizes this picture to account for higher-dimensional types, where UIP … Continue reading

## A Formal Proof that the Higher Fundamental Groups are Abelian

Homotopy type theory (HoTT) will have applications for both computer science and math. On the computer science side, applications include using homotopy type theory’s more general notion of equality to make formal verification of software easier. On the mathematical side, … Continue reading