The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

Have a look at our math-classes and corn libraries:
http://math-classes.github.io/
https://github.com/coq-community/corn

Math-classes also includes categories.
John, I've moved math-classes to the coq-community to make it easier
for others to contribute/share code.
Could any of the work there be useful for you?
On Wed, Oct 3, 2018 at 8:31 PM John Wiegley 
<johnw AT newartisans.com>
 wrote:
>
> >>>>> "J-SH" == Jason -Zhong Sheng- Hu 
> >>>>> <fdhzs2010 AT hotmail.com>
> >>>>>  writes:
>
> J-SH> I am wondering are there any libraries which fully commit to setoids 
> in
> J-SH> Coq? I am looking for ones that push the idea of setoids as far as
> J-SH> possible. For example, agda's standard library (agda-stdlib) is 
> entirely
> J-SH> built around setoids. I am mainly looking for libraries that handle 
> list
> J-SH> and relations around it in that manner and hoping someone has done 
> some
> J-SH> work.
>
> My category theory library is entirely based on setoids everywhere (making 
> it
> about quasi-categories, basically):
>
>   https://github.com/jwiegley/category-theory
>
> What gets tricky is that Sets is now the category of Setoids, meaning that
> every object also needs a setoid relation, etc.
>
> --
> John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F
> http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2