2022-10-06 11:31:00 +02:00
|
|
|
# CwFs
|
|
|
|
|
|
2022-10-06 20:45:47 +02:00
|
|
|
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
|
2022-10-06 11:31:00 +02:00
|
|
|
|
|
|
|
|
# Dependencies
|
|
|
|
|
|
|
|
|
|
* `1Lab@504cf7594c9fd7a4afb103d6fce3665cd3d994c3`
|
|
|
|
|
* `Agda@52467b24fd0670168b2dd8855e9b8d25227e78b9`
|
