This repository contains early experiments aiming to rebuild the Slate theorem prover (https://slate-prover.org, https://github.com/SReichelt/slate) on top of a more solid foundation.
For a technical description of what this foundation could look like, see DefinitionalUnivalence.pdf.