A literate formalization of categories with families in cubical agda.
Go to file
Rachel Lambda Samuelsson 8d082302f9 change text to better reflect current state 2022-10-28 16:23:22 +02:00
src change text to better reflect current state 2022-10-28 16:23:22 +02:00
.gitignore Began initial work 2022-10-06 00:05:15 +02:00
README.md update README 2022-10-08 13:10:55 +02:00
cwfs.agda-lib Began initial work 2022-10-06 00:05:15 +02:00

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 Ive listed the commits used for both the 1Lab and Agda.

  • 1Lab@504cf7594c9fd7a4afb103d6fce3665cd3d994c3
  • Agda@52467b24fd0670168b2dd8855e9b8d25227e78b9