Commits

Anonymous committed 96c680d

Curry-Howard

Comments (0)

Files changed (4)

 
 ∅ : {ℓ : _} → Category ℓ
 ∅ {ℓ} = record
-          { Obj = ∅-type
+          { Obj = ∅-type
           ; _⇒_ = λ a → λ ()
           ; _≈_ = λ {o₁} → λ {}
           ; id = λ {}

FirstConcepts.agda

    Теперь мы снова определим пустой тип, но уже для всех уровней сразу:
   -}
 
-data ∅ (ℓ : Level) : Set ℓ where
+data ∅ {ℓ : Level} : Set ℓ where
 
 -- Таким образом, для любого уровня ℓ имеется пустой тип на этом уровне
 
+module Main where
 {-
 --------- Меняя мир морфизм за морфизмом ------------
 Как с нуля построить инструмент моделирования, анализа и программирования
 Чтобы перейти к содержимому этого модуля, можно щелкнуть на его имени.
 -} 
 
--- Основные понятия Agda и пустой тип ∅
-import FirstConcepts
--- Семейства типов. Функции. Отношения
-import Relations
--- Записи, отношение эквивалентности
-import  Equivalence
--- Пропозициональная эквивалентность (тождественность)
-import PropositionalEquivalence
--- Ура ! понятие категории!
-import Category
+module Agda where
+    -- Основные понятия Agda и пустой тип ∅
+    import FirstConcepts
+
+    -- Curry-Howard correspondence. Типы как утверждения. 
+    import CurryHoward
+    -- Семейства типов. Функции. Отношения
+    import Relations
+    -- Записи, отношение эквивалентности
+    import  Equivalence
+    -- Пропозициональная эквивалентность (тождественность)
+    import PropositionalEquivalence
+
+module Categories where
+   -- Ура ! понятие категории!
+  import Category
 -- К этому моменту у нас есть понятие о мире категорий и первый представитель этого мира
 -- Мы уже можем начать его продуктивно изучать. 
--- Дальнейший план: категория Hom, категория Cat (категория категорий), примеры категорий .
+  module ConstructionsInCategoryTheory where
+  module ExamplesOfCategories where
      /></head
   ><body
   ><pre
-    ><a name="1" class="Comment"
+    ><a name="1" class="Keyword"
+      >module</a
+      ><a name="7"
+      > </a
+      ><a name="8" href="Main.html#1" class="Module"
+      >Main</a
+      ><a name="12"
+      > </a
+      ><a name="13" class="Keyword"
+      >where</a
+      ><a name="18"
+      >
+</a
+      ><a name="19" 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;&#1085;&#1086;&#1075;&#1080;&#1077; &#1074;&#1077;&#1097;&#1080; &#1074; &#1090;&#1077;&#1082;&#1089;&#1090;&#1077; &#1103;&#1074;&#1083;&#1103;&#1102;&#1090;&#1089;&#1103; &#1089;&#1089;&#1099;&#1083;&#1082;&#1072;&#1084;&#1080;. &#1053;&#1080;&#1078;&#1077; &#1084;&#1099; &#1074;&#1082;&#1083;&#1102;&#1095;&#1072;&#1077;&#1084; &#1084;&#1086;&#1076;&#1091;&#1083;&#1100; FirstConcepts.
 &#1063;&#1090;&#1086;&#1073;&#1099; &#1087;&#1077;&#1088;&#1077;&#1081;&#1090;&#1080; &#1082; &#1089;&#1086;&#1076;&#1077;&#1088;&#1078;&#1080;&#1084;&#1086;&#1084;&#1091; &#1101;&#1090;&#1086;&#1075;&#1086; &#1084;&#1086;&#1076;&#1091;&#1083;&#1103;, &#1084;&#1086;&#1078;&#1085;&#1086; &#1097;&#1077;&#1083;&#1082;&#1085;&#1091;&#1090;&#1100; &#1085;&#1072; &#1077;&#1075;&#1086; &#1080;&#1084;&#1077;&#1085;&#1080;.
 -}</a
-      ><a name="934"
+      ><a name="952"
       > 
 
 </a
-      ><a name="937" class="Comment"
+      ><a name="955" class="Keyword"
+      >module</a
+      ><a name="961"
+      > </a
+      ><a name="962" href="Main.html#962" class="Module"
+      >Agda</a
+      ><a name="966"
+      > </a
+      ><a name="967" class="Keyword"
+      >where</a
+      ><a name="972"
+      >
+    </a
+      ><a name="977" class="Comment"
       >-- &#1054;&#1089;&#1085;&#1086;&#1074;&#1085;&#1099;&#1077; &#1087;&#1086;&#1085;&#1103;&#1090;&#1080;&#1103; Agda &#1080; &#1087;&#1091;&#1089;&#1090;&#1086;&#1081; &#1090;&#1080;&#1087; &#8709;</a
-      ><a name="976"
+      ><a name="1016"
+      >
+    </a
+      ><a name="1021" class="Keyword"
+      >import</a
+      ><a name="1027"
+      > </a
+      ><a name="1028" href="FirstConcepts.html#1" class="Module"
+      >FirstConcepts</a
+      ><a name="1041"
+      >
+
+    </a
+      ><a name="1047" class="Comment"
+      >-- Curry-Howard correspondence. &#1058;&#1080;&#1087;&#1099; &#1082;&#1072;&#1082; &#1091;&#1090;&#1074;&#1077;&#1088;&#1078;&#1076;&#1077;&#1085;&#1080;&#1103;. </a
+      ><a name="1101"
+      >
+    </a
+      ><a name="1106" class="Keyword"
+      >import</a
+      ><a name="1112"
+      > </a
+      ><a name="1113" href="CurryHoward.html#1" class="Module"
+      >CurryHoward</a
+      ><a name="1124"
+      >
+    </a
+      ><a name="1129" class="Comment"
+      >-- &#1057;&#1077;&#1084;&#1077;&#1081;&#1089;&#1090;&#1074;&#1072; &#1090;&#1080;&#1087;&#1086;&#1074;. &#1060;&#1091;&#1085;&#1082;&#1094;&#1080;&#1080;. &#1054;&#1090;&#1085;&#1086;&#1096;&#1077;&#1085;&#1080;&#1103;</a
+      ><a name="1167"
+      >
+    </a
+      ><a name="1172" class="Keyword"
+      >import</a
+      ><a name="1178"
+      > </a
+      ><a name="1179" href="Relations.html#1" class="Module"
+      >Relations</a
+      ><a name="1188"
+      >
+    </a
+      ><a name="1193" class="Comment"
+      >-- &#1047;&#1072;&#1087;&#1080;&#1089;&#1080;, &#1086;&#1090;&#1085;&#1086;&#1096;&#1077;&#1085;&#1080;&#1077; &#1101;&#1082;&#1074;&#1080;&#1074;&#1072;&#1083;&#1077;&#1085;&#1090;&#1085;&#1086;&#1089;&#1090;&#1080;</a
+      ><a name="1229"
+      >
+    </a
+      ><a name="1234" class="Keyword"
+      >import</a
+      ><a name="1240"
+      >  </a
+      ><a name="1242" href="Equivalence.html#1" class="Module"
+      >Equivalence</a
+      ><a name="1253"
+      >
+    </a
+      ><a name="1258" class="Comment"
+      >-- &#1055;&#1088;&#1086;&#1087;&#1086;&#1079;&#1080;&#1094;&#1080;&#1086;&#1085;&#1072;&#1083;&#1100;&#1085;&#1072;&#1103; &#1101;&#1082;&#1074;&#1080;&#1074;&#1072;&#1083;&#1077;&#1085;&#1090;&#1085;&#1086;&#1089;&#1090;&#1100; (&#1090;&#1086;&#1078;&#1076;&#1077;&#1089;&#1090;&#1074;&#1077;&#1085;&#1085;&#1086;&#1089;&#1090;&#1100;)</a
+      ><a name="1312"
+      >
+    </a
+      ><a name="1317" class="Keyword"
+      >import</a
+      ><a name="1323"
+      > </a
+      ><a name="1324" href="PropositionalEquivalence.html#1" class="Module"
+      >PropositionalEquivalence</a
+      ><a name="1348"
+      >
+
+</a
+      ><a name="1350" class="Keyword"
+      >module</a
+      ><a name="1356"
+      > </a
+      ><a name="1357" href="Main.html#1357" class="Module"
+      >Categories</a
+      ><a name="1367"
+      > </a
+      ><a name="1368" class="Keyword"
+      >where</a
+      ><a name="1373"
+      >
+   </a
+      ><a name="1377" class="Comment"
+      >-- &#1059;&#1088;&#1072; ! &#1087;&#1086;&#1085;&#1103;&#1090;&#1080;&#1077; &#1082;&#1072;&#1090;&#1077;&#1075;&#1086;&#1088;&#1080;&#1080;!</a
+      ><a name="1404"
+      >
+  </a
+      ><a name="1407" class="Keyword"
+      >import</a
+      ><a name="1413"
+      > </a
+      ><a name="1414" href="Category.html#1" class="Module"
+      >Category</a
+      ><a name="1422"
       >
 </a
-      ><a name="977" class="Keyword"
-      >import</a
-      ><a name="983"
-      > </a
-      ><a name="984" href="FirstConcepts.html#1" class="Module"
-      >FirstConcepts</a
-      ><a name="997"
+      ><a name="1423" class="Comment"
+      >-- &#1050; &#1101;&#1090;&#1086;&#1084;&#1091; &#1084;&#1086;&#1084;&#1077;&#1085;&#1090;&#1091; &#1091; &#1085;&#1072;&#1089; &#1077;&#1089;&#1090;&#1100; &#1087;&#1086;&#1085;&#1103;&#1090;&#1080;&#1077; &#1086; &#1084;&#1080;&#1088;&#1077; &#1082;&#1072;&#1090;&#1077;&#1075;&#1086;&#1088;&#1080;&#1081; &#1080; &#1087;&#1077;&#1088;&#1074;&#1099;&#1081; &#1087;&#1088;&#1077;&#1076;&#1089;&#1090;&#1072;&#1074;&#1080;&#1090;&#1077;&#1083;&#1100; &#1101;&#1090;&#1086;&#1075;&#1086; &#1084;&#1080;&#1088;&#1072;</a
+      ><a name="1511"
       >
 </a
-      ><a name="998" class="Comment"
-      >-- &#1057;&#1077;&#1084;&#1077;&#1081;&#1089;&#1090;&#1074;&#1072; &#1090;&#1080;&#1087;&#1086;&#1074;. &#1060;&#1091;&#1085;&#1082;&#1094;&#1080;&#1080;. &#1054;&#1090;&#1085;&#1086;&#1096;&#1077;&#1085;&#1080;&#1103;</a
-      ><a name="1036"
+      ><a name="1512" class="Comment"
+      >-- &#1052;&#1099; &#1091;&#1078;&#1077; &#1084;&#1086;&#1078;&#1077;&#1084; &#1085;&#1072;&#1095;&#1072;&#1090;&#1100; &#1077;&#1075;&#1086; &#1087;&#1088;&#1086;&#1076;&#1091;&#1082;&#1090;&#1080;&#1074;&#1085;&#1086; &#1080;&#1079;&#1091;&#1095;&#1072;&#1090;&#1100;. </a
+      ><a name="1560"
       >
-</a
-      ><a name="1037" class="Keyword"
-      >import</a
-      ><a name="1043"
+  </a
+      ><a name="1563" class="Keyword"
+      >module</a
+      ><a name="1569"
       > </a
-      ><a name="1044" href="Relations.html#1" class="Module"
-      >Relations</a
-      ><a name="1053"
+      ><a name="1570" href="Main.html#1570" class="Module"
+      >ConstructionsInCategoryTheory</a
+      ><a name="1599"
+      > </a
+      ><a name="1600" class="Keyword"
+      >where</a
+      ><a name="1605"
       >
-</a
-      ><a name="1054" class="Comment"
-      >-- &#1047;&#1072;&#1087;&#1080;&#1089;&#1080;, &#1086;&#1090;&#1085;&#1086;&#1096;&#1077;&#1085;&#1080;&#1077; &#1101;&#1082;&#1074;&#1080;&#1074;&#1072;&#1083;&#1077;&#1085;&#1090;&#1085;&#1086;&#1089;&#1090;&#1080;</a
-      ><a name="1090"
-      >
-</a
-      ><a name="1091" class="Keyword"
-      >import</a
-      ><a name="1097"
-      >  </a
-      ><a name="1099" href="Equivalence.html#1" class="Module"
-      >Equivalence</a
-      ><a name="1110"
-      >
-</a
-      ><a name="1111" class="Comment"
-      >-- &#1055;&#1088;&#1086;&#1087;&#1086;&#1079;&#1080;&#1094;&#1080;&#1086;&#1085;&#1072;&#1083;&#1100;&#1085;&#1072;&#1103; &#1101;&#1082;&#1074;&#1080;&#1074;&#1072;&#1083;&#1077;&#1085;&#1090;&#1085;&#1086;&#1089;&#1090;&#1100; (&#1090;&#1086;&#1078;&#1076;&#1077;&#1089;&#1090;&#1074;&#1077;&#1085;&#1085;&#1086;&#1089;&#1090;&#1100;)</a
-      ><a name="1165"
-      >
-</a
-      ><a name="1166" class="Keyword"
-      >import</a
-      ><a name="1172"
+  </a
+      ><a name="1608" class="Keyword"
+      >module</a
+      ><a name="1614"
       > </a
-      ><a name="1173" href="PropositionalEquivalence.html#1" class="Module"
-      >PropositionalEquivalence</a
-      ><a name="1197"
-      >
-</a
-      ><a name="1198" class="Comment"
-      >-- &#1059;&#1088;&#1072; ! &#1087;&#1086;&#1085;&#1103;&#1090;&#1080;&#1077; &#1082;&#1072;&#1090;&#1077;&#1075;&#1086;&#1088;&#1080;&#1080;!</a
-      ><a name="1225"
-      >
-</a
-      ><a name="1226" class="Keyword"
-      >import</a
-      ><a name="1232"
+      ><a name="1615" href="Main.html#1615" class="Module"
+      >ExamplesOfCategories</a
+      ><a name="1635"
       > </a
-      ><a name="1233" href="Category.html#1" class="Module"
-      >Category</a
-      ><a name="1241"
-      >
-</a
-      ><a name="1242" class="Comment"
-      >-- &#1050; &#1101;&#1090;&#1086;&#1084;&#1091; &#1084;&#1086;&#1084;&#1077;&#1085;&#1090;&#1091; &#1091; &#1085;&#1072;&#1089; &#1077;&#1089;&#1090;&#1100; &#1087;&#1086;&#1085;&#1103;&#1090;&#1080;&#1077; &#1086; &#1084;&#1080;&#1088;&#1077; &#1082;&#1072;&#1090;&#1077;&#1075;&#1086;&#1088;&#1080;&#1081; &#1080; &#1087;&#1077;&#1088;&#1074;&#1099;&#1081; &#1087;&#1088;&#1077;&#1076;&#1089;&#1090;&#1072;&#1074;&#1080;&#1090;&#1077;&#1083;&#1100; &#1101;&#1090;&#1086;&#1075;&#1086; &#1084;&#1080;&#1088;&#1072;</a
-      ><a name="1330"
-      >
-</a
-      ><a name="1331" class="Comment"
-      >-- &#1052;&#1099; &#1091;&#1078;&#1077; &#1084;&#1086;&#1078;&#1077;&#1084; &#1085;&#1072;&#1095;&#1072;&#1090;&#1100; &#1077;&#1075;&#1086; &#1087;&#1088;&#1086;&#1076;&#1091;&#1082;&#1090;&#1080;&#1074;&#1085;&#1086; &#1080;&#1079;&#1091;&#1095;&#1072;&#1090;&#1100;. </a
-      ><a name="1379"
-      >
-</a
-      ><a name="1380" class="Comment"
-      >-- &#1044;&#1072;&#1083;&#1100;&#1085;&#1077;&#1081;&#1096;&#1080;&#1081; &#1087;&#1083;&#1072;&#1085;: &#1082;&#1072;&#1090;&#1077;&#1075;&#1086;&#1088;&#1080;&#1103; Hom, &#1082;&#1072;&#1090;&#1077;&#1075;&#1086;&#1088;&#1080;&#1103; Cat (&#1082;&#1072;&#1090;&#1077;&#1075;&#1086;&#1088;&#1080;&#1103; &#1082;&#1072;&#1090;&#1077;&#1075;&#1086;&#1088;&#1080;&#1081;), &#1087;&#1088;&#1080;&#1084;&#1077;&#1088;&#1099; &#1082;&#1072;&#1090;&#1077;&#1075;&#1086;&#1088;&#1080;&#1081; .</a
+      ><a name="1636" class="Keyword"
+      >where</a
       ></pre
     ></body
   ></html