An experimental implementation of homotopy type theory in the interactive proof assistant Isabelle
Branch: master
Clone or download
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
ex add ROOT file Sep 18, 2018
tests Overhaul of the theory presentations. New methods in HoTT_Methods.thy… Sep 18, 2018
.gitignore .gitignore Aug 18, 2018
Coprod.thy Not sure what advantage is provided by having eta-expanded forms in t… Sep 19, 2018
Empty.thy
Equal.thy Partway through associativity proof. Lots to work on to make this mor… Feb 18, 2019
Equality.thy Derive can prove pathcomp_comp. Fix typo. Sep 20, 2018
HoTT.thy Renaming Sep 19, 2018
HoTT_Base.thy Method "quantify" converts product inhabitation into Pure universal s… Feb 17, 2019
HoTT_Methods.thy Method "quantify" converts product inhabitation into Pure universal s… Feb 17, 2019
HoTT_Typing.thy Put typing functionality into a .thy and clean up antiquotations, whi… Feb 11, 2019
LICENSE Rename LICENSE.md to LICENSE Aug 21, 2018
Nat.thy
Prod.thy finalize quantify methods Feb 17, 2019
Projections.thy Method "quantify" converts product inhabitation into Pure universal s… Feb 17, 2019
README.md Update README.md Sep 20, 2018
ROOT 1. Change syntax to rely less on unicode/control symbols. Feb 4, 2019
Sum.thy Method "quantify" converts product inhabitation into Pure universal s… Feb 17, 2019
Unit.thy Overhaul of the theory presentations. New methods in HoTT_Methods.thy… Sep 18, 2018
Univalence.thy Renaming Sep 19, 2018
util.ML Put typing functionality into a .thy and clean up antiquotations, whi… Feb 11, 2019

README.md

Isabelle/HoTT

An experimental implementation of homotopy type theory in the interactive theorem prover Isabelle.

Usage

The default entry point for the logic is HoTT, which loads everything else.

You can also load theories selectively, in this case,HoTT_Base is required and HoTT_Methods is helpful.

License

GNU LGPLv3