depsterr
/
cwfs
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
A literate formalization of categories with families in cubical agda.
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
21 Commits
1 Branch
0 Tags
451 KiB
Tag: Branch: Tree: master
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from 'master'
${ noResults }
Rachel Samuelsson 8d082302f9
change text to better reflect current state 		7 months ago
src change text to better reflect current state 7 months ago
.gitignore Began initial work 8 months ago
README.md update README 8 months ago
cwfs.agda-lib Began initial work 8 months ago

README.md

CwFs

A literate formalization of categories with families in 1Lab cubical agda.

Goals

  • Defining \mathcal Fam
  • 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