И я таки ошибся

[posic]

как и опасался, но (насколько сейчас известно) не в том месте, где искал ошибку, а в самом конце. Из полной строгости композиции функторов A → B → C просто не следует полная строгость функтора A → B, это вам не вложения множеств. Поэтому неверно, что теорема Д.О. следует из моей, на что Д.О. мне и указал в письме.

Ну ладно, это еще ничего. Одного доказательства теоремы Д.О. достаточно, нет необходимости иметь непременно два. Сейчас я withdraw этот claim.