KC
Size: a a a
2020 August 03
AG
там тоже они, но вшитые в само исчисление
KC
Так зачем ты душишь кривду
AG
а тут как я понимаю они только для имен работают
Oℕ
что это такое то
AG
что то типа разницы между сепарационкой и линейщиной
AG
что это такое то
ну тип конструкция, позволяющая определять свои логические коннективы, параметризованные перестановками
D
public export
data Ten : Sp a -> Sp a -> Sp a where
MkTen : (proj1 : Sh s zs) -> (proj2 : Sh t zs) -> Cover True (snd $ thinning proj1) (snd $ thinning proj2) -> Ten s t zs
data Ten : Sp a -> Sp a -> Sp a where
MkTen : (proj1 : Sh s zs) -> (proj2 : Sh t zs) -> Cover True (snd $ thinning proj1) (snd $ thinning proj2) -> Ten s t zs
D
ну что за пиздец!
AG
это конъюнкция в топосе
AG
ради нее собственно все и городится
w
ради нее собственно все и городится
Эх, сча бы городится
D
в топосе?
AG
где?
в кодебрёйн подходе
AG
идея примерно та же что в линейщине - разделить контекст между потомками
AG
но при этом сохранить викенинг и контракцию