From 2c370ff25d4273df5797bdc0bd3453e43b34acab Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Mon, 25 Apr 2022 22:23:42 -0400 Subject: [PATCH] closes issue #190 --- doc/TYPES2021/referee/report-summary.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/doc/TYPES2021/referee/report-summary.md b/doc/TYPES2021/referee/report-summary.md index 3bc00fa8..4e6014cf 100644 --- a/doc/TYPES2021/referee/report-summary.md +++ b/doc/TYPES2021/referee/report-summary.md @@ -21,6 +21,15 @@ (addressed point c) + (Other than 'choosing setoids', very little, for part a. Our setup is the same as that of + Abel [1]. Capretta [5] uses setoids as well, but not universes since Coq doesn't "really". + It is hard to compare with [2], since their aim and ours are quite different, but it would be useful + to do so in the future. Our work is strictly more general than that of [11], which also uses + setoids, but restricts itself to finitary arities, which makes things "messy". [14] is quite + different, being in HoTT-UniMath, multi-sorted yet finitary. And yet, a lot of the 'results' + end up involving very similar statements. In other words, universal algebra seems to be quite + foundations-independent, at some level that should be investigated in the future) + 4. ~~Some links are broken (e.g. in [8]); some footnotes need to have first letters capitalised.~~ (fixed) @@ -74,6 +83,8 @@ algebras in S K, as in ยง6.2, would be forbidden because of size issues (e.g., let K be the class of all algebras with empty signature). + (A discussion section has been added for this) + 4. > ~~To the best of our knowledge, this constitutes~~ > ~~the first machine-verified proof of Birkoff's celebrated 1935 result.~~