Oℕ
Тут было о нём примерно что-то вроде "А как по английски этот термин"
a · a = a. И элементы со свойством a · f · b = f, то первые можно считать объектами (b тоже с первым свойством), а вторые - стрелками. И можно из этого строить категорииSize: a a a
2020 February 12
МБ
Это когда у нас есть ассоциативная композиция (любая) и элементы со свойством
IK
Почему
Void является initial object? id и absurd же разные вещи. Значит морфинизм из Void в Void не уникальный.Oℕ
Почему
Void является initial object? id и absurd же разные вещи. Значит морфинизм из Void в Void не уникальный.одинаковые
O
так и хаск - не категория
Oℕ
id @ Void и absurd @ Void - это одинаковые функции
IK
Как у нас тут вообще определено равенство морфизмов?
IK
так и хаск - не категория
Почему
Oℕ
Как у нас тут вообще определено равенство морфизмов?
forall a. f a = g a
Oℕ
Почему
это не относится к инициальности Войда
IK
Там опечатка
IK
Войд не терминальный же
O
v :: a -> Void
v _ = undefined
v _ = undefined
Oℕ
Ну я всегда могу сказать "терминальный в оппозит категории", не подловите
IK
А у нас все _|_ равны получается?
Oℕ
v :: a -> Void
v _ = undefined
v _ = undefined
что это
O
доказательство, что войд - терминальный)))
Oℕ
доказательство, что войд - терминальный)))
это не доказательство, что войд терминальный
IK
Там нужна уникальность такого морфизма
IK
А не просто существование