category-theory

Category theory library

An axiomatic formalization of category theory in Coq for personal study and practical work

An axiom-free formalization of category theory in Coq for personal study and practical work

GitHub

759 stars
20 watching
71 forks
Language: Coq
last commit: 3 months ago
Linked from 2 awesome lists

cartesiancartesian-closed-categorycategoriescategorycategory-theorycomonadsconstructioncoqfunctormonadmonoidprofunctorprofunctor-composition

Backlinks from these awesome lists:

Related projects:

Repository Description Stars
amintimany/categories An implementation of category theory in the Coq proof assistant. 94
jcouyang/cat.js A JavaScript implementation of category theory concepts with various monad and functor classes. 15
jwiegley/coq-haskell A Coq library providing definitions and notations to facilitate interaction between Haskell developers and the Coq proof assistant. 168
uncomplicate/fluokitten A Clojure library implementing category theory concepts for functional programming 468
coq-community/graph-theory Formalized graph theory results for research and verification 35
hivert/coq-combi An algebraic combinatorics library formalized in Coq, providing a comprehensive set of functions and theories for symmetric functions. 1
jtassarotti/coq-proba A Coq-based probability theory library providing results and definitions for discrete probability, measure theory, and probabilistic choice monads. 50
choukh/set-theory A formalization of set theory and its foundational axioms in the Coq proof assistant language 59
geohot/coq-hardy Formalizing mathematical theorems from Hardy's book in Coq to create a rigorous and reproducible formalization of number theory 53
hott/coq-hott A Coq library for interpreting Martin-Löf's intensional type theory into abstract homotopy theory and relating it to higher category theory. 1,262
affeldt-aist/monae A Coq library for formalizing and reasoning about monads with equational logic 70
charguer/tlc A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. 38
coq-community/coqeal A Coq library providing algebraic data structures and algorithms 67