Alexander Grothendieck (1928-2014)

Гений, великий интуит, создатель новой математики, и один из самых странных и необычных людей столетия.


(Он тут одновременно похож на Гэндальфа, Мерлина и библейских патриархов.)

(no subject)

Для шрифта unifont имеется карта в виде картинки, если её посмотреть, например, сразу приходит интуитивное понимание, сколько на самом деле базовых китайских иероглифов: http://unifoundry.com/pub/unifont-7.0.06/unifont-7.0.06.bmp (ахтунг, файлик немаленький, там все 256² символов основного юникода). Можно посмотреть сперва издалека на эту серую тучу высотой в полфайла, а потом приблизиться и посмотреть в ужасе.

Это, конечно, только основные иероглифы, использующиеся сейчас в китайском, и отчасти корейском и японском языках, всего 20941 символов. (Тут ещё надо отметить, что они там изображены в китайском написании. Добавив в юникодном тексте после кода иероглифа специальный символ варианции (#FE00..#FE0F)) можно выбрать японское или корейское написание, которые отличаются от китайских для нескольких тысяч иероглифов. Их знание, насколько я понимаю, позволяет читать газеты, вывески всякие, простые книжки и т.д. В дополнение к указанным иероглифам в базовом юникоде ещё существуют общеупотребительное расширение А, содержащие 6582 иероглифов, часто содержащихся в географических названиях и современных тематических статьях.

Но это всё ещё далеко не все иероглифы! Это всего 25 тысяч символов, которые, учитывая дубликаты, получившиеся из-за отдельного кодирования упрощённого (после культурной революции) китайского следовало бы скорее считать 18 тысячами. При этом говорят, что грамотный человек должет знать вдвое больше иероглифов, порядка 40000.

На то в юникоде есть дополнения B и его поправки C и D (они должны были быть одним дополнением B, если бы не технические накладки), содержащие совокупно 47082 символа, правда из них пара сотен снова являются дубликатами, и ещё тысяч десять не собственно китайские, а вьетнамские иероглифы, которые совсем вышли из употребления в XX веке, когда Вьетнам перешёл на латиницу. Конечно же, и это не всё, иероглифы, кажется, придумывали все, кому не лень, так что по сусеком наскребается ещё несколько тысяч.

Попытка ответить на свой вопрос #HoTT

Несколько постов назад я задал вопрос, как бы нам так определить для высших индуктивных типов T тип $T, зависимых бесконечных последовательностей, где первым элементом e: T, вторым e1: Id(e, e), третьим e2: Id(e1, e1) и так далее. Понятно что это можно рассматривать как тип коданных заданный деструктором

d: $[T] -> (head: T, tail: $[Id(head, head)]),

но хочется же не этого. ( Read more... )