В рейтинге участвует:

групп:

каналов:

Виртуальный сервер на SSD - недорого!

Аренда выделенных и виртуальных серверов (VDS/VPS), хостинг, аренда IP-адресов, администрирование, круглосуточная поддержка

qwarta.ru подробнее

Резервное копирование с проверкой на вирусы!!!

Удобный сервис создания резервных копий на любой сервер сети интернет. Отслеживайте изменения, проверяйте на вирусы. Надежно защитите свой бизнес!

go.backupland.com

Выбираете сервер? Любая конфигурация на заказ!

Аренда физических серверов любых конфигураций под любые запросы - 1С бухгалтерия, игровые сервера, нагруженные проекты, интернет-магазины!

qwarta.ru подробнее

Size: a a a

groupoid.space

72 membersпожаловаться на группу
2017 November 02

TN

Tonpa Namdak in groupoid.space
Кароче повестка дня такая. Морберг готов принять Зигоморфизмы и другие рекурсивные схемы, но только при условии, что в файле не будет недоказанных теорем (наличие кейворда андефинед, аксиома в стиле кока). Для этого надо подключить fmap как тайпкласс через control.functor.
источник
07:46пожаловаться#1

TN

Tonpa Namdak in groupoid.space
Если есть желающие попробовать — это сделать — обсуждаем. Если нет — придется сделать мне самому :-)
источник
07:46пожаловаться#2

TN

Tonpa Namdak in groupoid.space
https://github.com/mortberg/cubicaltt/pull/86
источник
07:46пожаловаться#3

TN

Tonpa Namdak in groupoid.space
Можно выбрать любой тип и пытаться писать базовую либу в университетском стиле — каждому студенту свой тип-функтор и его естественные преобразования.
источник
07:48пожаловаться#4

TN

Tonpa Namdak in groupoid.space
http://groupoid.space/mltt/types/
источник
07:48пожаловаться#5

NP

Nikolay Pochekai in groupoid.space
Мне это интересно, но я что-то сообразить не могу какой конечный продукт предполагается: какое-то расширение кока?
источник
15:58пожаловаться#6

TN

Tonpa Namdak in groupoid.space
Групоид Инфинити — это спецификация на систему языков для создания сетифицируемой платформы, экстракта в другие языки и расширений MLTT ядра, как то пи-калкулусы или стрим-калкулусы.
источник
16:04пожаловаться#7

TN

Tonpa Namdak in groupoid.space
Хотя автор работает с экстрактом в Эрланг, вы можете писать имплементации в рамках концепции Групоид Инфинити в другие языки: Хаскель, Раст или что-то околофункциональное.
источник
16:05пожаловаться#8

TN

Tonpa Namdak in groupoid.space
Прежде всего речь идет о расширяемом ядре на базе MLTT, и сертифицированном интерпретаторе (прототип которого есть только на расте).
источник
16:06пожаловаться#9

TN

Tonpa Namdak in groupoid.space
Не смотря на то, что Групоид Инфинити — это инженерный проект, топ-левел язык делается совместимым с гомотопическим прувером от ученика Воеводского, Андерса Мортберга.
источник
16:07пожаловаться#10

TN

Tonpa Namdak in groupoid.space
Базовая библиотека пишется на его языке и делается совместимой с его языком — cubicaltt
источник
16:07пожаловаться#11

TN

Tonpa Namdak in groupoid.space
Ну и если вы хотите доказать свои модели или теоремы на cubicaltt, тут есть люди которые могут вам помочь с этим, если вы математик, а не инженер.
источник
16:09пожаловаться#12

NP

Nikolay Pochekai in groupoid.space
То есть нужно либу на cubicaltt написать, грубо?
источник
16:27пожаловаться#13

TN

Tonpa Namdak in groupoid.space
она есть, нужно выполнять задания по ее доработке
источник
16:27пожаловаться#14

TN

Tonpa Namdak in groupoid.space
https://github.com/groupoid/infinity/tree/master/priv
источник
16:27пожаловаться#15

NK

ID:402926333 in groupoid.space
http://dlicata.web.wesleyan.edu/pubs/lb14cubical/lb14cubes-oxford.pdf
@tonpa это кстати оно?
источник
20:24пожаловаться#16

TN

Tonpa Namdak in groupoid.space
Оно
источник
20:25пожаловаться#17

NK

ID:402926333 in groupoid.space
https://homotopytypetheory.org/2017/09/16/a-hands-on-introduction-to-cubicaltt/
Homotopy Type Theory
A hands-on introduction to cubicaltt
Some months ago I gave a series of hands-on lectures on cubicaltt at Inria Sophia Antipolis that can be found at: The lectures cover the main features of the system and don’t assume any prior…
источник
20:52пожаловаться#18

NK

ID:402926333 in groupoid.space
https://github.com/groupoid/infinity/tree/master/priv
GitHub
groupoid/infinity
♾️ INFINITY: Mathematical Components. Contribute to groupoid/infinity development by creating an account on GitHub.
источник
21:07пожаловаться#19

NK

ID:402926333 in groupoid.space
http://www.cse.chalmers.se/~coquand/rules7.pdf
источник
21:18пожаловаться#20