You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
||1 month ago|
|src||1 month ago|
|.gitignore||2 months ago|
|README.md||2 months ago|
|cwfs.agda-lib||2 months ago|
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.