Skip to content

anuyts/willow

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

92 Commits
 
 
 
 
 
 
 
 

Repository files navigation

willow

Personal agda library. It is called willow because it needed a name.

willow

This is the old version.

basic contains basic type theory stuff.

cat contains category theory.

cat2 is discontinued.

You need to call the repository directory on your computer 'willow' for the directory structure to work. This is so that you can easily refer to it as a library from parallel projects.

willow2

This is the new version.

basic contains basic type theory stuff.

cat contains category theory.

INTENDED IMPROVEMENTS OF willow2 OVER willow:

  • Use of the standard library
  • Use of instance arguments (but are they useful here?)
    • For structure on types: yes
    • For structure on functions: less so
  • Use of irrelevance
  • Level in the record (but currently using type-in-type)

About

Personal agda library

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages