23 lines
658 B
Markdown
23 lines
658 B
Markdown
# 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` |