Anatoly Levenchuk (ailev) wrote,
Anatoly Levenchuk
ailev

Category:

Унивалентные основания математики

Вот страничка материалов про унивалентные основания математики Владимира Воеводского: http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html -- язык Coq, классы не как sets, а как homotopy types, теория категорий. Далее -- Eventually it became clear to me that the univalent semantics is just a first step and that I am really working on new foundations of mathematics.

Меня чем дальше, тем больше интересуют подходы к классам, в которых они не являются множествами. Связанный с этим парадокс -- что простые смертные классами-не-множествами как раз и думают (http://ailev.livejournal.com/1007293.html), но предлагаемые математикой и компьютерной наукой формализмы этих "не-множеств" простым смертным недоступны.
Subscribe

  • Вычислительное мышление: пять тем для отслеживания в 2021

    Некоторые темы для отслеживания и размышлений на досуге. При этом охотно верю, что у кого-то это идеи для размышления в рабочее время. Вот кто сидит…

  • lytdybr

    Удивляюсь, почему не обсуждаются причины, а только следствия типа "а чего они законы нарушают": не обсуждаются право народа на собрания (с чего это…

  • lytdybr

    Делаю рабочую тетрадь к курсу системного менеджмента: то, что лекции отличает от учебного курса -- тренажёрные вопросы, упражнения, задания. Написал…

  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

  • 49 comments

  • Вычислительное мышление: пять тем для отслеживания в 2021

    Некоторые темы для отслеживания и размышлений на досуге. При этом охотно верю, что у кого-то это идеи для размышления в рабочее время. Вот кто сидит…

  • lytdybr

    Удивляюсь, почему не обсуждаются причины, а только следствия типа "а чего они законы нарушают": не обсуждаются право народа на собрания (с чего это…

  • lytdybr

    Делаю рабочую тетрадь к курсу системного менеджмента: то, что лекции отличает от учебного курса -- тренажёрные вопросы, упражнения, задания. Написал…