Apr. 21st, 2016

HoTT

Apr. 21st, 2016 03:19 pm
akuklev: (ДР Цертуса 2011)
Для семейств индуктивных типов в HoTT эта-правила (aka каноничность) верны только пропозиционально, не субституционально (кроме как в erasable-контексте).

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

Я ковыряю Cubical TT, и ощущение, что вроде так можно. Там термы в замкнутой форме, вроде как, несут на себе достаточно информации, чтобы это всегда работало. Это-ж значит, что когда мы про тип (propositionally) знаем, что он set-like, можно пользоваться паттерн-матчингом в полную силу.
akuklev: (ДР Цертуса 2011)
http://www.display-tan.com/!
Ура, ура, наконец-то! Платёжная карточка, карточка с дисплеем и кнопками для бесконтактного подтверждения платежей смарткартой по Bluetooth и NFC. Никакого девайса носить с собой не надо, никакого считывания с экрана и вбивания через клавиатуру, идеально.

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

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

December 2016

S M T W T F S
    123
456789 10
11121314151617
18192021222324
25262728293031

Page Summary

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 19th, 2017 06:52 pm
Powered by Dreamwidth Studios