658 B

Raw Permalink Blame History

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