coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Impredicative Set

From: Jay Kruer <kruerj AT reed.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Impredicative Set
Date: Fri, 15 Mar 2019 14:33:33 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=kruerj AT reed.edu; spf=Pass smtp.mailfrom=kruerj AT reed.edu; spf=None smtp.helo=postmaster AT mail-qt1-f170.google.com
Ironport-phdr: 9a23:GcCu7hQFJ3UTFayIlErc7tQazNpsv+yvbD5Q0YIujvd0So/mwa68bRWN2/xhgRfzUJnB7Loc0qyK6vimATVIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfK9+IA+qoQnMq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mHLhcJ/g61VvRGvqRJhzYDTe4yVKON+fqbBcdMaWWZMXMBcXDFBDIOmaIsPCvIMM+JCoIj9ulAAqAG+BRSyC+P11zRFgXz23bcn0+s/CwHG3hctH8gQv3vKsdr5LrkdXv2ozKTRyzjIcvBY2S/l5YTWbhwspeuAULFwfMbL1EUiFh/Jgk+NpYHnIz+ZzvkBvmib4uZ6W++ihXQrpxx/rzSz3MsglI/EjZ8PxF/e7yV22oM1KMW4SEFlZd6kF4NdtySAOIt3RsMuWnhouDonxrEft563YSoHxIg9yx7QbPyHdIeI4hb9W+qLPTh4g3dldKq+hxa070eg1vXxWteo3FtOtCZIkdnBumoQ2xHS9sSLUOZx80W91TqX0gDc8OBEIUQ6larBLJ4hx6Y9lpkJsUTeACD2gkf2gbSMdko65Oen9v7rbav7qZ+BL4N0kB3xMrwymsyjBuQ1KhQBX2+C+eilyLLj+VD5T65Rg/0tkqjZtYjaKt4Bqq64BQ9VyIcj5AylAzeoytRL1UUAeVlCYVeMi5XjE1DIOvHxS/ml0Hq2lzI+5fnXdp77H5jXZizAiqrsZ7RV8UNRxEw+wc0JtMEcMa0IPP+mAhy5j9ffFBJsa1XlkdaiM81008YlYUzKB6aYNK3ItlrRvrA1LuSAIoIZpWSkcqR317vVlXY83GQlU+yxx5JOMCKiE/lqZUiVfCi024pTISIxpgM7CdfSphiCXDpUPSjgWqs94nQiFNvjA96cHsaih7uO2Cr9FZpTNDhL

Hi coq-club,

I am wondering how “sketchy” the use of impredicative Set in Coq developments
is considered. I have seen that impredicative Set is inconsistent with some
axioms of classical mathematics (e.g. excluded middle), but for the careful
user who avoids such axioms (or needs no axioms in their development at all)
is there any reason to avoid it? The Coq reference manual alludes to some
intuitionists taking issue with impredicative Set even before one introduces
inconsistency with axioms but I haven't been able to find any of those
arguments.

Thanks,
— Jay

[Coq-Club] Impredicative Set, Jay Kruer, 03/15/2019
- Re: [Coq-Club] Impredicative Set, Stefan Monnier, 03/15/2019
  - Re: [Coq-Club] Impredicative Set, Théo Zimmermann, 03/15/2019
    - Re: [Coq-Club] Impredicative Set, Jean-Francois Monin, 03/15/2019