Sep. 27th, 2016

akuklev: (ДР Цертуса 2011)
Ура, дописал наконец свои соображения про то, откуда должны браться линейные зависимые типы, и как именно они связаны с топологией вычислимости и “полем с одним элементом”, плюс обрисовал в общих чертах как в HoTT получить ту самую категорию, которая содержит как обычные типы, так и иные спектры, и как последние можно понимать в смысле вычислений: https://github.com/akuklev/Linear-HoTT/blob/master/F1-LinTypes

Оно сырое дико и с уймой не доказанного пока wishful thinking, будем дорабатывать...

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 Jul. 28th, 2017 04:44 pm
Powered by Dreamwidth Studios