FIXMEs

[rolyp]

A subset of the current FIXMEs in the implementation.

Renamings

• algebra to algebraic-theory (purely because case-insensitive MacOS has clash with Algebra)
• commutative-monoid-cat to cmon
• galois to latgal?
• fam to indexed-family (to avoid confusion with Fam construction/2-functor)
• categories to category
• families-exponentials and families-functor to fam-exponentials and fam-functor?
• grothendieck to fam

Miscellaneous

• Equations relating eval and lambda in HasExponentials
• Equations relating join and unit in Monad
• CMon has all biproducts
• Unify join-semilattice meet-semilattice into semilat?

commutative-monoid-cat.agda

• cat has binary biproducts (via binary products and CMon self-enrichment?)

fam.agda

• Formalise indexed category?

galois.agda

• Meet (join) preservation of fwd (bwd) is implied by adjointness and monotonicity
• cat has initial object
• cat has binary biproducts (by CMon-enrichment?)
• rename ⊗ to ⊕
• cat is CMon-enriched
• galois.TWO is a monoid (by CMon-enrichment)
• Move presence out of Galois (relationship to two and Bool)?