An attempt at a category theory encoding in Coq, for learning purposes.
Core concepts (Category, Functor, NaturalTransformation, etc.)
are in the CT directory. Instances and derivations both live in the
CT/Instance directory (and thus the CT.Instance namespace). A simple
algebra hierarchy is found in CT/Algebra. Definitions there are largely
decategorified, even when the
structures can be defined purely categorically. There are instances (e.g.
CT.Instance.Category.MonoidCategory (the category for any given Monoid))
which make use of them.
The layout of the project is fairly simple. If you wish to work with, for example, functor categories, you'll likely want to do something like:
Require Import CT.Category.
Require Import CT.Instance.Category.FunctorCategory.
(* ... *)In any documentation we write, an instance is a particular usage of a
concept. For example CT.Instance.Coq.Functor exports a CoqOptionFunctor
which, as the name suggests, is a Functor for Coq's option type
(specifically it is an endofunctor from CoqType -> CoqType, where CoqType
is defined in CT.Instance.Coq.Category to be the category of Coq types).
We call something a derivation if passing it something generates a
specialized version of that thing. For example, FunctorCategory is a
derivation because it takes two Category parameters to return the functor
category between them. Similarly, a MonoidCategory takes a Monoid and
returns a Category with a single object (with composition defined by
Monoid's mu).
These ("instance", "derivation") are mostly made-up terms, but we have been using them pretty consistently in our documentation/on IRC.
We rarely use Notation or Infix in the library. This is intentional and done
for added clarity. While Coq's notation system can be extremely helpful
(especially in combination with scopes), since this is a library written
for educational purposes, we wish to not cloud any view of what is actually
happening. We do sprinkle in use of implicit arguments fairly liberally,
however.
... so far.
- https://arxiv.org/pdf/1505.06430v1.pdf (and https://github.com/amintimany/Categories)
- The Homotopy Type Theory source
- Basic Category Theory
- copumpkin/categories - an Agda encoding of category theory
- http://www.cs.ox.ac.uk/ralf.hinze/publications/TFP09.pdf (and https://github.com/jwiegley/coq-lattice/)
MIT