A literate formalization of categories with families in cubical agda.
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.
Rachel Samuelsson 8d082302f9 change text to better reflect current state 1 month ago
src change text to better reflect current state 1 month ago
.gitignore Began initial work 2 months ago
README.md update README 2 months ago
cwfs.agda-lib Began initial work 2 months ago

README.md

CwFs

A literate formalization of categories with families in 1Lab cubical agda.

Goals

  • Defining \mathcal Fam
  • Defining CwFs
  • Defining extra structure for CwFs
    • \prod
    • \sum
    • \mathcal U
    • Id
  • Defining categories of various CwFs
    • Is there a good way to define a category of CwFs with arbitrary extra structure?
  • Proving a few basic initiality results

Dependencies

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.

  • 1Lab@504cf7594c9fd7a4afb103d6fce3665cd3d994c3
  • Agda@52467b24fd0670168b2dd8855e9b8d25227e78b9