ЗП
что нет? это два куска одного целого леммы Йонеды
phi . psi = id
psi . phi = id
phi . psi = id
psi . phi = id
Size: a a a
2019 December 23
AZ
ну я как раз про это и говорил
AZ
Олег сказал что тут exists должен быть
AZ
а у меня три forall
ЗП
exists в Койонеде
AZ
то есть путаница в имнеовании, понял
PG
Боюсь ошибится, но вроде в хаскеле exists именно через forall пишется
ЗП
Йонеда про квантор всеобщности
Койонеда про квантор существования
Койонеда про квантор существования
ЗП
Боюсь ошибится, но вроде в хаскеле exists именно через forall пишется
не обязательно в хаскеле, exists выразим через двойной ранг forall
AZ
в койонеде будет что-то вроде
exists a. (a -> x, f a) <~> f x
exists a. (a -> x, f a) <~> f x
а, ты про койонеду и говорил. Всё, извини
МБ
Странно. Йонеда, вроде, как раз о существовании морфизма, определяющего естественное преобразование
ЗП
но у хаскеля есть и ExistentialQuantification
в частности все это может быть покрыто через GADTs
в частности все это может быть покрыто через GADTs
ЗП
Странно. Йонеда, вроде, как раз о существовании морфизма, определяющего естественное преобразование
Yoneda f -| f -| Coyoneda f
вроде так
вроде так
МБ
Что-то я запутался. Речь идёт о лемме Йонеды или о вложении Йонеды?
Oℕ
ко-Йонеда это в общем-то то же самое утверждение, другая его формулировка, на вики перечислены все четыре
простая и ко, для ковариантных и контравариантных
простая и ко, для ковариантных и контравариантных
Oℕ
Yoneda f -| f -| Coyoneda f
вроде так
вроде так
Это конечно же и близко не так.
Вы только что написали, что можете найти сопряжение для любого функтора в Set
Вы только что написали, что можете найти сопряжение для любого функтора в Set
ЗП
ко-Йонеда это в общем-то то же самое утверждение, другая его формулировка, на вики перечислены все четыре
простая и ко, для ковариантных и контравариантных
простая и ко, для ковариантных и контравариантных
койонеда нужна только когда надо сокрыть реализацию, а так да, одно и тоже
в общем это все вообще про Representation Theorem
в общем это все вообще про Representation Theorem
ЗП
Это конечно же и близко не так.
Вы только что написали, что можете найти сопряжение для любого функтора в Set
Вы только что написали, что можете найти сопряжение для любого функтора в Set
значит там равенства, я уже забыл
Oℕ
ну да, они все изоморфны
ЗП
часто идеи RT это про оптимизации