PG
Пока у меня и так все получается.
Size: a a a
2018 January 12
ЕО
Сетоиды это множество с отношением эквивалентности. Но имеет смысл их рассматривать только в интуиционистских системах, потому что в классических аксиоматиках они ведут себе как множества
ЗП
Сетоиды это множество с отношением эквивалентности. Но имеет смысл их рассматривать только в интуиционистских системах, потому что в классических аксиоматиках они ведут себе как множества
это же у сетоида 3 правила должно быть?
1) рефлексивность
2) симметричность
3) транзитивность
1) рефлексивность
2) симметричность
3) транзитивность
PG
к
это же у сетоида 3 правила должно быть?
1) рефлексивность
2) симметричность
3) транзитивность
1) рефлексивность
2) симметричность
3) транзитивность
ну насколько я знаю по таплу, отношение эквивалентности это и есть отношение рефлексивности+симметричности+транзитивности
к
ЗП
ты мне пытаешься про
≈ рассказать?к
нет, просто ты на сообщение, где уже сказано, что в сетоиде есть отношение эквивалентности, спросил, есть ли там отношение эквивалентности через его составляющие. Логичен был вывод, что ты этого не знал, поэтому я и написал
ЗП
нет, просто ты на сообщение, где уже сказано, что в сетоиде есть отношение эквивалентности, спросил, есть ли там отношение эквивалентности через его составляющие. Логичен был вывод, что ты этого не знал, поэтому я и написал
я переспросил, если бы я не знал, я бы спросил про свойства
ЕО
это же у сетоида 3 правила должно быть?
1) рефлексивность
2) симметричность
3) транзитивность
1) рефлексивность
2) симметричность
3) транзитивность
Это не у сетоида, это у отношения эквивалетности
ЗП
Это не у сетоида, это у отношения эквивалетности
сетоид подразумевает под собой это https://github.com/agda/agda/blob/master/examples/Setoid.agda#L23-L29
ЕО
_≈_ <- это отношение эквивалетности
PG
Надо меньше код писать и больше думать, вроде у сетоида нету таких свойств, но у него есть отношение эквивалентности внутре.
к
чет агда очень сложная, столько кейвордов
🦉
я слушаю вас
🦉
и охуеваю
🦉
читаю чат раста
🦉
и охуеваю
ЗП
еще пока эту агду заведешь на компе
🦉
здесь сетоиды там сессионные типы