An Implementation of Homotopy Type Theory in Isabelle/Pure

TL;DR

This thesis implements a fragment of Homotopy Type Theory within Isabelle/Pure, providing a formal framework and discussing the challenges of encoding dependent type theory with universes in a simple type-theoretic logic.

Contribution

It offers the first implementation of a fragment of HoTT in Isabelle/Pure and analyzes the encoding of intensional dependent type theory with universes.

Findings

Successful implementation of HoTT fragment in Isabelle/Pure

Insights into encoding dependent type theory with universes

Discussion of design decisions and issues in the encoding process

Abstract

In this Masters thesis we present an implementation of a fragment of "book HoTT" as an object logic for the interactive proof assistant Isabelle. We also give a mathematical description of the underlying theory of the Isabelle/Pure logical framework, and discuss various issues and design decisions that arise when attempting to encode intensional dependent type theory with universes inside a simple type-theoretic logical foundation.