diff --git a/README.md b/README.md index d29ecc9..02edcad 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,12 @@ # CwFs -A formalization of CwFs in cubical agda using the 1Lab as a library. +A formalization of CwFs in literate cubical agda using the 1Lab as a library. + +# Goals + +* Defining CwFs +* Defining type formers for CwFs +* Proving some basic initiality results # Dependencies