Hacker News
new
|
past
|
comments
|
ask
|
show
|
jobs
|
submit
login
solomatov
on Aug 5, 2017
|
parent
|
context
|
favorite
| on:
A formalization of category theory in Coq
Concerning everything important. It seems, that it's enough for equality to respect only composition. So, basically category of categories is expressible there. But HoTT would give you much more power.
Guidelines
|
FAQ
|
Lists
|
API
|
Security
|
Legal
|
Apply to YC
|
Contact
Search: