rachel/cwfs
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

update README

Browse Source
This commit is contained in:
Rachel Lambda Samuelsson 2022-10-08 13:10:55 +02:00
parent a0a1d1a7ed
commit ece686e955
1 changed files with 13 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
README.md
View File

@ -1,14 +1,23 @@
# CwFs
A formalization of CwFs in literate cubical agda using the 1Lab as a library.
A literate formalization of categories with families in 1Lab cubical agda.
# Goals
* Defining CwFs
* Defining type formers for CwFs
* Proving some basic initiality results
- [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`