Feb 2021: This project has been merged into Isabelle/HoTT and development here will cease.
Dependent type theory for Isabelle.
A minimal intensional dependent type theory object logic for Isabelle, supporting univalence and book HoTT. This project aims to improve upon Isabelle/HoTT, and will eventually be merged into that codebase.
An initial system description is available here: Isabelle/Spartan — A Dependent Type Theory Framework for Isabelle