HoTT

Для семейств индуктивных типов в HoTT эта-правила (aka каноничность) верны только пропозиционально, не субституционально (кроме как в erasable-контексте).

Это так, да тех пор, пока при операции подстановки действительно просто подсталяется терм, однако если операция подстановки модифицирует терм, используя данные типизации из контекста, нельзя ли восстановить “подстановочность” для set-like типов?

Я ковыряю Cubical TT, и ощущение, что вроде так можно. Там термы в замкнутой форме, вроде как, несут на себе достаточно информации, чтобы это всегда работало. Это-ж значит, что когда мы про тип (propositionally) знаем, что он set-like, можно пользоваться паттерн-матчингом в полную силу.

Карточное

http://www.display-tan.com/!
Ура, ура, наконец-то! Платёжная карточка, карточка с дисплеем и кнопками для бесконтактного подтверждения платежей смарткартой по Bluetooth и NFC. Никакого девайса носить с собой не надо, никакого считывания с экрана и вбивания через клавиатуру, идеально.

А, нет, неидеально, на карточке только кнопка OK и нету кнопочек для вбивания PINа для транзакций на значительные суммы.

Это всё, конечно, полумеры. Когда-нибудь просто сделают смартфоны в формфакторе платёжной карты.