This repository is now archived. Development has moved to https://github.com/jaycech3n/internal-diagrams.
Categories with families in HoTT-Agda, and constructions thereon.
Developed on Agda 2.6.1.3. Depends on Andrew Swan's fork of the HoTT-Agda library.