DB
Чем этот плагин не плагин
Size: a a a
2020 December 04
AG
ну у него под лин заточено, а тут для чего угодно
к
-- пруф что для любого e, e = []
-- пустой список на любой точке j от [0..1] равен пустому списку
-- del в точке 0 равен x::e, а в точке 1 равен e
_≡[] : (e : List⁰ A) → e ≡ []-- пустой список на любой точке j от [0..1] равен пустому списку
([] ≡[]) j = []
-- del в точке 0 равен x::e, а в точке 1 равен e
((x e) ≡[]) j = del x ((e ≡[]) j) j
-- тут строится квадрат, это уже нужно рисовать
(del x e i ≡[]) j = del x ((e ≡[]) j) (i ∨ j)к
ну у него под лин заточено, а тут для чего угодно
да я его использую просто чтобы юникод писать и вставлять куда-нибудь)
AG
ну вот можно взять латех-инпут
AG
был еще от японца какой то
DB
-- пруф что для любого e, e = []
-- пустой список на любой точке j от [0..1] равен пустому списку
-- del в точке 0 равен x::e, а в точке 1 равен e
_≡[] : (e : List⁰ A) → e ≡ []-- пустой список на любой точке j от [0..1] равен пустому списку
([] ≡[]) j = []
-- del в точке 0 равен x::e, а в точке 1 равен e
((x e) ≡[]) j = del x ((e ≡[]) j) j
-- тут строится квадрат, это уже нужно рисовать
(del x e i ≡[]) j = del x ((e ≡[]) j) (i ∨ j)Вот эти точки ваще неясно
AG
это самая волшебная часть кубов
AG
так называемые интервальные пред-типы
к
так, смотри еще раз
абстрактно, если мы имеем пространство (читай как тип) X, и две точке на нем a, b : X, то равенство
p : a = b
это НЕПРЕРЫВНАЯ функция
p : [0..1] -> X
с ограничениями что
p 0 = a
p 1 = b
а между 0 и 1 какой-то путь непрерывный
абстрактно, если мы имеем пространство (читай как тип) X, и две точке на нем a, b : X, то равенство
p : a = b
это НЕПРЕРЫВНАЯ функция
p : [0..1] -> X
с ограничениями что
p 0 = a
p 1 = b
а между 0 и 1 какой-то путь непрерывный
AG
был еще от японца какой то
AG
тоже похоже сгнил правда :(
к
то есть
del : (x :: xs) = xs
это такая функция, которая в del 0 будет равна (x::xs), а в del 1 = xs
при этом функция гарантированно непрерывная, и раз это задается аксиматически, значит это все одна и та же точка
del : (x :: xs) = xs
это такая функция, которая в del 0 будет равна (x::xs), а в del 1 = xs
при этом функция гарантированно непрерывная, и раз это задается аксиматически, значит это все одна и та же точка
к
простой пример
если у нас есть
p : a = b
то мы можем построить обратный путь
q : b = a
q i = p (1 - i)
если у нас есть
p : a = b
то мы можем построить обратный путь
q : b = a
q i = p (1 - i)
DB
так, смотри еще раз
абстрактно, если мы имеем пространство (читай как тип) X, и две точке на нем a, b : X, то равенство
p : a = b
это НЕПРЕРЫВНАЯ функция
p : [0..1] -> X
с ограничениями что
p 0 = a
p 1 = b
а между 0 и 1 какой-то путь непрерывный
абстрактно, если мы имеем пространство (читай как тип) X, и две точке на нем a, b : X, то равенство
p : a = b
это НЕПРЕРЫВНАЯ функция
p : [0..1] -> X
с ограничениями что
p 0 = a
p 1 = b
а между 0 и 1 какой-то путь непрерывный
Две точки равны, если между ними есть непрерывный путь?
к
symm : a = b -> b = a
symm path i = path (1 - i)
symm path i = path (1 - i)
к
Две точки равны, если между ними есть непрерывный путь?
ну вот такое кубическое равенство задает это равенство точек аксиоматически
к
то есть не
"если точки равны, то есть путь"
а
"если есть путь, то равны"
"если точки равны, то есть путь"
а
"если есть путь, то равны"
DB
то есть не
"если точки равны, то есть путь"
а
"если есть путь, то равны"
"если точки равны, то есть путь"
а
"если есть путь, то равны"
Я так и написал(
к
а между двумя одинаковым точками всегда есть путь
refl : (a : X) -> a = a
refl x i = x
refl : (a : X) -> a = a
refl x i = x