CwFs
A formalization of CwFs in literate cubical agda using the 1Lab as a
library.
Goals
- Defining CwFs
- Defining type formers for CwFs
- Proving some basic initiality results
Dependencies
1Lab@504cf7594c9fd7a4afb103d6fce3665cd3d994c3Agda@52467b24fd0670168b2dd8855e9b8d25227e78b9