Sandro Stucki

[ re #1752 ] add properties of ordered structures for Nat.

15

Follow-up to #1752, implementing the new ordered structures for `Data.Nat`. The PR currently replaces the old (unordered) proofs by ordered ones and then re-exports derived versions of the old ones....

[ draft ] add Galois connections and residuated lattices.

3

This PR is not ready to be merged. I think the contents are useful, but there are some problems with the organization of the code (what goes into which module...

Challenge: prove that the Discrete functor is the (cartesian) left-adjoint of the forgetful functor from Cats to Sets

8

Categories currently don't carry an explicit notion of equality on objects. This seems to be a "standard" way to mechanize categories constructively (as far as I'm aware), it is in...

Create a contributor's guide

2

(Prompted by the discussion in https://github.com/agda/agda-categories/pull/304#issuecomment-905410931.) There are some guidelines in the README.md about what idioms to use and to avoid, but there are also a bunch of non-trivial patterns...

This corresponds to Section 1.5 of [Kelly's book](http://www.tac.mta.ca/tac/reprints/articles/10/tr10abs.html). (Depends on #120.) A nice result that can be mechanized once this is done: every CCC, is self-enriched. I.e. an (ordinary) CCC...

Rename record fields for functorial actions and components of natural transformations

12

#### TL;DR I really, *really*, don't like the names of the fields `F₀`, `F₁` and `η` in the `Functor` and `NaturalTransformation` records. Below, I explain why and suggest some alternatives....