AG
Ну человек явно ещё не готов к сетоидам. В идрисовской формулировке они там именно, что пользуются встроенным равенством и просто аксиомы направо и налево лепят
в коке скорее так
Size: a a a
2020 July 27
IJ
Пробовал определить тайпкласс параметризованный типом объектов. Ещё не дочитался до functional existentionality. Буду рыть в эту сторону, спасибо!
Это грубо говоря
Inductive feq A B : (A->B)->(A->B)->Prop :=
| feq_intro: forall f g,
(forall x, f x = g x) -> feq f g
Inductive feq A B : (A->B)->(A->B)->Prop :=
| feq_intro: forall f g,
(forall x, f x = g x) -> feq f g
IJ
Это грубо говоря
Inductive feq A B : (A->B)->(A->B)->Prop :=
| feq_intro: forall f g,
(forall x, f x = g x) -> feq f g
Inductive feq A B : (A->B)->(A->B)->Prop :=
| feq_intro: forall f g,
(forall x, f x = g x) -> feq f g
Про эту штуку вы легко докажете нужные вам свойства (предполагаю, коммутации)
Oℕ
в коке скорее так
Ну я имею в виду https://github.com/statebox/idris-ct, я коковские и не смотрел особо
AK
Это грубо говоря
Inductive feq A B : (A->B)->(A->B)->Prop :=
| feq_intro: forall f g,
(forall x, f x = g x) -> feq f g
Inductive feq A B : (A->B)->(A->B)->Prop :=
| feq_intro: forall f g,
(forall x, f x = g x) -> feq f g
Для каждой категории это должен быть свой feq?
Oℕ
Ближайшая любимая теория, где можно как-то обойтись без сетоидов и аксиом - это HoTT, но там свои нюансы
AK
Ещё вопрос, что «лучше» для формальной проверки знаний в теоркате: idris, agda, coq, alloy или всё равно?
Oℕ
arend
Oℕ
Точно не всё равно, но везде будут свои проблемы
AK
Стало понятнее куда копать, спасибо!
AG
Ещё вопрос, что «лучше» для формальной проверки знаний в теоркате: idris, agda, coq, alloy или всё равно?
если ограничиваться вашим списком, то agda с включенным кубическим режимом
AG
но надо учитывать что это экспериментальная реализация по своей сути
KV
И всё это ради одного несчастного funext
AG
скорее ради хитов
AG
можно напрямую всякие пулбеки кодировать
KV
скорее ради хитов
Это в смысле чтобы определение категории сразу с равенствами писать?
KV
Что-то я этим вопросом сам себя озадачил
AG
да много всякого можно придумать
AG
Oℕ
Это в смысле чтобы определение категории сразу с равенствами писать?
свободные штуки например