век живи, век учись

Когда я тут возмущался фривольностью строительства типовых лямбд на декартово-замкнутой категории, меня сильно задело, что декартово произведение, к примеру, используется в качестве типа - но ведь оно с точностью до изоморфизма!

Ну всё не так загадочно.

Функтор декартова произведения - сопряженный функтор к диагонали. Конечно, сопряженный функтор тоже с точностью до изоморфизма; можно взять такой, можно взять такой. Но когда один взяли, то мы его уже взяли - вот значения этого функтора и берутся в качестве значений произведения. К типа это и относится, непосредственно. HoTT пока не нужен, в этом смысле.

Это я приник к источнику с утреца, к МакЛейну.

добрая страховка

Заходишь это на их сайт, логинишься, и вдруг большими буквами посередине экрана:

Skin Cancer

Нет, это не у вас. Это вообще, к слову пришлось. Это они пугают. Мол, сходите проверьтесь (а то у нас будут большие расходы).

где живёт маркиз

Если бы вы были собакой