This seminar supposed to be a contemporary introduction to modern type theory that is suitable for mathematicians needs, in the sense that this theory forms a foundation of mathematics and the language for theorems formulation and their proofs.

https://groupoid.space/course

[1]. Лузгарев, Конспект. Алгебраическая K-теория для самых маленьких
     http://mahalex.net/special-courses/_ktheory/ktheory.pdf

[2]. Лузгарев, Конспект. Алгебраическая геометрия
       http://mahalex.net/special-courses/_ag/ag.pdf

[3]  REDMOND MCNAMARA. INTRODUCTION TO DE RHAM COHOMOLOGY
      http://math.uchicago.edu/~may/REU2014/REUPapers/McNamara.pdf

K-Theory foundation. Grothendieck Group.
Checking: grothendieck
File loaded.
>

https://threadreaderapp.com/thread/1012890522711744512.html

Третий курс по HoTT http://www.andrew.cmu.edu/user/erijke/hott/

A General Language. by Erret Bishop. The Unpublished Paper on Type Theory before Martin-Löf.

[1] Higher-Dimensional Types in the Mechanization of Homotopy Theory (PhD)
Kuen-Bang Hou (Favonia)
https://favonia.org/files/thesis.pdf

[2] Synthetic Cohomology in Homotopy Type Theory
Evan Cavallo December 16, 2015
https://www.cs.cmu.edu/~rwh/theses/cavallo.pdf

A GEOMETRIC INTRODUCTION TO K-THEORY DANIEL DUGGER
http://pages.uoregon.edu/ddugger/kgeom.pdf

Друзья, группа переходит в закрытый режим, я вам все послал сообщение "Привет, какими судьбами на групоиде?" вы можете ответить на него, рассказав о себе и своей мотивации, и согласиться о нераспространении приватной информации которая будет тут возможно выкладываться, а так же не упоминать мое имя в интернете в дальнейшем. Если вы не согласны с этим, просто проигнорируйте это, или заявите о несогласии, и я вас автоматически отпишу. Те, кто не получил этого сообщения, вполне вероятно уже прошли проверку временем или подписали такой контракт. Ничего личного, просто мы сужаем сектарное пространство. Спасибо за понимание.

Недавно в рассылке HoTT (кто не подписался, советую) https://groups.google.com/forum/#!forum/homotopytypetheory проскакивал вопрос о вариантах J элиминатора.

Все три версии J: Диагнальная (моя любимая), HoTT (классическая) и Полины-Моурин (поправьте меня если ошибся), есть у нас на групоиде. На курсах будут задачи конструктивного доказательства изоморфизма между всеми тремя версиями (три теоремы, можно расчепить на 6 стрелок), и это будет прямо на первой секции курсов!

http://groupoid.space/mltt/types/path/