(no subject)

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

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