This repository contains a highly experimental implementation of finite-dimensional type theory, presented at HoTT/UF 2020: https://hott-uf.github.io/2020/HoTTUF_2020_paper_11.pdf
The implementation makes use the construction of type theory inside type theory by Altenkirch and Kaposi, 2016.
The core rules can be found in 'FTT/Core.agda'.
Definitional equalities are, where possible, proved by the rewrite pragma of Agda. Where this is not possible, we often resort to postulates. These postulates are mostly evident, but laborious to prove.
Some admissible rules in FTT, such as uniqueness of identity proofs, and a formalization of semi-simplicial types (which is still in progress) can be found in 'Examples'.