23 lines
469 B
Markdown
23 lines
469 B
Markdown
|
Remove stuff about models of type theory
|
||
|
|
|
||
|
|
Add references to specific (noteable) implementaitons of category theory:
|
||
|
|
* Unimath
|
||
|
|
* cubicaltt
|
||
|
|
* https://github.com/pcapriotti/agda-categories
|
||
|
|
* https://github.com/copumpkin/categories
|
||
|
|
* ...
|
||
|
|
|
||
|
|
Talk about structure of library:
|
||
|
|
===
|
||
|
|
|
||
|
|
Propositional- and non-propositional stuff split up
|
||
|
|
Providing "equiality principles"
|
||
|
|
Provide overview of what has been proven.
|
||
|
|
|
||
|
|
What can I say about reusability?
|
||
|
|
|
||
|
|
Misc
|
||
|
|
====
|
||
|
|
|
||
|
|
Propositional content
|