coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] libraries for setoids?

From: "John Wiegley" <johnw AT newartisans.com>
To: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
Cc: "coq-club\@inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] libraries for setoids?
Date: Wed, 03 Oct 2018 11:31:02 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=johnw AT newartisans.com; spf=Pass smtp.mailfrom=johnw AT newartisans.com; spf=Pass smtp.helo=postmaster AT out3-smtp.messagingengine.com
Ironport-phdr: 9a23:G30n9R0LdwiPgUnksmDT+DRfVm0co7zxezQtwd8ZseIeKvad9pjvdHbS+e9qxAeQG9mDtLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPYQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7Vq4/Vyi84Kh3SR/okCYHOCA/8GHLkcx7kaZXrAu8qxBj34LYZYeYP+d8cKzAZ9MXXWpPUNhMWSNDDI28aIgBD+QPMulXs4bwvEcOoQekCAWwGO/i0CNEi3nr1qM6yeQhFgTG0RQuE9wKt3TUrNP1P7oSXuC00qbIwjHDYO1W2Dvz9YPFdRIhofaMXbJ2f8vc0k8vGB3Lj1qKs4zlIzKV1v8XvGid9OpsT/6gi2kiqwxopDWk28kiio7Mho0Py1DE8z10wIArKty2UkF7e8KkEJpLty6AMYt2WdkuTH1vuCY/0rEGtp+7fDQKyJQ63BHTceCIc4+N4h/lSe2fIi94iWpkdb++nRq+7FWsxvDmWsS7ylpGsChInsHOu30MzRDf9MaKR/Rn8kqg3TuDzR3f5+5ALE0yiKHVMYQuwqQqmZoWqUnDHjH5mEHxjKKOcUUk5/So5ur+brX9o5+cK5d0hhv7Mqswgcy/Gv43MgcPX2id9uSzyrvj/UL4QLVMkPI6iLXWsJffJcgDp665BRFa0po75hu+DjqqyskUkWQaIF5fdx+LlZblNlPWLPD9F/i/glCskDlxx/DBO73sGpfNLn/DkLfnc7dw8EhcxxQ9zN9F/ZJUFrABIOnpVU/3r9zUFAM2Mwuxw+r/EtVyypseWX6TAq+eKK7drViI5vs2L+aQYI8VpS3yJuM+5//uiH85gUUScbOo3ZsRcnC4H+5pL1+XYXr20Z89FjIotxE5SqSvul2FVzEbXHa/Wa15rhEmQNaoAYfRXdr12eSp3CCnG5RXYiZNDVXaQlnycIDREdULaCTaHc5snTgJRPLpH40m1RexnAn31LN9MuvP8ysD85nk0Y4mtKXoiRgu+GksXIym2GaXQjQxxztQHm5k7OVEuUV4j2y7/+19iv1cG8ZU4qoWAAE3KpfG0+1hAtbpHAnGe4XQEQr0cpCdGTg0C+kJ7ZoWeU8kRIekgw/KxTarGLYTjPqAA5lmqvuBjUi0HN50zjP97Idkj1QiRZAWZ2q7mvU67A3PH8jMnl6Cnqmrc6sR2iHM8mrFxm2L7hhV
Organization: New Artisans LLC

>>>>> "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

[Coq-Club] libraries for setoids?, Jason -Zhong Sheng- Hu, 10/01/2018
- Re: [Coq-Club] libraries for setoids?, John Wiegley, 10/03/2018
  - Re: [Coq-Club] libraries for setoids?, Bas Spitters, 10/03/2018