readme + annot fix

Kaptch · Jun 25, 2019 · fd7d73f · fd7d73f
1 parent 7e0040f
commit fd7d73f
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 82 deletions.
diff --git a/README.md b/README.md
@@ -1,77 +1,23 @@
-# Шаблон выпускной работы для студентов направления ФИИТ мехмата ЮФУ
+# Изоморфизм тривиального расслоения и семейства типов
+# Equivalence of family of types and fibration
 
-Это официальная версия шаблона для оформления
+Работа выполнена на основе [MMCS SFEDU thesis](https://github.com/mmcs-sfedu/mmcs_sfedu_thesis)
 
-* курсовой,
-* бакалаврской,
-* магистерской
+## Аннотация
 
-работ в [LaTeX](https://ru.wikipedia.org/wiki/LaTeX) для студентов направления ФИИТ [мехмата ЮФУ](http://mmcs.sfedu.ru/).
+Системы верификации --- программы, разработанные для формализации доказательств на компьютере. Большая часть из них базируется на теории типов, которая делится на множество подвидов.
+Гомотопическая теория типов (Homotopy type theory, HoTT) выделяется тем, что базируется на связи между теорией типов и теорией гомотопий. Эта область лежит в основе Унивалентных оснований математики (Univalent Foundation, UF) --- попытки формализовать математику, используя в качестве фундамента не множества, а гомотопические типы, а также высшие индуктивные типы (Higher Inductive Types, HIT). Этот подход интересен тем, что позволяет работать с гомотопической теорией, используя синтетический метод, то есть, не опираясь на более базовые примитивы, как, например, множества.
 
-Шаблон сделан на основе версии, [разработанной А.М.Пеленицыным для студентов мехмата ЮФУ](https://github.com/MMCS-SFEDU/mmcs_sfedu_thesis).
+В данный момент существует несколько систем верификации, которые поддерживают гомотопическую теорию типов нативно или благодаря расширениям, но эта поддержка обеспечивается различными наборами примитивных операций, для некоторых из которых существует совсем мало примеров.
+В работе рассматривается формализация нетривиального расслоения над окружностью --- ленты Мёбиуса, а также портирование доказательства изоморфизма тривиальных расслоений и зависимых типов на верификатор доказательств Arend. Это доказательство показывает, что базовые теоретико-типовые конструкции соответствуют гомотопическим.
 
-Результат, который можно получить с данным проектом,
-можно посмотреть здесь:
+Код, которому посвящена данная работа, можно найти на GitHub в репозитории организации Groupoid Infinity. Доказательство выполнено в файле [Fiber.ard](https://github.com/groupoid/arend/blob/master/src/Fiber.ard), формализация ленты Мёбиуса --- в файле [Moebius.ard](https://github.com/groupoid/arend/blob/master/src/Moebius.ard).
 
-[ ![](https://www.sharelatex.com/github/repos/MMCS-SFEDU/mmcs_sfedu_thesis/builds/latest/badge.svg)](https://www.sharelatex.com/github/repos/MMCS-SFEDU/mmcs_sfedu_thesis/builds/latest/output.pdf)
+## Annotation
 
-Чтобы попробовать этот проект на деле, проще всего пойти на сайт [overleaf.com](http://overleaf.com), создать там новый проект (“Create new paper”) и закачать все файлы нашего проекта в этот проект.
-
-Однако Overleaf работает очень медленно (есть даже
-[специальный тикет](http://support.overleaf.com/forums/137318-feedback/suggestions/7135647-make-compilation-faster)
-на их форуме поддержки: вы можете проголосовать за привлечение сил на ускорение).
-Для написания серьёзных
-работ рекомендуется проводить сборку проекта на локальном
-компьютере с использованием современного дистрибутива LaTeX,
-например, [TeX Live](https://www.tug.org/texlive/). По желанию
-можно использовать какую-либо
-[LaTeX IDE](https://ru.wikipedia.org/wiki/LaTeX#LaTeX-.D1.80.D0.B5.D0.B4.D0.B0.D0.BA.D1.82.D0.BE.D1.80.D1.8B)
-(в состав TeX Live входит IDE TeXworks) или любой редактор с
-подсветкой синтаксиса, (желательно) автодополнением и
-возможностью сборки с помощью `make` по горячей клавише.
-
-## Состав
-
-Большинство файлов проекта содержат достаточно подробные комментарии о своём назначении.
-Дадим краткое описание основных файлов, все они требуют редактирования (для последнего файла сперва хватит беглого знакомства с содержимым).
-
-* `main.tex`: основной текст работы.
-
-* `SETUP.tex`: информация об авторе и других формальных параметрах работы, в том числе о типе работы (один из трёх типов, перечисленных выше).
-
-* `biblio.bib`: список литературных и электронных источников,
-использованных в работе, в формате [BibTeX](https://ru.wikipedia.org/wiki/BibTeX).
-
-* `my_macro.tex`: несколько полезных макросов, которые могут понадобиться для набора текста (стоит с ними ознакомиться).
-
-Кроме того, в корневом каталоге проекта имеются:
-
-* `Makefile`: для упрощения сборки проекта с помощью утилиты [make](https://ru.wikipedia.org/wiki/Make). Полезно для тех, кто не использует специализированные IDE.
-
-* `preamble.tex`: преамбула документа. Для базового использования проекта изучение этого файла не требуется.
-
-* Каталог `core` с реализацией базового функционала в файлах:
-
-	* `appearance.tex`: настройка внешнего вида,
-	* `title_macro.tex`: настройка титульного листа,
-	* `theorem_styles.tex`: определение окружений типа «Определение», «Теорема»…
-
-	Для базового использования проекта изучение содержимого этого каталога не требуется.
-
-* Каталог `img` с иллюстрациями к работе.
-
-## Рекомендации пользователям Windows
-
-1. Скачайте и запустите
-	[установщик TeX Live](http://mirror.ctan.org/systems/texlive/tlnet/install-tl-windows.exe).
-
-2. Выберите самый полный вариант установки (Simple install (big) на данный,
-	2015 г., момент). Он потребует около 4 Гб, но избавит от дополнительных сложностей.
-
-3. После установки в меню *Пуск*/*Программы* должна появиться группа *TeX Live*. В ней можно открыть одну из двух опций для сборки проекта:
-	* TeXworks — очень скромный редактор с возможностью сборки по горячей клавише,
-	* TeX Live command-line — командная строка, в ней нужно переместиться в каталог проекта с помощью команды `cd путь` и выполнить команду сборки `make`. После этого в каталоге появится PDF файл.
-
-	Дополнительно к этим вариантам можно установить более продвинутую LaTeX IDE, например, [TeXnicCenter](http://www.texniccenter.org/).
+In this paper I report on formalizing a Moebius strip and on porting a proof of equivalence of fibration and family of types using the proof assistant Arend. The former task is a demonstration of basic Arend features and the latter is an evidence of a correspondence between basic constructions of homotopy and type theories. The code can be found in Arend Groupoid Infinity repository (moebius strip: [Moebius.ard](https://github.com/groupoid/arend/blob/master/src/Moebius.ard), proof: [Fiber.ard](https://github.com/groupoid/arend/blob/master/src/Fiber.ard).
 
+## Contacts
 
+mail: [email protected]
+tg: @kaptch
diff --git a/main.tex b/main.tex
@@ -1,13 +1,5 @@
-% В этом файле следует писать текст работы, разбивая его на
-% разделы (section), подразделы (subsection) и, если нужно,
-% главы (chapter).
-
-% Предварительно следует указать необходимую информацию
-% в файле SETUP.tex
-
 \input{preamble.tex}
 
-
 \NewBibliographyString{langjapanese}
 \NewBibliographyString{fromjapanese}
 
@@ -19,7 +11,7 @@
 Гомотопическая теория типов (Homotopy type theory, HoTT) выделяется тем, что базируется на связи между теорией типов и теорией гомотопий. Эта область лежит в основе Унивалентных оснований математики (Univalent Foundation, UF) --- попытки формализовать математику, используя в качестве фундамента не множества, а гомотопические типы или $\infty$-группоиды, а также высшие индуктивные типы (Higher Inductive Types, HIT). Этот подход интересен тем, что позволяет работать с гомотопической теорией, используя синтетический метод, то есть, не опираясь на более базовые примитивы, как, например, множества.
 
 В данный момент существует несколько систем верификации, которые поддерживают гомотопическую теорию типов нативно или благодаря расширениям, но эта поддержка обеспечивается различными наборами примитивных операций, для некоторых из которых существует совсем мало примеров.
-В работе рассматривается формализация нетривиального расслоения над окружностью --- ленты Мёбиуса, а также портирование доказательства изоморфизма тривиального расслоения и зависимого типа на верификатор доказательств Arend. Это доказательство показывает, что базовые теоретико-типовые конструкции соответствуют гомотопическим.
+В работе рассматривается формализация нетривиального расслоения над окружностью --- ленты Мёбиуса, а также портирование доказательства изоморфизма тривиальных расслоений и зависимых типов на верификатор доказательств Arend. Это доказательство показывает, что базовые теоретико-типовые конструкции соответствуют гомотопическим.
 
 Код, которому посвящена данная работа, можно найти на GitHub\autocite{Grp1} в репозитории организации Groupoid Infinity. Доказательство выполнено в файле Fiber.ard\autocite{Fiber}, формализация ленты Мёбиуса --- в файле Moebius.ard\autocite{Moebius}.
 
@@ -31,9 +23,9 @@
 
 There are several proof assistants, which support homotopy type theory natively or via extensions. Some of them are Coq\autocite{Coq}, Agda\autocite{Agda}, cubicaltt\autocite{Cubicaltt}, and redtt\autocite{Redtt}. They come with different sets of most basic operations. Some of these sets are studied better than others. Arend\autocite{Arend} is a proof assistant, which provides users with an interval type (a type that is inductively constructed from two terms, whose interpretation is as the endpoints of the interval, together with a path between them); an eliminator for an interval type---\textit{coe}, which allows, for every type over the interval, to transport elements from the fiber over left to the fiber over an arbitrary point; a dependent path type, which consists of all functions that maps elements of the interval type to the term of type parameterized by the given term of the interval type; and a function \textit{iso}, which can be used to define univalence---one of the cornerstones of homotopy type theory\autocite{Arenddocs}\autocite{nlab}.
 
-Homotopy type theory relies on the idea that type-theoretic constructions correspond to some equivalents from homotopy theory. E.g., the statement that the term $a$ is of type $A$, which is written as $a:A$, can be expressed as ``$A$ is a space and $a$ is a point of A''. In addition to the kinds of types and terms above, we also may consider types and terms with parameters. These are usually called \textit{dependent} types (or \textit{type families}) and terms (if $B$ is a type, then we might have a type $(x:B)\ E(x)$, which is parameterized by $B$). From the homotopy-theoretic point of view, we might think of such a type as a \textit{fibration} $E \to B$ over the space $B$. The fibration makes precise the idea of one space (\textit{fiber}) being parameterized by another (\textit{base}) with fibers being equivalent in some coherent way. % actually homotopy equivalent
+Homotopy type theory relies on the idea that type-theoretic constructions correspond to some equivalents from homotopy theory. E.g., the statement that the term $a$ is of type $A$, which is written as $a:A$, can be expressed as ``$A$ is a space and $a$ is a point of A''. In addition to the kinds of types and terms above, we also may consider types and terms with parameters. These are usually called \textit{dependent} types (or \textit{type families}) and terms (if $B$ is a type, then we might have a type $(x:B)\ E(x)$, which is parameterized by $B$). From the homotopy-theoretic point of view, we might think of such a type as a \textit{fibration} $E \to B$ over the space $B$. The fibration makes precise the idea of one space (\textit{fiber}) being parameterized by another (\textit{base}) with fibers being equivalent in some coherent way.
 
-In this paper I report on formalizing a Moebius strip and on porting a proof of equivalence between the fibration and the type family using the proof assistant Arend. The former task is a demonstration of basic Arend features and the latter is an evidence of a correspondence between basic constructions of homotopy and type theories. The code can be found in Arend Groupoid Infinity repository (moebius strip: Moebius.ard\autocite{Moebius}, proof: Fiber.ard\autocite{Fiber}).
+In this paper I report on formalizing a Moebius strip and on porting a proof of equivalence of the fibration and the family of types using the proof assistant Arend. The former task is a demonstration of basic Arend features and the latter is an evidence of a correspondence between basic constructions of homotopy theory and type theory. The code can be found in Arend Groupoid Infinity repository (moebius strip: Moebius.ard\autocite{Moebius}, proof: Fiber.ard\autocite{Fiber}).
 
 \section{Preliminaries}
 
@@ -246,7 +238,7 @@ \section{Isomorphism between a fibration and a dependent type}
 \end{lstlisting}
 \end{ListingEnv}
 
-Now we need to define mutually inverse functions between the type that represents a type family and the type that represents a trivial fibration. 
+Now we need to define mutually inverse functions between the type that represents a family of types and the type that represents a trivial fibration. 
 
 \begin{ListingEnv}[H]
 \begin{lstlisting}
@@ -384,8 +376,8 @@ \section{Isomorphism between a fibration and a dependent type}
 In this paper I provided the proof of a correspondence between dependent types---basic type theoretic constructions, and fibrations---basic homotopy theoretic constructions in the proof-assistant Arend. This correspondence shows that working on homotopy theory can be approached syntactically if using type theory with ease, because there is no need for complex definitions of the simplest homotopy construction.
 
 \begin{otherlanguage}{english}
-\printbibliography[%{}
-    heading=bibintoc%
+\printbibliography[
+    heading=bibintoc
     ,title=Bibliography
 ]
 \end{otherlanguage}