ΛВ
А чё идёт не так?
Size: a a a
2021 June 16
AG
The function comprehension principle is immediate for weak propositions in OTT and XTT, but fails for strict propositions.
(1) To exhibit a function A→B from a weak functional relation, we may extract the y:B using the universal property of the weak squash type, fulfilling the auxiliary obligation using the weak uniqueness of y with R(x,y).
(2) In doing the same with a strict functional relation, we run into a problem: to make a function out of an element of the strict squash type, we end up needing that y is unique with R(x,y) up to judgmental equality, but we have only an element of path B(y,y′) for each y′ such that R(x,y′).
Therefore, short of adding equality reflection, we must conclude that the weak notion of proposition is the “correct” one, and the strict one is not particularly useful for mathematics in an environment without equality reflection. Unfortunately, we will see that another indispensable reasoning principle in constructive and classical mathematics, the effectivity of equivalence relations, appears to be compatible only with the strict notion in a boundary separated environment lacking equality reflection. (In contrast, full cubical type theory satisfies a vastly stronger exactness condition called descent, generalizing both the disjointness of coproducts and the effectivity of equivalence relations.)
(1) To exhibit a function A→B from a weak functional relation, we may extract the y:B using the universal property of the weak squash type, fulfilling the auxiliary obligation using the weak uniqueness of y with R(x,y).
(2) In doing the same with a strict functional relation, we run into a problem: to make a function out of an element of the strict squash type, we end up needing that y is unique with R(x,y) up to judgmental equality, but we have only an element of path B(y,y′) for each y′ such that R(x,y′).
Therefore, short of adding equality reflection, we must conclude that the weak notion of proposition is the “correct” one, and the strict one is not particularly useful for mathematics in an environment without equality reflection. Unfortunately, we will see that another indispensable reasoning principle in constructive and classical mathematics, the effectivity of equivalence relations, appears to be compatible only with the strict notion in a boundary separated environment lacking equality reflection. (In contrast, full cubical type theory satisfies a vastly stronger exactness condition called descent, generalizing both the disjointness of coproducts and the effectivity of equivalence relations.)
w
это нихуя не читаемо
R
если дашь описание понятное для девопса
R
то я могу у своего спросить
R
еси он не занят
ΛВ
А как не коннектится?
AG
интересно шо стерлинг фактически говорит что спроп походит только для программирования
AG
но при это на практике как я понимаю его наоборот используют для пучковизации сельского хозяйства
AG
где противоречие интересно
AG
аксиома уникального выбора не важна для синтаксических моделей видимо
GP
экпоузи порты каждого жава процесса внутри каждого пода и форварди порт себе на локал
GP
ну вот эти флаги все жмхремоут и тп
GP
а потом делаешь port-forward
GP
а я прочитал все посты, у тебя hostname точн тот?
Oℕ
я форвардю с помощью кубцтл