search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
359 stars 67 forks source link

Add strict initial objects #423

Closed 4e554c4c closed 1 week ago

4e554c4c commented 2 weeks ago

This commit add strict initial object, and proves that any initial object in a CCC is strict. There is also a refactoring of the empty diagram.

JacquesCarette commented 2 weeks ago

On the question

I wonder why everything was using liftC (Discrete 0) then

This is because Data.Empty.Polymorphic did not yet exist when this was created. I contributed those because of this lack, but never had the chance to come back to agda-categories to refactor!