A list of modules to port about agda-categories HOT 28 CLOSED

@JacquesCarette are you able to check the boxes above?

from agda-categories.

Yes, I can (and just checked Functor/Discrete.agda). Unfortunately, this doesn't let me do anything 'alternate', like cross it off. For example, Equalizer.agda was empty in the original library, so we should ignore it. Same with Enriched and Closed. And Bifunctor/NaturalTransformation was not useful enough to bother with. Should these also be checked?

from agda-categories.

Equalizer is defined so we should check it. I don't know why some modules are empty in the original library. there are some of those I would like to define. if you think there are some modules that are not too useful we can check them off and regard them as done.

from agda-categories.

Dropping Object/Indexed, IndexedProduct and IndexedProducts.

from agda-categories.

Object/Exponentiating (and supporting functions) are not used anywhere, and not really documented on nLab either, so dropping for now. Unless there's a specific request later.

from agda-categories.

Presheaves -> Category.Construction.Presheaves.

from agda-categories.

Object/Exponentiating (and supporting functions) are not used anywhere, and not really documented on nLab either, so dropping for now. Unless there's a specific request later.

I believe that's a special status of exponential.

https://ncatlab.org/nlab/show/exponential+object#related_notions

More generally, a morphism f:Y→A is exponentiable (or powerful) when it is exponentiable in the over category C/A.
...
Conversely, if X is such that X^Y exists for all Y, we say that X is exponentiating.

but I am not sure if this concept is useful outside the context of CCC.

from agda-categories.

If there's anything you feel we do need, go ahead and 'uncheck' it.

from agda-categories.

no I don't find it useful. i was just quote the related part from nLab. in CCC exponential is a bifunctor so this concept indeed looks less important to me.

from agda-categories.

Terminal.agda becomes Categories.instance.One.

from agda-categories.

2-Categories/Categories (which was far from finished) becomes Categories.2-Category.Instance.Cats (and is done).

from agda-categories.

Object/SubobjectClassifier.agda moved to Diagram.SubobjectClassifier.

from agda-categories.

Categories.Products is Categories.Category.Monoidal.Instance.Cats

from agda-categories.

Congruence really doesn't seem useful (or stylistically compatible), so I'm going to drop it.

from agda-categories.

Functor.Coalgebras (which should be Category.Construction.F-Coalgebras) was empty, so is trivially "ported". It still needs implemented, but that should be a different issue.

from agda-categories.

Skipping Lift, as I'm hoping it is largely not needed. [Not quite true, but I think it's overkill]

from agda-categories.

Monad.Algebra and Monad.Algebras were empty.

from agda-categories.

Normalize is very cool - but should be done via Reflection these days rather than in this manner. Drop.

from agda-categories.

Looks to me like the contents of Object/BinaryProducts/Abstract has already been put elsewhere?

from agda-categories.

Topos was empty - marking it as done. It can be done later.

from agda-categories.

Object/Terminal/Exponentiating not useful enough, dropping. Other two Object/Terminal/... are in Categories.Object.Product.Construction as they are constructors of products (and exponentials) [under some assumptions, in this case, of there being a Terminal object around). This file may get extended with more constructions.

from agda-categories.

Monoidal/IntConstruction was highly unfinished, and is quite non-trivial. So while it should eventually be implemented, that's not an issue of 'porting'.

from agda-categories.

Monad/Coproduct isn't really a coproduct of monads. It is rather a construction of (trivial) monad(s) when an underlying category has all coproducts. This doesn't seem all that useful, dropping.

from agda-categories.

I'm marking 2-Category as done, as there is now an adequate definition. 2-Category/Categories was unfinished. The only way to hope to do it would be to port the old 2-Category as it was done (unbundled, by hand), so that the axioms can hard-code which equality to use. A horrible hack, but it would allow things to work a bit more. Really not worth it, IMHO, as Bicategory is really the better option.

from agda-categories.

CategorySolver is another piece of technology that doesn't seem worth porting at all.

from agda-categories.

@HuStmpHrrr : all that's left is Adjunction/CompositionLaws, but I've looked at it, and I don't strongly feel like porting it. In particular, it looks to me like a proper port would require using Mates, and you're the expert there. We could even decide to do that one 'in the future', open an issue and close this one.

from agda-categories.

all these composition laws require equivalence of adjoints. is it reasonable to talk about equivalence between adjoints? we had it before but it was removed. I supposed not. then we just don't need this module.

from agda-categories.

In a proof-relevant setting based on Hom-Setoids, it doesn't make sense to ask for too-strong an equivalence of Adjoints (thus the mention of Mates). So we can't just port this, it would be a whole new implementation. Which can be done later, when someone actually needs it.

from agda-categories.