[Coq-Club] libraries for setoids?

[Jason -Zhong Sheng- Hu]

Hi all,

I am wondering are there any libraries which fully commit to setoids in Coq? I am looking for ones that push the idea of setoids as far as possible. For example, agda's standard library (agda-stdlib) is entirely built around setoids. I am mainly looking for libraries that handle list and relations around it in that manner and hoping someone has done some work.

Sincerely Yours,

Jason Hu

[John Wiegley]

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.

[Bas Spitters]

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?

Post by John Wiegley
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
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