jwiegley/category-theory
View on GitHub ↗ ★ 820 Rocq Prover
An axiom-free formalization of category theory in Coq for personal study and practical work
3 mentions on Hacker News by 3 people: 1 story, 2 comments · first 2017-08-04 · latest 2026-09-29
20082026
-
…so good at maths though? I'm struggling to understand how it is raising issues such as this one https://github.com/jwiegley/category-theory/issues/598 in a mathematical category theory library written in Rocq prover, and creating and…
comment by jjhjhjhjhjh · 2026-09-29 · in Coding is not solved -
…It's a straight-forward construction within this framework and even part of the development[1]. [1] https://github.com/jwiegley/category-theory/blob/master/Inst...
comment by xhusshjd · 2017-08-05 · in A formalization of category theory in Coq -
▲ 109
A formalization of category theory in Coqstory by noch · 2017-08-04 · 33 comments