Commits

Anonymous committed f17e89c

initial

  • Participants

Comments (0)

Files changed (7)

+.agdai
+

File FirstConcepts.agda

+module FirstConcepts where
+{- 
+ Agda работает с типами. Типы - это такие наборы. Как множества. Agda позволяет нам определять 
+ новые типы. Начнем мы с типа, не содежращего ничего -}
+
+private
+  -- В дальнейшем мы изменим определения, которые даём здесь, поэтому 
+  -- писать будем в private - блоке. Имена из него не будут видны снаружи
+  data ∅ : Set where
+
+{-
+--------- Меняя мир морфизм за морфизмом ------------
+Как с нуля построить инструмент моделирования, анализа и программирования
+
+Мы начнем создавать формализм теории категорий и применять его к самому себе
+и окружающему миру. Начать можно было бы с естественного языка, но на нем
+очень легко ошибаться. Поэтому начнем мы с сочетания естественного языка 
+и существующего формализма - теории типов Пера Мартина-Лёффа в его реализации в 
+системе Agda.
+
+Мы постараемся использовать абсолютный минимум от Agda, как можно раньше переходя
+на собственный, создаваемый формализм. Мы практически не будем использовать стандартную
+библиотеку. Целью не является изучение Agda. Все используемые конструкции будут объясняться
+на естественном языке ровно в том объеме, который нам необходим
+-} 
+
+-- Основные понятия Agda
+import FirstConcepts

File html/Agda.Primitive.html

+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml"
+><head
+  ><title
+    >Agda.Primitive</title
+    ><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"
+     /><meta http-equiv="Content-Style-Type" content="text/css"
+     /><link href="Agda.css" rel="stylesheet" type="text/css"
+     /></head
+  ><body
+  ><pre
+    ><a name="1" class="Comment"
+      >-- The Agda primitives (preloaded).</a
+      ><a name="36"
+      >
+
+</a
+      ><a name="38" class="Keyword"
+      >module</a
+      ><a name="44"
+      > </a
+      ><a name="45" href="Agda.Primitive.html#1" class="Module"
+      >Agda.Primitive</a
+      ><a name="59"
+      > </a
+      ><a name="60" class="Keyword"
+      >where</a
+      ><a name="65"
+      >
+
+</a
+      ><a name="67" class="Comment"
+      >------------------------------------------------------------------------</a
+      ><a name="139"
+      >
+</a
+      ><a name="140" class="Comment"
+      >-- Universe levels</a
+      ><a name="158"
+      >
+</a
+      ><a name="159" class="Comment"
+      >------------------------------------------------------------------------</a
+      ><a name="231"
+      >
+
+</a
+      ><a name="233" class="Keyword"
+      >infixl</a
+      ><a name="239"
+      > </a
+      ><a name="240" class="Number"
+      >6</a
+      ><a name="241"
+      > _&#8852;_
+
+</a
+      ><a name="247" class="Comment"
+      >-- Level is the first thing we need to define.</a
+      ><a name="293"
+      >
+</a
+      ><a name="294" class="Comment"
+      >-- The other postulates can only be checked if built-in Level is known.</a
+      ><a name="365"
+      >
+
+</a
+      ><a name="367" class="Keyword"
+      >postulate</a
+      ><a name="376"
+      >
+  </a
+      ><a name="379" href="Agda.Primitive.html#379" class="Postulate"
+      >Level</a
+      ><a name="384"
+      > </a
+      ><a name="385" class="Symbol"
+      >:</a
+      ><a name="386"
+      > </a
+      ><a name="387" class="PrimitiveType"
+      >Set</a
+      ><a name="390"
+      >
+
+</a
+      ><a name="392" class="Comment"
+      >-- MAlonzo compiles Level to (). This should be safe, because it is</a
+      ><a name="459"
+      >
+</a
+      ><a name="460" class="Comment"
+      >-- not possible to pattern match on levels.</a
+      ><a name="503"
+      >
+
+</a
+      ><a name="505" class="Symbol"
+      >{-#</a
+      ><a name="508"
+      > </a
+      ><a name="509" class="Keyword"
+      >COMPILED_TYPE</a
+      ><a name="522"
+      > </a
+      ><a name="523" href="Agda.Primitive.html#379" class="Postulate"
+      >Level</a
+      ><a name="528"
+      > () </a
+      ><a name="532" class="Symbol"
+      >#-}</a
+      ><a name="535"
+      >
+</a
+      ><a name="536" class="Symbol"
+      >{-#</a
+      ><a name="539"
+      > </a
+      ><a name="540" class="Keyword"
+      >BUILTIN</a
+      ><a name="547"
+      > LEVEL </a
+      ><a name="554" href="Agda.Primitive.html#379" class="Postulate"
+      >Level</a
+      ><a name="559"
+      >    </a
+      ><a name="563" class="Symbol"
+      >#-}</a
+      ><a name="566"
+      >
+
+</a
+      ><a name="568" class="Keyword"
+      >postulate</a
+      ><a name="577"
+      >
+  </a
+      ><a name="580" href="Agda.Primitive.html#580" class="Postulate"
+      >lzero</a
+      ><a name="585"
+      > </a
+      ><a name="586" class="Symbol"
+      >:</a
+      ><a name="587"
+      > </a
+      ><a name="588" href="Agda.Primitive.html#379" class="Postulate"
+      >Level</a
+      ><a name="593"
+      >
+  </a
+      ><a name="596" href="Agda.Primitive.html#596" class="Postulate"
+      >lsuc</a
+      ><a name="600"
+      >  </a
+      ><a name="602" class="Symbol"
+      >:</a
+      ><a name="603"
+      > </a
+      ><a name="604" class="Symbol"
+      >(</a
+      ><a name="605" href="Agda.Primitive.html#605" class="Bound"
+      >&#8467;</a
+      ><a name="606"
+      > </a
+      ><a name="607" class="Symbol"
+      >:</a
+      ><a name="608"
+      > </a
+      ><a name="609" href="Agda.Primitive.html#379" class="Postulate"
+      >Level</a
+      ><a name="614" class="Symbol"
+      >)</a
+      ><a name="615"
+      > </a
+      ><a name="616" class="Symbol"
+      >&#8594;</a
+      ><a name="617"
+      > </a
+      ><a name="618" href="Agda.Primitive.html#379" class="Postulate"
+      >Level</a
+      ><a name="623"
+      >
+  </a
+      ><a name="626" href="Agda.Primitive.html#626" class="Postulate Operator"
+      >_&#8852;_</a
+      ><a name="629"
+      >   </a
+      ><a name="632" class="Symbol"
+      >:</a
+      ><a name="633"
+      > </a
+      ><a name="634" class="Symbol"
+      >(</a
+      ><a name="635" href="Agda.Primitive.html#635" class="Bound"
+      >&#8467;&#8321;</a
+      ><a name="637"
+      > </a
+      ><a name="638" href="Agda.Primitive.html#638" class="Bound"
+      >&#8467;&#8322;</a
+      ><a name="640"
+      > </a
+      ><a name="641" class="Symbol"
+      >:</a
+      ><a name="642"
+      > </a
+      ><a name="643" href="Agda.Primitive.html#379" class="Postulate"
+      >Level</a
+      ><a name="648" class="Symbol"
+      >)</a
+      ><a name="649"
+      > </a
+      ><a name="650" class="Symbol"
+      >&#8594;</a
+      ><a name="651"
+      > </a
+      ><a name="652" href="Agda.Primitive.html#379" class="Postulate"
+      >Level</a
+      ><a name="657"
+      >
+
+</a
+      ><a name="659" class="Symbol"
+      >{-#</a
+      ><a name="662"
+      > </a
+      ><a name="663" class="Keyword"
+      >COMPILED</a
+      ><a name="671"
+      > </a
+      ><a name="672" href="Agda.Primitive.html#580" class="Postulate"
+      >lzero</a
+      ><a name="677"
+      > ()           </a
+      ><a name="691" class="Symbol"
+      >#-}</a
+      ><a name="694"
+      >
+</a
+      ><a name="695" class="Symbol"
+      >{-#</a
+      ><a name="698"
+      > </a
+      ><a name="699" class="Keyword"
+      >COMPILED</a
+      ><a name="707"
+      > </a
+      ><a name="708" href="Agda.Primitive.html#596" class="Postulate"
+      >lsuc</a
+      ><a name="712"
+      >  (\_ -&gt; ())   </a
+      ><a name="727" class="Symbol"
+      >#-}</a
+      ><a name="730"
+      >
+</a
+      ><a name="731" class="Symbol"
+      >{-#</a
+      ><a name="734"
+      > </a
+      ><a name="735" class="Keyword"
+      >COMPILED</a
+      ><a name="743"
+      > </a
+      ><a name="744" href="Agda.Primitive.html#626" class="Postulate Operator"
+      >_&#8852;_</a
+      ><a name="747"
+      >   (\_ _ -&gt; ()) </a
+      ><a name="763" class="Symbol"
+      >#-}</a
+      ><a name="766"
+      >
+
+</a
+      ><a name="768" class="Symbol"
+      >{-#</a
+      ><a name="771"
+      > </a
+      ><a name="772" class="Keyword"
+      >BUILTIN</a
+      ><a name="779"
+      > LEVELZERO </a
+      ><a name="790" href="Agda.Primitive.html#580" class="Primitive"
+      >lzero</a
+      ><a name="795"
+      > </a
+      ><a name="796" class="Symbol"
+      >#-}</a
+      ><a name="799"
+      >
+</a
+      ><a name="800" class="Symbol"
+      >{-#</a
+      ><a name="803"
+      > </a
+      ><a name="804" class="Keyword"
+      >BUILTIN</a
+      ><a name="811"
+      > LEVELSUC  </a
+      ><a name="822" href="Agda.Primitive.html#596" class="Primitive"
+      >lsuc</a
+      ><a name="826"
+      >  </a
+      ><a name="828" class="Symbol"
+      >#-}</a
+      ><a name="831"
+      >
+</a
+      ><a name="832" class="Symbol"
+      >{-#</a
+      ><a name="835"
+      > </a
+      ><a name="836" class="Keyword"
+      >BUILTIN</a
+      ><a name="843"
+      > LEVELMAX  </a
+      ><a name="854" href="Agda.Primitive.html#626" class="Primitive Operator"
+      >_&#8852;_</a
+      ><a name="857"
+      >   </a
+      ><a name="860" class="Symbol"
+      >#-}</a
+      ><a name="863"
+      >
+</a
+      ></pre
+    ></body
+  ></html
+>

File html/Agda.css

+/* Aspects. */
+.Comment       { color: #B22222 }
+.Keyword       { color: #CD6600 }
+.String        { color: #B22222 }
+.Number        { color: #A020F0 }
+.Symbol        { color: #404040 }
+.PrimitiveType { color: #0000CD }
+.Operator      {}
+
+/* NameKinds. */
+.Bound                  { color: black   }
+.InductiveConstructor   { color: #008B00 }
+.CoinductiveConstructor { color: #8B7500 }
+.Datatype               { color: #0000CD }
+.Field                  { color: #EE1289 }
+.Function               { color: #0000CD }
+.Module                 { color: #A020F0 }
+.Postulate              { color: #0000CD }
+.Primitive              { color: #0000CD }
+.Record                 { color: #0000CD }
+
+/* OtherAspects. */
+.DottedPattern      {}
+.UnsolvedMeta       { color: black; background: yellow         }
+.UnsolvedConstraint { color: black; background: yellow         }
+.TerminationProblem { color: black; background: #FFA07A        }
+.IncompletePattern  { color: black; background: #F5DEB3        }
+.Error              { color: red;   text-decoration: underline }
+.TypeChecks         { color: black; background: #ADD8E6        }
+
+/* Standard attributes. */
+a { text-decoration: none }
+a[href]:hover { background-color: #B4EEB4 }

File html/FirstConcepts.html

+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml"
+><head
+  ><title
+    >FirstConcepts</title
+    ><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"
+     /><meta http-equiv="Content-Style-Type" content="text/css"
+     /><link href="Agda.css" rel="stylesheet" type="text/css"
+     /></head
+  ><body
+  ><pre
+    ><a name="1" class="Keyword"
+      >module</a
+      ><a name="7"
+      > </a
+      ><a name="8" href="FirstConcepts.html#1" class="Module"
+      >FirstConcepts</a
+      ><a name="21"
+      > </a
+      ><a name="22" class="Keyword"
+      >where</a
+      ><a name="27"
+      >
+</a
+      ><a name="28" class="Comment"
+      >{- 
+ Agda &#1088;&#1072;&#1073;&#1086;&#1090;&#1072;&#1077;&#1090; &#1089; &#1090;&#1080;&#1087;&#1072;&#1084;&#1080;. &#1058;&#1080;&#1087;&#1099; - &#1101;&#1090;&#1086; &#1090;&#1072;&#1082;&#1080;&#1077; &#1085;&#1072;&#1073;&#1086;&#1088;&#1099;. &#1050;&#1072;&#1082; &#1084;&#1085;&#1086;&#1078;&#1077;&#1089;&#1090;&#1074;&#1072;. Agda &#1087;&#1086;&#1079;&#1074;&#1086;&#1083;&#1103;&#1077;&#1090; &#1085;&#1072;&#1084; &#1086;&#1087;&#1088;&#1077;&#1076;&#1077;&#1083;&#1103;&#1090;&#1100; 
+ &#1085;&#1086;&#1074;&#1099;&#1077; &#1090;&#1080;&#1087;&#1099;. &#1053;&#1072;&#1095;&#1085;&#1077;&#1084; &#1084;&#1099; &#1089; &#1090;&#1080;&#1087;&#1072;, &#1085;&#1077; &#1089;&#1086;&#1076;&#1077;&#1078;&#1088;&#1072;&#1097;&#1077;&#1075;&#1086; &#1085;&#1080;&#1095;&#1077;&#1075;&#1086; -}</a
+      ><a name="183"
+      >
+
+</a
+      ><a name="185" class="Keyword"
+      >private</a
+      ><a name="192"
+      >
+  </a
+      ><a name="195" class="Comment"
+      >-- &#1042; &#1076;&#1072;&#1083;&#1100;&#1085;&#1077;&#1081;&#1096;&#1077;&#1084; &#1084;&#1099; &#1080;&#1079;&#1084;&#1077;&#1085;&#1080;&#1084; &#1086;&#1087;&#1088;&#1077;&#1076;&#1077;&#1083;&#1077;&#1085;&#1080;&#1103;, &#1082;&#1086;&#1090;&#1086;&#1088;&#1099;&#1077; &#1076;&#1072;&#1105;&#1084; &#1079;&#1076;&#1077;&#1089;&#1100;, &#1087;&#1086;&#1101;&#1090;&#1086;&#1084;&#1091; </a
+      ><a name="263"
+      >
+  </a
+      ><a name="266" class="Comment"
+      >-- &#1087;&#1080;&#1089;&#1072;&#1090;&#1100; &#1073;&#1091;&#1076;&#1077;&#1084; &#1074; private - &#1073;&#1083;&#1086;&#1082;&#1077;. &#1048;&#1084;&#1077;&#1085;&#1072; &#1080;&#1079; &#1085;&#1077;&#1075;&#1086; &#1085;&#1077; &#1073;&#1091;&#1076;&#1091;&#1090; &#1074;&#1080;&#1076;&#1085;&#1099; &#1089;&#1085;&#1072;&#1088;&#1091;&#1078;&#1080;</a
+      ><a name="337"
+      >
+  </a
+      ><a name="340" class="Keyword"
+      >data</a
+      ><a name="344"
+      > </a
+      ><a name="345" href="FirstConcepts.html#345" class="Datatype"
+      >&#8709;</a
+      ><a name="346"
+      > </a
+      ><a name="347" class="Symbol"
+      >:</a
+      ><a name="348"
+      > </a
+      ><a name="349" class="PrimitiveType"
+      >Set</a
+      ><a name="352"
+      > </a
+      ><a name="353" class="Keyword"
+      >where</a
+      ><a name="358"
+      >
+
+</a
+      ></pre
+    ></body
+  ></html
+>

File html/Main.html

+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml"
+><head
+  ><title
+    >Main</title
+    ><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"
+     /><meta http-equiv="Content-Style-Type" content="text/css"
+     /><link href="Agda.css" rel="stylesheet" type="text/css"
+     /></head
+  ><body
+  ><pre
+    ><a name="1" class="Comment"
+      >{-
+--------- &#1052;&#1077;&#1085;&#1103;&#1103; &#1084;&#1080;&#1088; &#1084;&#1086;&#1088;&#1092;&#1080;&#1079;&#1084; &#1079;&#1072; &#1084;&#1086;&#1088;&#1092;&#1080;&#1079;&#1084;&#1086;&#1084; ------------
+&#1050;&#1072;&#1082; &#1089; &#1085;&#1091;&#1083;&#1103; &#1087;&#1086;&#1089;&#1090;&#1088;&#1086;&#1080;&#1090;&#1100; &#1080;&#1085;&#1089;&#1090;&#1088;&#1091;&#1084;&#1077;&#1085;&#1090; &#1084;&#1086;&#1076;&#1077;&#1083;&#1080;&#1088;&#1086;&#1074;&#1072;&#1085;&#1080;&#1103;, &#1072;&#1085;&#1072;&#1083;&#1080;&#1079;&#1072; &#1080; &#1087;&#1088;&#1086;&#1075;&#1088;&#1072;&#1084;&#1084;&#1080;&#1088;&#1086;&#1074;&#1072;&#1085;&#1080;&#1103;
+
+&#1052;&#1099; &#1085;&#1072;&#1095;&#1085;&#1077;&#1084; &#1089;&#1086;&#1079;&#1076;&#1072;&#1074;&#1072;&#1090;&#1100; &#1092;&#1086;&#1088;&#1084;&#1072;&#1083;&#1080;&#1079;&#1084; &#1090;&#1077;&#1086;&#1088;&#1080;&#1080; &#1082;&#1072;&#1090;&#1077;&#1075;&#1086;&#1088;&#1080;&#1081; &#1080; &#1087;&#1088;&#1080;&#1084;&#1077;&#1085;&#1103;&#1090;&#1100; &#1077;&#1075;&#1086; &#1082; &#1089;&#1072;&#1084;&#1086;&#1084;&#1091; &#1089;&#1077;&#1073;&#1077;
+&#1080; &#1086;&#1082;&#1088;&#1091;&#1078;&#1072;&#1102;&#1097;&#1077;&#1084;&#1091; &#1084;&#1080;&#1088;&#1091;. &#1053;&#1072;&#1095;&#1072;&#1090;&#1100; &#1084;&#1086;&#1078;&#1085;&#1086; &#1073;&#1099;&#1083;&#1086; &#1073;&#1099; &#1089; &#1077;&#1089;&#1090;&#1077;&#1089;&#1090;&#1074;&#1077;&#1085;&#1085;&#1086;&#1075;&#1086; &#1103;&#1079;&#1099;&#1082;&#1072;, &#1085;&#1086; &#1085;&#1072; &#1085;&#1077;&#1084;
+&#1086;&#1095;&#1077;&#1085;&#1100; &#1083;&#1077;&#1075;&#1082;&#1086; &#1086;&#1096;&#1080;&#1073;&#1072;&#1090;&#1100;&#1089;&#1103;. &#1055;&#1086;&#1101;&#1090;&#1086;&#1084;&#1091; &#1085;&#1072;&#1095;&#1085;&#1077;&#1084; &#1084;&#1099; &#1089; &#1089;&#1086;&#1095;&#1077;&#1090;&#1072;&#1085;&#1080;&#1103; &#1077;&#1089;&#1090;&#1077;&#1089;&#1090;&#1074;&#1077;&#1085;&#1085;&#1086;&#1075;&#1086; &#1103;&#1079;&#1099;&#1082;&#1072; 
+&#1080; &#1089;&#1091;&#1097;&#1077;&#1089;&#1090;&#1074;&#1091;&#1102;&#1097;&#1077;&#1075;&#1086; &#1092;&#1086;&#1088;&#1084;&#1072;&#1083;&#1080;&#1079;&#1084;&#1072; - &#1090;&#1077;&#1086;&#1088;&#1080;&#1080; &#1090;&#1080;&#1087;&#1086;&#1074; &#1055;&#1077;&#1088;&#1072; &#1052;&#1072;&#1088;&#1090;&#1080;&#1085;&#1072;-&#1051;&#1105;&#1092;&#1092;&#1072; &#1074; &#1077;&#1075;&#1086; &#1088;&#1077;&#1072;&#1083;&#1080;&#1079;&#1072;&#1094;&#1080;&#1080; &#1074; 
+&#1089;&#1080;&#1089;&#1090;&#1077;&#1084;&#1077; Agda.
+
+&#1052;&#1099; &#1087;&#1086;&#1089;&#1090;&#1072;&#1088;&#1072;&#1077;&#1084;&#1089;&#1103; &#1080;&#1089;&#1087;&#1086;&#1083;&#1100;&#1079;&#1086;&#1074;&#1072;&#1090;&#1100; &#1072;&#1073;&#1089;&#1086;&#1083;&#1102;&#1090;&#1085;&#1099;&#1081; &#1084;&#1080;&#1085;&#1080;&#1084;&#1091;&#1084; &#1086;&#1090; Agda, &#1082;&#1072;&#1082; &#1084;&#1086;&#1078;&#1085;&#1086; &#1088;&#1072;&#1085;&#1100;&#1096;&#1077; &#1087;&#1077;&#1088;&#1077;&#1093;&#1086;&#1076;&#1103;
+&#1085;&#1072; &#1089;&#1086;&#1073;&#1089;&#1090;&#1074;&#1077;&#1085;&#1085;&#1099;&#1081;, &#1089;&#1086;&#1079;&#1076;&#1072;&#1074;&#1072;&#1077;&#1084;&#1099;&#1081; &#1092;&#1086;&#1088;&#1084;&#1072;&#1083;&#1080;&#1079;&#1084;. &#1052;&#1099; &#1087;&#1088;&#1072;&#1082;&#1090;&#1080;&#1095;&#1077;&#1089;&#1082;&#1080; &#1085;&#1077; &#1073;&#1091;&#1076;&#1077;&#1084; &#1080;&#1089;&#1087;&#1086;&#1083;&#1100;&#1079;&#1086;&#1074;&#1072;&#1090;&#1100; &#1089;&#1090;&#1072;&#1085;&#1076;&#1072;&#1088;&#1090;&#1085;&#1091;&#1102;
+&#1073;&#1080;&#1073;&#1083;&#1080;&#1086;&#1090;&#1077;&#1082;&#1091;. &#1062;&#1077;&#1083;&#1100;&#1102; &#1085;&#1077; &#1103;&#1074;&#1083;&#1103;&#1077;&#1090;&#1089;&#1103; &#1080;&#1079;&#1091;&#1095;&#1077;&#1085;&#1080;&#1077; Agda. &#1042;&#1089;&#1077; &#1080;&#1089;&#1087;&#1086;&#1083;&#1100;&#1079;&#1091;&#1077;&#1084;&#1099;&#1077; &#1082;&#1086;&#1085;&#1089;&#1090;&#1088;&#1091;&#1082;&#1094;&#1080;&#1080; &#1073;&#1091;&#1076;&#1091;&#1090; &#1086;&#1073;&#1098;&#1103;&#1089;&#1085;&#1103;&#1090;&#1100;&#1089;&#1103;
+&#1085;&#1072; &#1077;&#1089;&#1090;&#1077;&#1089;&#1090;&#1074;&#1077;&#1085;&#1085;&#1086;&#1084; &#1103;&#1079;&#1099;&#1082;&#1077; &#1088;&#1086;&#1074;&#1085;&#1086; &#1074; &#1090;&#1086;&#1084; &#1086;&#1073;&#1098;&#1077;&#1084;&#1077;, &#1082;&#1086;&#1090;&#1086;&#1088;&#1099;&#1081; &#1085;&#1072;&#1084; &#1085;&#1077;&#1086;&#1073;&#1093;&#1086;&#1076;&#1080;&#1084;
+-}</a
+      ><a name="782"
+      > 
+
+</a
+      ><a name="785" class="Comment"
+      >-- &#1054;&#1089;&#1085;&#1086;&#1074;&#1085;&#1099;&#1077; &#1087;&#1086;&#1085;&#1103;&#1090;&#1080;&#1103; Agda</a
+      ><a name="809"
+      >
+</a
+      ><a name="810" class="Keyword"
+      >import</a
+      ><a name="816"
+      > </a
+      ><a name="817" href="FirstConcepts.html#1" class="Module"
+      >FirstConcepts</a
+      ></pre
+    ></body
+  ></html
+>