Size: a a a

2020 December 04

DB

Danil Berestov in haskell_blah
Чем этот плагин не плагин
источник

AG

Alex Gryzlov in haskell_blah
ну у него под лин заточено, а тут для чего угодно
источник

к

кана in haskell_blah
-- пруф что для любого e, e = []
_≡[] : (e : List⁰ A) → e ≡ []
-- пустой список на любой точке j от [0..1] равен пустому списку
([]        ≡[]) j = []
-- список из x :: e в точке j равен тому чему равен del x (e = j) в точке 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)
источник

к

кана in haskell_blah
Alex Gryzlov
ну у него под лин заточено, а тут для чего угодно
да я его использую просто чтобы юникод писать и вставлять куда-нибудь)
источник

AG

Alex Gryzlov in haskell_blah
ну вот можно взять латех-инпут
источник

AG

Alex Gryzlov in haskell_blah
был еще от японца какой то
источник

DB

Danil Berestov in haskell_blah
кана
-- пруф что для любого e, e = []
_≡[] : (e : List⁰ A) → e ≡ []
-- пустой список на любой точке j от [0..1] равен пустому списку
([]        ≡[]) j = []
-- список из x :: e в точке j равен тому чему равен del x (e = j) в точке 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

Alex Gryzlov in haskell_blah
это самая волшебная часть кубов
источник

AG

Alex Gryzlov in haskell_blah
так называемые интервальные пред-типы
источник

к

кана in haskell_blah
так, смотри еще раз

абстрактно, если мы имеем пространство (читай как тип) X, и две точке на нем a, b : X, то равенство
p : a = b
это НЕПРЕРЫВНАЯ функция
p : [0..1] -> X
с ограничениями что
p 0 = a
p 1 = b
а между 0 и 1 какой-то путь непрерывный
источник

AG

Alex Gryzlov in haskell_blah
Alex Gryzlov
был еще от японца какой то
источник

AG

Alex Gryzlov in haskell_blah
тоже похоже сгнил правда :(
источник

к

кана in haskell_blah
то есть
del : (x :: xs) = xs
это такая функция, которая в del 0 будет равна (x::xs), а в del 1 = xs
при этом функция гарантированно непрерывная, и раз это задается аксиматически, значит это все одна и та же точка
источник

к

кана in haskell_blah
простой пример
если у нас есть
p : a = b
то мы можем построить обратный путь
q : b = a
q i = p (1 - i)
источник

DB

Danil Berestov in haskell_blah
кана
так, смотри еще раз

абстрактно, если мы имеем пространство (читай как тип) X, и две точке на нем a, b : X, то равенство
p : a = b
это НЕПРЕРЫВНАЯ функция
p : [0..1] -> X
с ограничениями что
p 0 = a
p 1 = b
а между 0 и 1 какой-то путь непрерывный
Две точки равны, если между ними есть непрерывный путь?
источник

к

кана in haskell_blah
symm : a = b -> b = a
symm path i = path (1 - i)
источник

к

кана in haskell_blah
Danil Berestov
Две точки равны, если между ними есть непрерывный путь?
ну вот такое кубическое равенство задает это равенство точек аксиоматически
источник

к

кана in haskell_blah
то есть не
"если точки равны, то есть путь"
а
"если есть путь, то равны"
источник

DB

Danil Berestov in haskell_blah
кана
то есть не
"если точки равны, то есть путь"
а
"если есть путь, то равны"
Я так и написал(
источник

к

кана in haskell_blah
а между двумя одинаковым точками всегда есть путь
refl : (a : X) -> a = a
refl x i = x
источник