From ece686e955c882280a961568f5e7dfbc3b4dd5de Mon Sep 17 00:00:00 2001
From: depsterr <depsterr@protonmail.com>
Date: Sat, 8 Oct 2022 13:10:55 +0200
Subject: [PATCH] update README

---
 README.md | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

diff --git a/README.md b/README.md
index 02edcad..7e655aa 100644
--- a/README.md
+++ b/README.md
@@ -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`
\ No newline at end of file