|Rachel Lambda Samuelsson 8d082302f9|
A literate formalization of categories with families in 1Lab cubical agda.
- Defining \mathcal Fam
- Defining CwFs
- Defining extra structure for
- \mathcal U
- Defining categories of various
- Is there a good way to define a category of CwFs with arbitrary extra structure?
- Proving a few basic initiality results
The 1Lab can be a bit stingy with which Agda version to use, so I’ve listed the commits used for both the 1Lab and Agda.