# CwFs

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

# Goals

- [x] Defining $\mathcal Fam$
- [x] 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`