Awesome

Generalized Cartesian Cubical Type Theory

Agda code for a Cartesian cubical set model of univalent type theory based on a weakened version of ABCFHL fibrations. This generalizes the construction in https://github.com/dlicata335/cart-cube and https://github.com/IanOrton/cubical-topos-experiments/.

This code is based on the formalization accompanying Ian Orton's Ph.D. thesis which can be found at: https://www.repository.cam.ac.uk/handle/1810/288558. We are grateful for Ian's permission to use his code.