change definition of function sets equality to not build-in cong (

agda / agda-categories

A new Categories library for Agda

https://agda.github.io/agda-categories

MIT License

366 stars 68 forks source link

change definition of function sets equality to not build-in cong ( #407

Closed JacquesCarette closed 9 months ago

JacquesCarette commented 9 months ago

see agda-stdlib issue #1467 for further information. Fix everything that needed fixed because of that - a lot!

Amazing how many things actually depend on the equivalence of function setoids. Which, by extension, just how much 'set theory' there is in category theory.

JacquesCarette commented 9 months ago

Sorry, I screwed this up and made the changes on master, tried to fix it by going to a branch, and failed.