8 citations · 8 across the 4 of their papers we have counts for
4 papers
2-Coherent Internal Models of Homotopical Type Theory
Joshua Chen
The program of internal type theory seeks to develop the categorical model theory of dependent type theory using the language of dependent type theory itself. In the present work w…
Homotopy Type Theory in Isabelle
Joshua Chen
This paper introduces Isabelle/HoTT, the first development of homotopy type theory in the Isabelle proof assistant. Building on earlier work by Paulson, I use Isabelle's existing l…
An Implementation of Homotopy Type Theory in Isabelle/Pure
Joshua Chen
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 descri…
The Temperley-Lieb categories and skein modules
Joshua Chen
We develop the theory of diagrammatic Temperley-Lieb categories in order to construct examples of spherical fusion categories, which we then use to construct Turaev-Viro skein modu…