Commits

Pavel Perikov  committed 98994a4

curry-howard

  • Participants
  • Parent commits 96c680d

Comments (0)

Files changed (4)

File CurryHoward.agda

+module CurryHoward where
+
+-- Введем тип для натуральных чисел
+data ℕ : Set where
+  zero : ℕ     -- Один из объектов в множестве ℕ. Нуль.
+  suc : ℕ → ℕ -- Способ конструирования еще объектов. Для любого объекта если "следующий" за ним
+
+one = suc zero
+three = suc (suc one)
+-- Парсер агды догадывается, что существует такая вещь, как натуральные числа, определенные подобным образом.
+-- И знает, как последовательность цифр превращать в такие числа. Но для этого ему нужно сообщить, 
+-- какой тип для этого использовать
+
+{-# BUILTIN NATURAL ℕ #-}
+
+four = 4
+
+-------- Типы, параметризованные типами
+data List (A : Set) : Set where
+  [] : List A                         -- пустой список
+  _∷_ : A → List A → List A    -- Список, в голову которого приписан еще один элемент
+
+infixr 3 _∷_      -- укажем компилятору приоритет и ассоциативность операции _∷_ 
+-- Приведенная выше конструкция определяет сразу семейство типов, индексированное типами (индекс, в данном случае - A)
+listOfNats : List ℕ
+listOfNats = 3 ∷ 6 ∷ 1212 ∷ 42 ∷ []
+
+listOfListsOfNat : List (List ℕ)
+listOfListsOfNat = (3 ∷ 5 ∷ []) ∷ [] ∷ (1 ∷ []) ∷ []
+
+-- Особенностью Agda и подобных систем является возможность определять семейства типов, индексированные _данными_
+-- Такая возможность называется "зависимые типы" 
+
+data Vector (A : Set) : (length : ℕ) → Set where
+  -- Семейство типов Vector (последовательность элементов определенной длинны) параметризовано типом (параметр A) и натуральным числом (индекс length)
+  -- Разница между параметрами и индексами несколько не очевидна. Все конструкторы семейства
+  -- должны создавать элементы семейств с одинаковым параметром, но они могут создавать элементы 
+  -- семейств с разными индексами. 
+  [] : Vector _ 0    -- пустой вектор. вместо параметра стоит прочерк, чекер догадается о чем идет речь. Но индекс указан
+  _∷_ : A → {n : _} → Vector A n → Vector _ (suc n) -- Имея элемент типа A и  вектор элементов типа A длиной n, можно получить новый вектор - длиной (n + 1)
+
+vec3 : Vector ℕ 3
+vec3 = 5 ∷ 7 ∷ 8 ∷ []
+
+-- Ошибка:
+-- vec2 : Vector ℕ 2
+-- vec2 = 1 ∷ []
+
+length : ∀{A n} → Vector A n → ℕ
+length {_} {n} _ = n
+
+-- Функция length никак не работает со своим параметром типа Vector. Она работает исключительно по типу
+
+-- Возможность параметризовать типы данными создает возможность создавать очень сложные и точные типы.
+-- Насколько сложные - отдельный вопрос
+
+-- == Curry-Howard correspondence  ==--
+
+-- Рассмотрим семейство типов Positive : ℕ → Set. Существует столько типов в семействе, сколько есть 
+-- натуральных чисел. Определим это семейство так: 
+
+data Positive : ℕ → Set where
+  is-positive : ∀ n → Positive (suc n)
+
+-- Теперь рассмотрим населенность различных членов этого семейства (типов)
+
+1-is-positive : Positive 1
+1-is-positive = is-positive 0
+
+3-is-positive : Positive 3
+3-is-positive = is-positive 2
+
+-- Подумаем, населен ли тип Positive 0? единственный способ создать элемент любого типа 
+-- семейства - это использовать конструктор is-positive. Конструктору нужно передать
+-- один парамет - n. Элемент при этом получится из семейства (n+1). Таким образом, 
+-- тип Positive 0 не населен.
+-- Попробуем это сформулировать в терминах Agda. Как сформулировать утверждение о том, что 
+-- тип не населен? в терминах Agda мы можем сказать следующее: Если некий тип A 
+-- не населен, то существует отображение A → ∅. Для любого населенного типа это не верно
+-- Если в типе A есть хотя бы один элемент a, то ему должен соответствовать элемент в ∅, 
+-- но в нем элементов нет. Следовательно, построить такое отображение не удастся.
+open import FirstConcepts using (∅)
+
+¬_ : (P : Set) → Set₁
+¬ P = P → ∅
+
+-- Соответственно, мы можем сформулировать утверждение:
+
+0-not-positive : ¬ (Positive 0)
+-- Мы должны построить функцию, которая принимает элемент типа Positive 0 возвращает элемент типа ∅
+-- Agda _способна_ увидеть в этом случае, что элементов типа Positive 0 не существует. Унификация
+-- не получается. Поэтому функция будет выглядеть следующим образом
+0-not-positive  ()
+-- вместо имени формального параметра стоит (). Это так называемый absurdity pattern. Параметра быть не может. 
+-- Правую часть (знак равенства и дальше) можно не писать.
+
+-- Соответствие Карри-Ховарда гласит: утверждения (пропозиции) соответствуют типам. Вопрос
+-- об истинности утверждений соответствует вопросу о наличии элементов этого типа. 
+-- Термы типа соответствуют доказательствам этого утверждения.
+-- Типы = утверждения, программы = доказательства
+
+-- Отметим, что тип может быть населен более, чем одним элементом. т.е. как именно сделано доказательство
+-- может играть роль.
+
+head : ∀ {A n} → Vector A n → Positive n → A
+head [] () -- не может существовать позитивного n для пустого вектора
+head (x ∷ v) _ = x
+
+-- Часто в рассуждениях принимают, что доказательство не важно, важен факт его наличия
+-- (proof irrelevance). Пока же мы имеем возможность ссылаться на само доказательство (терм нужного типа,
+-- иногда говорят proof object). К этому вопросу мы еще, возможно, вернемся. Пока скажем, что агда позволяет указывать
+-- требование proof irrelevance. Запишем тип функции head, которая не должна зависеть от конктретного доказательства
+-- позитивности n
+IrrelevantHead = ∀{A n} → Vector A n → .(Positive n) → A
+-- конструкция .(Positive n) говорит, что "разбирать на части" доказательство запрещено. Предъявляется только 
+-- факт его наличия. Этот тип  "более узкий", чем тип функции head. Если функция достигает результата
+-- не "разбирая на части" доказательство, то она может сделать то же самое с "полным" доступом к нему.
+-- Говоря более широко
+
+.to-irrelevant : {Proposition : Set} → (proof : Proposition) → Proposition
+to-irrelevant P = P
+
+-- точка в описании to-irrelevant сообщает нам, что ее результат иррелевантен. Мы всегда 
+-- можем преобразовать "прозрачное" доказательство proof в его иррелевантную версию (с обратным интереснее и сложнее)
+
+-- ----------------------------------------------------------------
+-- Curry-Howard correspondence гласит (в одну сторону): 
+-- утверждения могут быть представлены типами. Вопрос об истинности утверждений 
+-- соответствует вопросу о доказательстве населенности типа. В конструктивных рассуждениях
+-- таким доказательством являетя предоставление терма этого типа
+-- Системы с зависимыми типами позволяют конструировать очень сложные типы, выражающие
+-- очень широкий спектр утверждений.

File html/Category.html

       ><a name="1176" href="FirstConcepts.html#2046" class="Datatype"
       >&#8709;-type</a
       ><a name="1182"
-      > </a
-      ><a name="1183" href="Category.html#1146" class="Bound"
-      >&#8467;</a
-      ><a name="1184"
       >
           </a
-      ><a name="1195" class="Symbol"
+      ><a name="1193" class="Symbol"
       >;</a
-      ><a name="1196"
+      ><a name="1194"
       > </a
-      ><a name="1197" class="Field Operator"
+      ><a name="1195" class="Field Operator"
       >_&#8658;_</a
+      ><a name="1198"
+      > </a
+      ><a name="1199" class="Symbol"
+      >=</a
       ><a name="1200"
       > </a
       ><a name="1201" class="Symbol"
-      >=</a
+      >&#955;</a
       ><a name="1202"
       > </a
-      ><a name="1203" class="Symbol"
-      >&#955;</a
+      ><a name="1203" href="Category.html#1203" class="Bound"
+      >a</a
       ><a name="1204"
       > </a
-      ><a name="1205" href="Category.html#1205" class="Bound"
-      >a</a
+      ><a name="1205" class="Symbol"
+      >&#8594;</a
       ><a name="1206"
       > </a
       ><a name="1207" class="Symbol"
-      >&#8594;</a
+      >&#955;</a
       ><a name="1208"
       > </a
       ><a name="1209" class="Symbol"
-      >&#955;</a
-      ><a name="1210"
-      > </a
-      ><a name="1211" class="Symbol"
       >()</a
-      ><a name="1213"
+      ><a name="1211"
       >
           </a
-      ><a name="1224" class="Symbol"
+      ><a name="1222" class="Symbol"
       >;</a
-      ><a name="1225"
+      ><a name="1223"
       > </a
-      ><a name="1226" class="Field Operator"
+      ><a name="1224" class="Field Operator"
       >_&#8776;_</a
+      ><a name="1227"
+      > </a
+      ><a name="1228" class="Symbol"
+      >=</a
       ><a name="1229"
       > </a
       ><a name="1230" class="Symbol"
-      >=</a
+      >&#955;</a
       ><a name="1231"
       > </a
       ><a name="1232" class="Symbol"
-      >&#955;</a
-      ><a name="1233"
+      >{</a
+      ><a name="1233" href="Category.html#1233" class="Bound"
+      >o&#8321;</a
+      ><a name="1235" class="Symbol"
+      >}</a
+      ><a name="1236"
       > </a
-      ><a name="1234" class="Symbol"
-      >{</a
-      ><a name="1235" href="Category.html#1235" class="Bound"
-      >o&#8321;</a
       ><a name="1237" class="Symbol"
-      >}</a
+      >&#8594;</a
       ><a name="1238"
       > </a
       ><a name="1239" class="Symbol"
-      >&#8594;</a
+      >&#955;</a
       ><a name="1240"
       > </a
       ><a name="1241" class="Symbol"
-      >&#955;</a
-      ><a name="1242"
-      > </a
-      ><a name="1243" class="Symbol"
       >{}</a
-      ><a name="1245"
+      ><a name="1243"
       >
           </a
-      ><a name="1256" class="Symbol"
+      ><a name="1254" class="Symbol"
       >;</a
-      ><a name="1257"
+      ><a name="1255"
       > </a
-      ><a name="1258" class="Field"
+      ><a name="1256" class="Field"
       >id</a
+      ><a name="1258"
+      > </a
+      ><a name="1259" class="Symbol"
+      >=</a
       ><a name="1260"
       > </a
       ><a name="1261" class="Symbol"
-      >=</a
+      >&#955;</a
       ><a name="1262"
       > </a
       ><a name="1263" class="Symbol"
-      >&#955;</a
-      ><a name="1264"
-      > </a
-      ><a name="1265" class="Symbol"
       >{}</a
-      ><a name="1267"
+      ><a name="1265"
       >
           </a
-      ><a name="1278" class="Symbol"
+      ><a name="1276" class="Symbol"
       >;</a
-      ><a name="1279"
+      ><a name="1277"
       > </a
-      ><a name="1280" class="Field Operator"
+      ><a name="1278" class="Field Operator"
       >_&#8728;_</a
+      ><a name="1281"
+      > </a
+      ><a name="1282" class="Symbol"
+      >=</a
       ><a name="1283"
       > </a
       ><a name="1284" class="Symbol"
-      >=</a
+      >&#955;</a
       ><a name="1285"
       > </a
       ><a name="1286" class="Symbol"
-      >&#955;</a
-      ><a name="1287"
+      >{</a
+      ><a name="1287" href="Category.html#1287" class="Bound"
+      >o&#8321;</a
+      ><a name="1289" class="Symbol"
+      >}</a
+      ><a name="1290"
       > </a
-      ><a name="1288" class="Symbol"
+      ><a name="1291" class="Symbol"
       >{</a
-      ><a name="1289" href="Category.html#1289" class="Bound"
-      >o&#8321;</a
-      ><a name="1291" class="Symbol"
+      ><a name="1292" href="Category.html#1292" class="Bound"
+      >o&#8322;</a
+      ><a name="1294" class="Symbol"
       >}</a
-      ><a name="1292"
+      ><a name="1295"
       > </a
-      ><a name="1293" class="Symbol"
-      >{</a
-      ><a name="1294" href="Category.html#1294" class="Bound"
-      >o&#8322;</a
       ><a name="1296" class="Symbol"
-      >}</a
+      >&#8594;</a
       ><a name="1297"
       > </a
       ><a name="1298" class="Symbol"
-      >&#8594;</a
+      >&#955;</a
       ><a name="1299"
       > </a
       ><a name="1300" class="Symbol"
-      >&#955;</a
-      ><a name="1301"
-      > </a
-      ><a name="1302" class="Symbol"
       >{}</a
-      ><a name="1304"
+      ><a name="1302"
       >
           </a
-      ><a name="1315" class="Symbol"
+      ><a name="1313" class="Symbol"
       >;</a
-      ><a name="1316"
+      ><a name="1314"
       > </a
-      ><a name="1317" class="Field"
+      ><a name="1315" class="Field"
       >&#8776;-equivalence</a
+      ><a name="1328"
+      > </a
+      ><a name="1329" class="Symbol"
+      >=</a
       ><a name="1330"
       > </a
       ><a name="1331" class="Symbol"
-      >=</a
+      >&#955;</a
       ><a name="1332"
       > </a
       ><a name="1333" class="Symbol"
-      >&#955;</a
-      ><a name="1334"
+      >{</a
+      ><a name="1334" href="Category.html#1334" class="Bound"
+      >o&#8321;</a
+      ><a name="1336" class="Symbol"
+      >}</a
+      ><a name="1337"
       > </a
-      ><a name="1335" class="Symbol"
-      >{</a
-      ><a name="1336" href="Category.html#1336" class="Bound"
-      >o&#8321;</a
       ><a name="1338" class="Symbol"
-      >}</a
+      >&#8594;</a
       ><a name="1339"
       > </a
       ><a name="1340" class="Symbol"
-      >&#8594;</a
+      >&#955;</a
       ><a name="1341"
       > </a
       ><a name="1342" class="Symbol"
-      >&#955;</a
-      ><a name="1343"
-      > </a
-      ><a name="1344" class="Symbol"
       >{}</a
-      ><a name="1346"
+      ><a name="1344"
       >
           </a
-      ><a name="1357" class="Symbol"
+      ><a name="1355" class="Symbol"
       >;</a
-      ><a name="1358"
+      ><a name="1356"
       > </a
-      ><a name="1359" class="Field"
+      ><a name="1357" class="Field"
       >&#8728;-resp-&#8776;</a
+      ><a name="1365"
+      > </a
+      ><a name="1366" class="Symbol"
+      >=</a
       ><a name="1367"
       > </a
       ><a name="1368" class="Symbol"
-      >=</a
+      >&#955;</a
       ><a name="1369"
       > </a
       ><a name="1370" class="Symbol"
-      >&#955;</a
-      ><a name="1371"
+      >{</a
+      ><a name="1371" href="Category.html#1371" class="Bound"
+      >o&#8321;</a
+      ><a name="1373" class="Symbol"
+      >}</a
+      ><a name="1374"
       > </a
-      ><a name="1372" class="Symbol"
+      ><a name="1375" class="Symbol"
       >{</a
-      ><a name="1373" href="Category.html#1373" class="Bound"
-      >o&#8321;</a
-      ><a name="1375" class="Symbol"
+      ><a name="1376" href="Category.html#1376" class="Bound"
+      >o&#8322;</a
+      ><a name="1378" class="Symbol"
       >}</a
-      ><a name="1376"
+      ><a name="1379"
       > </a
-      ><a name="1377" class="Symbol"
-      >{</a
-      ><a name="1378" href="Category.html#1378" class="Bound"
-      >o&#8322;</a
       ><a name="1380" class="Symbol"
-      >}</a
+      >&#8594;</a
       ><a name="1381"
       > </a
       ><a name="1382" class="Symbol"
-      >&#8594;</a
+      >&#955;</a
       ><a name="1383"
       > </a
       ><a name="1384" class="Symbol"
-      >&#955;</a
-      ><a name="1385"
-      > </a
-      ><a name="1386" class="Symbol"
       >{}</a
-      ><a name="1388"
+      ><a name="1386"
       >
           </a
-      ><a name="1399" class="Symbol"
+      ><a name="1397" class="Symbol"
       >;</a
-      ><a name="1400"
+      ><a name="1398"
       > </a
-      ><a name="1401" class="Field"
+      ><a name="1399" class="Field"
       >identity&#737;</a
+      ><a name="1408"
+      > </a
+      ><a name="1409" class="Symbol"
+      >=</a
       ><a name="1410"
       > </a
       ><a name="1411" class="Symbol"
-      >=</a
+      >&#955;</a
       ><a name="1412"
       > </a
       ><a name="1413" class="Symbol"
-      >&#955;</a
-      ><a name="1414"
+      >{</a
+      ><a name="1414" href="Category.html#1414" class="Bound"
+      >o&#8321;</a
+      ><a name="1416" class="Symbol"
+      >}</a
+      ><a name="1417"
       > </a
-      ><a name="1415" class="Symbol"
-      >{</a
-      ><a name="1416" href="Category.html#1416" class="Bound"
-      >o&#8321;</a
       ><a name="1418" class="Symbol"
-      >}</a
+      >&#8594;</a
       ><a name="1419"
       > </a
       ><a name="1420" class="Symbol"
-      >&#8594;</a
+      >&#955;</a
       ><a name="1421"
       > </a
       ><a name="1422" class="Symbol"
-      >&#955;</a
-      ><a name="1423"
-      > </a
-      ><a name="1424" class="Symbol"
       >{}</a
-      ><a name="1426"
+      ><a name="1424"
       >
           </a
-      ><a name="1437" class="Symbol"
+      ><a name="1435" class="Symbol"
       >;</a
-      ><a name="1438"
+      ><a name="1436"
       > </a
-      ><a name="1439" class="Field"
+      ><a name="1437" class="Field"
       >identity&#691;</a
+      ><a name="1446"
+      > </a
+      ><a name="1447" class="Symbol"
+      >=</a
       ><a name="1448"
       > </a
       ><a name="1449" class="Symbol"
-      >=</a
+      >&#955;</a
       ><a name="1450"
       > </a
       ><a name="1451" class="Symbol"
-      >&#955;</a
-      ><a name="1452"
+      >{</a
+      ><a name="1452" href="Category.html#1452" class="Bound"
+      >o&#8321;</a
+      ><a name="1454" class="Symbol"
+      >}</a
+      ><a name="1455"
       > </a
-      ><a name="1453" class="Symbol"
-      >{</a
-      ><a name="1454" href="Category.html#1454" class="Bound"
-      >o&#8321;</a
       ><a name="1456" class="Symbol"
-      >}</a
+      >&#8594;</a
       ><a name="1457"
       > </a
       ><a name="1458" class="Symbol"
-      >&#8594;</a
+      >&#955;</a
       ><a name="1459"
       > </a
       ><a name="1460" class="Symbol"
-      >&#955;</a
-      ><a name="1461"
-      > </a
-      ><a name="1462" class="Symbol"
       >{}</a
-      ><a name="1464"
+      ><a name="1462"
       >
           </a
-      ><a name="1475" class="Symbol"
+      ><a name="1473" class="Symbol"
       >;</a
-      ><a name="1476"
+      ><a name="1474"
       > </a
-      ><a name="1477" class="Field"
+      ><a name="1475" class="Field"
       >&#8728;-assoc</a
+      ><a name="1482"
+      > </a
+      ><a name="1483" class="Symbol"
+      >=</a
       ><a name="1484"
       > </a
       ><a name="1485" class="Symbol"
-      >=</a
+      >&#955;</a
       ><a name="1486"
       > </a
       ><a name="1487" class="Symbol"
-      >&#955;</a
-      ><a name="1488"
+      >{</a
+      ><a name="1488" href="Category.html#1488" class="Bound"
+      >o&#8321;</a
+      ><a name="1490" class="Symbol"
+      >}</a
+      ><a name="1491"
       > </a
-      ><a name="1489" class="Symbol"
+      ><a name="1492" class="Symbol"
       >{</a
-      ><a name="1490" href="Category.html#1490" class="Bound"
-      >o&#8321;</a
-      ><a name="1492" class="Symbol"
+      ><a name="1493" href="Category.html#1493" class="Bound"
+      >o&#8322;</a
+      ><a name="1495" class="Symbol"
       >}</a
-      ><a name="1493"
+      ><a name="1496"
       > </a
-      ><a name="1494" class="Symbol"
+      ><a name="1497" class="Symbol"
       >{</a
-      ><a name="1495" href="Category.html#1495" class="Bound"
-      >o&#8322;</a
-      ><a name="1497" class="Symbol"
+      ><a name="1498" href="Category.html#1498" class="Bound"
+      >o&#8323;</a
+      ><a name="1500" class="Symbol"
       >}</a
-      ><a name="1498"
+      ><a name="1501"
       > </a
-      ><a name="1499" class="Symbol"
-      >{</a
-      ><a name="1500" href="Category.html#1500" class="Bound"
-      >o&#8323;</a
       ><a name="1502" class="Symbol"
-      >}</a
+      >&#8594;</a
       ><a name="1503"
       > </a
       ><a name="1504" class="Symbol"
-      >&#8594;</a
+      >&#955;</a
       ><a name="1505"
       > </a
       ><a name="1506" class="Symbol"
-      >&#955;</a
-      ><a name="1507"
-      > </a
-      ><a name="1508" class="Symbol"
       >{}</a
-      ><a name="1510"
+      ><a name="1508"
       >
           </a
-      ><a name="1521" class="Symbol"
+      ><a name="1519" class="Symbol"
       >}</a
-      ><a name="1522"
+      ><a name="1520"
       >
 </a
-      ><a name="1523" class="Keyword"
+      ><a name="1521" class="Keyword"
       >data</a
-      ><a name="1527"
+      ><a name="1525"
       > </a
-      ><a name="1528" href="Category.html#1528" class="Datatype"
+      ><a name="1526" href="Category.html#1526" class="Datatype"
       >OnlyEmpty</a
-      ><a name="1537"
+      ><a name="1535"
       > </a
+      ><a name="1536" class="Symbol"
+      >{</a
+      ><a name="1537" href="Category.html#1537" class="Bound"
+      >&#8467;</a
       ><a name="1538" class="Symbol"
-      >{</a
-      ><a name="1539" href="Category.html#1539" class="Bound"
-      >&#8467;</a
+      >}</a
+      ><a name="1539"
+      > </a
       ><a name="1540" class="Symbol"
-      >}</a
+      >:</a
       ><a name="1541"
       > </a
-      ><a name="1542" class="Symbol"
-      >:</a
-      ><a name="1543"
+      ><a name="1542" href="Category.html#97" class="Record"
+      >Category</a
+      ><a name="1550"
       > </a
-      ><a name="1544" href="Category.html#97" class="Record"
-      >Category</a
+      ><a name="1551" href="Category.html#1537" class="Bound"
+      >&#8467;</a
       ><a name="1552"
       > </a
-      ><a name="1553" href="Category.html#1539" class="Bound"
-      >&#8467;</a
+      ><a name="1553" class="Symbol"
+      >&#8594;</a
       ><a name="1554"
       > </a
-      ><a name="1555" class="Symbol"
-      >&#8594;</a
-      ><a name="1556"
+      ><a name="1555" class="PrimitiveType"
+      >Set</a
+      ><a name="1558"
       > </a
-      ><a name="1557" class="PrimitiveType"
-      >Set</a
+      ><a name="1559" href="Category.html#1537" class="Bound"
+      >&#8467;</a
       ><a name="1560"
       > </a
-      ><a name="1561" href="Category.html#1539" class="Bound"
-      >&#8467;</a
-      ><a name="1562"
-      > </a
-      ><a name="1563" class="Keyword"
+      ><a name="1561" class="Keyword"
       >where</a
-      ><a name="1568"
+      ><a name="1566"
       >
    </a
-      ><a name="1572" href="Category.html#1572" class="InductiveConstructor"
+      ><a name="1570" href="Category.html#1570" class="InductiveConstructor"
       >empty</a
+      ><a name="1575"
+      > </a
+      ><a name="1576" class="Symbol"
+      >:</a
       ><a name="1577"
       > </a
-      ><a name="1578" class="Symbol"
-      >:</a
-      ><a name="1579"
+      ><a name="1578" href="Category.html#1526" class="Datatype"
+      >OnlyEmpty</a
+      ><a name="1587"
       > </a
-      ><a name="1580" href="Category.html#1528" class="Datatype"
-      >OnlyEmpty</a
+      ><a name="1588" href="Category.html#1118" class="Function"
+      >&#8709;</a
       ><a name="1589"
-      > </a
-      ><a name="1590" href="Category.html#1118" class="Function"
-      >&#8709;</a
-      ><a name="1591"
       >
 
 </a
-      ><a name="1593" href="Category.html#1593" class="Function"
+      ><a name="1591" href="Category.html#1591" class="Function"
       >CatWithEmpty</a
-      ><a name="1605"
+      ><a name="1603"
       >  </a
+      ><a name="1605" class="Symbol"
+      >:</a
+      ><a name="1606"
+      > </a
       ><a name="1607" class="Symbol"
+      >{</a
+      ><a name="1608" href="Category.html#1608" class="Bound"
+      >&#8467;</a
+      ><a name="1609"
+      > </a
+      ><a name="1610" class="Symbol"
       >:</a
-      ><a name="1608"
-      > </a
-      ><a name="1609" class="Symbol"
-      >{</a
-      ><a name="1610" href="Category.html#1610" class="Bound"
-      >&#8467;</a
       ><a name="1611"
       > </a
       ><a name="1612" class="Symbol"
-      >:</a
-      ><a name="1613"
+      >_}</a
+      ><a name="1614"
       > </a
-      ><a name="1614" class="Symbol"
-      >_}</a
+      ><a name="1615" class="Symbol"
+      >&#8594;</a
       ><a name="1616"
+      >  </a
+      ><a name="1618" href="Category.html#97" class="Record"
+      >Category</a
+      ><a name="1626"
       > </a
-      ><a name="1617" class="Symbol"
-      >&#8594;</a
-      ><a name="1618"
-      >  </a
-      ><a name="1620" href="Category.html#97" class="Record"
-      >Category</a
-      ><a name="1628"
+      ><a name="1627" class="Symbol"
+      >(</a
+      ><a name="1628" href="Agda.Primitive.html#596" class="Primitive"
+      >suc</a
+      ><a name="1631"
       > </a
-      ><a name="1629" class="Symbol"
-      >(</a
-      ><a name="1630" href="Agda.Primitive.html#596" class="Primitive"
-      >suc</a
-      ><a name="1633"
-      > </a
-      ><a name="1634" href="Category.html#1610" class="Bound"
+      ><a name="1632" href="Category.html#1608" class="Bound"
       >&#8467;</a
-      ><a name="1635" class="Symbol"
+      ><a name="1633" class="Symbol"
       >)</a
-      ><a name="1636"
+      ><a name="1634"
       > 
 </a
-      ><a name="1638" href="Category.html#1593" class="Function"
+      ><a name="1636" href="Category.html#1591" class="Function"
       >CatWithEmpty</a
-      ><a name="1650"
+      ><a name="1648"
       > </a
+      ><a name="1649" class="Symbol"
+      >{</a
+      ><a name="1650" href="Category.html#1650" class="Bound"
+      >&#8467;</a
       ><a name="1651" class="Symbol"
-      >{</a
-      ><a name="1652" href="Category.html#1652" class="Bound"
-      >&#8467;</a
+      >}</a
+      ><a name="1652"
+      > </a
       ><a name="1653" class="Symbol"
-      >}</a
+      >=</a
       ><a name="1654"
       > </a
-      ><a name="1655" class="Symbol"
-      >=</a
-      ><a name="1656"
-      > </a
-      ><a name="1657" class="Keyword"
+      ><a name="1655" class="Keyword"
       >record</a
-      ><a name="1663"
+      ><a name="1661"
       >
                      </a
-      ><a name="1685" class="Symbol"
+      ><a name="1683" class="Symbol"
       >{</a
-      ><a name="1686"
+      ><a name="1684"
       > </a
-      ><a name="1687" class="Field"
+      ><a name="1685" class="Field"
       >Obj</a
+      ><a name="1688"
+      > </a
+      ><a name="1689" class="Symbol"
+      >=</a
       ><a name="1690"
       > </a
-      ><a name="1691" class="Symbol"
-      >=</a
-      ><a name="1692"
+      ><a name="1691" href="Category.html#1526" class="Datatype"
+      >OnlyEmpty</a
+      ><a name="1700"
       > </a
-      ><a name="1693" href="Category.html#1528" class="Datatype"
-      >OnlyEmpty</a
+      ><a name="1701" href="Category.html#1118" class="Function"
+      >&#8709;</a
       ><a name="1702"
-      > </a
-      ><a name="1703" href="Category.html#1118" class="Function"
-      >&#8709;</a
-      ><a name="1704"
       >
                      </a
-      ><a name="1726" class="Symbol"
+      ><a name="1724" class="Symbol"
       >;</a
-      ><a name="1727"
+      ><a name="1725"
       > </a
-      ><a name="1728" class="Field Operator"
+      ><a name="1726" class="Field Operator"
       >_&#8658;_</a
+      ><a name="1729"
+      > </a
+      ><a name="1730" class="Symbol"
+      >=</a
       ><a name="1731"
       > </a
       ><a name="1732" class="Symbol"
-      >=</a
+      >&#955;</a
       ><a name="1733"
       > </a
       ><a name="1734" class="Symbol"
-      >&#955;</a
+      >{</a
       ><a name="1735"
       > </a
       ><a name="1736" class="Symbol"
-      >{</a
+      >_</a
       ><a name="1737"
       > </a
       ><a name="1738" class="Symbol"
       ><a name="1739"
       > </a
       ><a name="1740" class="Symbol"
-      >_</a
+      >&#8594;</a
       ><a name="1741"
       > </a
-      ><a name="1742" class="Symbol"
-      >&#8594;</a
-      ><a name="1743"
+      ><a name="1742" href="Category.html#1526" class="Datatype"
+      >OnlyEmpty</a
+      ><a name="1751"
       > </a
-      ><a name="1744" href="Category.html#1528" class="Datatype"
-      >OnlyEmpty</a
+      ><a name="1752" href="Category.html#1118" class="Function"
+      >&#8709;</a
       ><a name="1753"
       > </a
-      ><a name="1754" href="Category.html#1118" class="Function"
-      >&#8709;</a
+      ><a name="1754" class="Symbol"
+      >}</a
       ><a name="1755"
-      > </a
-      ><a name="1756" class="Symbol"
-      >}</a
-      ><a name="1757"
       >
                      </a
-      ><a name="1779" class="Symbol"
+      ><a name="1777" class="Symbol"
       >;</a
-      ><a name="1780"
+      ><a name="1778"
       > </a
-      ><a name="1781" class="Field Operator"
+      ><a name="1779" class="Field Operator"
       >_&#8776;_</a
+      ><a name="1782"
+      > </a
+      ><a name="1783" class="Symbol"
+      >=</a
       ><a name="1784"
       > </a
       ><a name="1785" class="Symbol"
-      >=</a
+      >&#955;</a
       ><a name="1786"
       > </a
       ><a name="1787" class="Symbol"
-      >&#955;</a
+      >{</a
       ><a name="1788"
       > </a
       ><a name="1789" class="Symbol"
-      >{</a
+      >_</a
       ><a name="1790"
       > </a
       ><a name="1791" class="Symbol"
       ><a name="1792"
       > </a
       ><a name="1793" class="Symbol"
-      >_</a
+      >&#8594;</a
       ><a name="1794"
       > </a
-      ><a name="1795" class="Symbol"
-      >&#8594;</a
-      ><a name="1796"
+      ><a name="1795" href="Category.html#1526" class="Datatype"
+      >OnlyEmpty</a
+      ><a name="1804"
       > </a
-      ><a name="1797" href="Category.html#1528" class="Datatype"
-      >OnlyEmpty</a
+      ><a name="1805" href="Category.html#1118" class="Function"
+      >&#8709;</a
       ><a name="1806"
       > </a
-      ><a name="1807" href="Category.html#1118" class="Function"
-      >&#8709;</a
+      ><a name="1807" class="Symbol"
+      >}</a
       ><a name="1808"
-      > </a
-      ><a name="1809" class="Symbol"
-      >}</a
-      ><a name="1810"
       >
                      </a
-      ><a name="1832" class="Symbol"
+      ><a name="1830" class="Symbol"
       >;</a
-      ><a name="1833"
+      ><a name="1831"
       > </a
-      ><a name="1834" class="Field"
+      ><a name="1832" class="Field"
       >id</a
+      ><a name="1834"
+      > </a
+      ><a name="1835" class="Symbol"
+      >=</a
       ><a name="1836"
       > </a
       ><a name="1837" class="Symbol"
-      >=</a
+      >&#955;</a
       ><a name="1838"
       > </a
       ><a name="1839" class="Symbol"
-      >&#955;</a
-      ><a name="1840"
+      >{</a
+      ><a name="1840" href="Category.html#1840" class="Bound"
+      >o</a
+      ><a name="1841" class="Symbol"
+      >}</a
+      ><a name="1842"
       > </a
-      ><a name="1841" class="Symbol"
-      >{</a
-      ><a name="1842" href="Category.html#1842" class="Bound"
-      >o</a
       ><a name="1843" class="Symbol"
-      >}</a
+      >&#8594;</a
       ><a name="1844"
       > </a
-      ><a name="1845" class="Symbol"
-      >&#8594;</a
-      ><a name="1846"
-      > </a
-      ><a name="1847" href="Category.html#1572" class="InductiveConstructor"
+      ><a name="1845" href="Category.html#1570" class="InductiveConstructor"
       >empty</a
-      ><a name="1852"
+      ><a name="1850"
       >
                      </a
-      ><a name="1874" class="Symbol"
+      ><a name="1872" class="Symbol"
       >;</a
-      ><a name="1875"
+      ><a name="1873"
       > </a
-      ><a name="1876" class="Field Operator"
+      ><a name="1874" class="Field Operator"
       >_&#8728;_</a
+      ><a name="1877"
+      > </a
+      ><a name="1878" class="Symbol"
+      >=</a
       ><a name="1879"
       > </a
       ><a name="1880" class="Symbol"
-      >=</a
+      >&#955;</a
       ><a name="1881"
       > </a
       ><a name="1882" class="Symbol"
-      >&#955;</a
-      ><a name="1883"
+      >{</a
+      ><a name="1883" href="Category.html#1883" class="Bound"
+      >o&#8321;</a
+      ><a name="1885" class="Symbol"
+      >}</a
+      ><a name="1886"
       > </a
-      ><a name="1884" class="Symbol"
+      ><a name="1887" class="Symbol"
       >{</a
-      ><a name="1885" href="Category.html#1885" class="Bound"
-      >o&#8321;</a
-      ><a name="1887" class="Symbol"
+      ><a name="1888" href="Category.html#1888" class="Bound"
+      >o&#8322;</a
+      ><a name="1890" class="Symbol"
       >}</a
-      ><a name="1888"
+      ><a name="1891"
       > </a
-      ><a name="1889" class="Symbol"
+      ><a name="1892" class="Symbol"
       >{</a
-      ><a name="1890" href="Category.html#1890" class="Bound"
-      >o&#8322;</a
-      ><a name="1892" class="Symbol"
+      ><a name="1893" href="Category.html#1893" class="Bound"
+      >o&#8323;</a
+      ><a name="1895" class="Symbol"
       >}</a
-      ><a name="1893"
+      ><a name="1896"
       > </a
-      ><a name="1894" class="Symbol"
-      >{</a
-      ><a name="1895" href="Category.html#1895" class="Bound"
-      >o&#8323;</a
-      ><a name="1897" class="Symbol"
-      >}</a
+      ><a name="1897" href="Category.html#1897" class="Bound"
+      >_</a
       ><a name="1898"
       > </a
       ><a name="1899" href="Category.html#1899" class="Bound"
       >_</a
       ><a name="1900"
       > </a
-      ><a name="1901" href="Category.html#1901" class="Bound"
-      >_</a
+      ><a name="1901" class="Symbol"
+      >&#8594;</a
       ><a name="1902"
       > </a
-      ><a name="1903" class="Symbol"
-      >&#8594;</a
-      ><a name="1904"
-      > </a
-      ><a name="1905" href="Category.html#1572" class="InductiveConstructor"
+      ><a name="1903" href="Category.html#1570" class="InductiveConstructor"
       >empty</a
-      ><a name="1910"
+      ><a name="1908"
       >
                      </a
-      ><a name="1932" class="Symbol"
+      ><a name="1930" class="Symbol"
       >;</a
-      ><a name="1933"
+      ><a name="1931"
       > </a
-      ><a name="1934" class="Field"
+      ><a name="1932" class="Field"
       >&#8776;-equivalence</a
+      ><a name="1945"
+      > </a
+      ><a name="1946" class="Symbol"
+      >=</a
       ><a name="1947"
-      > </a
-      ><a name="1948" class="Symbol"
-      >=</a
-      ><a name="1949"
       > 
                             </a
-      ><a name="1979" class="Keyword"
+      ><a name="1977" class="Keyword"
       >record</a
-      ><a name="1985"
+      ><a name="1983"
       > 
                               </a
-      ><a name="2017" class="Symbol"
+      ><a name="2015" class="Symbol"
       >{</a
-      ><a name="2018"
+      ><a name="2016"
       > </a
-      ><a name="2019" class="Field"
+      ><a name="2017" class="Field"
       >refl</a
+      ><a name="2021"
+      > </a
+      ><a name="2022" class="Symbol"
+      >=</a
       ><a name="2023"
       > </a
       ><a name="2024" class="Symbol"
-      >=</a
+      >&#955;</a
       ><a name="2025"
       > </a
       ><a name="2026" class="Symbol"
-      >&#955;</a
-      ><a name="2027"
+      >{</a
+      ><a name="2027" href="Category.html#2027" class="Bound"
+      >a</a
+      ><a name="2028" class="Symbol"
+      >}</a
+      ><a name="2029"
       > </a
-      ><a name="2028" class="Symbol"
-      >{</a
-      ><a name="2029" href="Category.html#2029" class="Bound"
-      >a</a
       ><a name="2030" class="Symbol"
-      >}</a
+      >&#8594;</a
       ><a name="2031"
       > </a
-      ><a name="2032" class="Symbol"
-      >&#8594;</a
-      ><a name="2033"
-      > </a
-      ><a name="2034" href="Category.html#1572" class="InductiveConstructor"
+      ><a name="2032" href="Category.html#1570" class="InductiveConstructor"
       >empty</a
-      ><a name="2039"
+      ><a name="2037"
       >
                               </a
-      ><a name="2070" class="Symbol"
+      ><a name="2068" class="Symbol"
       >;</a
-      ><a name="2071"
+      ><a name="2069"
       > </a
-      ><a name="2072" class="Field"
+      ><a name="2070" class="Field"
       >sym</a
+      ><a name="2073"
+      > </a
+      ><a name="2074" class="Symbol"
+      >=</a
       ><a name="2075"
       > </a
       ><a name="2076" class="Symbol"
-      >=</a
+      >&#955;</a
       ><a name="2077"
       > </a
       ><a name="2078" class="Symbol"
-      >&#955;</a
-      ><a name="2079"
+      >{</a
+      ><a name="2079" href="Category.html#2079" class="Bound"
+      >a</a
+      ><a name="2080" class="Symbol"
+      >}</a
+      ><a name="2081"
       > </a
-      ><a name="2080" class="Symbol"
+      ><a name="2082" class="Symbol"
       >{</a
-      ><a name="2081" href="Category.html#2081" class="Bound"
-      >a</a
-      ><a name="2082" class="Symbol"
+      ><a name="2083" href="Category.html#2083" class="Bound"
+      >b</a
+      ><a name="2084" class="Symbol"
       >}</a
-      ><a name="2083"
+      ><a name="2085"
       > </a
-      ><a name="2084" class="Symbol"
-      >{</a
-      ><a name="2085" href="Category.html#2085" class="Bound"
-      >b</a
-      ><a name="2086" class="Symbol"
-      >}</a
+      ><a name="2086" href="Category.html#2086" class="Bound"
+      >_</a
       ><a name="2087"
       > </a
-      ><a name="2088" href="Category.html#2088" class="Bound"
-      >_</a
+      ><a name="2088" class="Symbol"
+      >&#8594;</a
       ><a name="2089"
       > </a
-      ><a name="2090" class="Symbol"
-      >&#8594;</a
-      ><a name="2091"
-      > </a
-      ><a name="2092" href="Category.html#1572" class="InductiveConstructor"
+      ><a name="2090" href="Category.html#1570" class="InductiveConstructor"
       >empty</a
-      ><a name="2097"
+      ><a name="2095"
       >
                               </a
-      ><a name="2128" class="Symbol"
+      ><a name="2126" class="Symbol"
       >;</a
-      ><a name="2129"
+      ><a name="2127"
       > </a
-      ><a name="2130" class="Field"
+      ><a name="2128" class="Field"
       >trans</a
+      ><a name="2133"
+      > </a
+      ><a name="2134" class="Symbol"
+      >=</a
       ><a name="2135"
       > </a
       ><a name="2136" class="Symbol"
-      >=</a
+      >&#955;</a
       ><a name="2137"
       > </a
       ><a name="2138" class="Symbol"
-      >&#955;</a
-      ><a name="2139"
+      >{</a
+      ><a name="2139" href="Category.html#2139" class="Bound"
+      >a</a
+      ><a name="2140" class="Symbol"
+      >}</a
+      ><a name="2141"
       > </a
-      ><a name="2140" class="Symbol"
+      ><a name="2142" class="Symbol"
       >{</a
-      ><a name="2141" href="Category.html#2141" class="Bound"
-      >a</a
-      ><a name="2142" class="Symbol"
+      ><a name="2143" href="Category.html#2143" class="Bound"
+      >b</a
+      ><a name="2144" class="Symbol"
       >}</a
-      ><a name="2143"
+      ><a name="2145"
       > </a
-      ><a name="2144" class="Symbol"
+      ><a name="2146" class="Symbol"
       >{</a
-      ><a name="2145" href="Category.html#2145" class="Bound"
-      >b</a
-      ><a name="2146" class="Symbol"
+      ><a name="2147" href="Category.html#2147" class="Bound"
+      >c</a
+      ><a name="2148" class="Symbol"
       >}</a
-      ><a name="2147"
+      ><a name="2149"
       > </a
-      ><a name="2148" class="Symbol"
-      >{</a
-      ><a name="2149" href="Category.html#2149" class="Bound"
-      >c</a
-      ><a name="2150" class="Symbol"
-      >}</a
+      ><a name="2150" href="Category.html#2150" class="Bound"
+      >_</a
       ><a name="2151"
       > </a
       ><a name="2152" href="Category.html#2152" class="Bound"
       >_</a
       ><a name="2153"
       > </a
-      ><a name="2154" href="Category.html#2154" class="Bound"
-      >_</a
+      ><a name="2154" class="Symbol"
+      >&#8594;</a
       ><a name="2155"
       > </a
-      ><a name="2156" class="Symbol"
-      >&#8594;</a
-      ><a name="2157"
+      ><a name="2156" href="Category.html#1570" class="InductiveConstructor"
+      >empty</a
+      ><a name="2161"
       > </a
-      ><a name="2158" href="Category.html#1572" class="InductiveConstructor"
-      >empty</a
+      ><a name="2162" class="Symbol"
+      >}</a
       ><a name="2163"
-      > </a
-      ><a name="2164" class="Symbol"
-      >}</a
-      ><a name="2165"
       >
                      </a
-      ><a name="2187" class="Symbol"
+      ><a name="2185" class="Symbol"
       >;</a
-      ><a name="2188"
+      ><a name="2186"
       > </a
-      ><a name="2189" class="Field"
+      ><a name="2187" class="Field"
       >&#8728;-resp-&#8776;</a
+      ><a name="2195"
+      > </a
+      ><a name="2196" class="Symbol"
+      >=</a
       ><a name="2197"
       > </a
       ><a name="2198" class="Symbol"
-      >=</a
+      >&#955;</a
       ><a name="2199"
       > </a
       ><a name="2200" class="Symbol"
-      >&#955;</a
-      ><a name="2201"
+      >{</a
+      ><a name="2201" href="Category.html#2201" class="Bound"
+      >o&#8321;</a
+      ><a name="2203" class="Symbol"
+      >}</a
+      ><a name="2204"
       > </a
-      ><a name="2202" class="Symbol"
+      ><a name="2205" class="Symbol"
       >{</a
-      ><a name="2203" href="Category.html#2203" class="Bound"
-      >o&#8321;</a
-      ><a name="2205" class="Symbol"
+      ><a name="2206" href="Category.html#2206" class="Bound"
+      >o&#8322;</a
+      ><a name="2208" class="Symbol"
       >}</a
-      ><a name="2206"
+      ><a name="2209"
       > </a
-      ><a name="2207" class="Symbol"
+      ><a name="2210" class="Symbol"
       >{</a
-      ><a name="2208" href="Category.html#2208" class="Bound"
-      >o&#8322;</a
-      ><a name="2210" class="Symbol"
+      ><a name="2211" href="Category.html#2211" class="Bound"
+      >o&#8323;</a
+      ><a name="2213" class="Symbol"
       >}</a
-      ><a name="2211"
+      ><a name="2214"
       > </a
-      ><a name="2212" class="Symbol"
+      ><a name="2215" class="Symbol"
       >{</a
-      ><a name="2213" href="Category.html#2213" class="Bound"
-      >o&#8323;</a
-      ><a name="2215" class="Symbol"
+      ><a name="2216" href="Category.html#2216" class="Bound"
+      >f&#8321;</a
+      ><a name="2218" class="Symbol"
       >}</a
-      ><a name="2216"
+      ><a name="2219"
       > </a
-      ><a name="2217" class="Symbol"
+      ><a name="2220" class="Symbol"
       >{</a
-      ><a name="2218" href="Category.html#2218" class="Bound"
-      >f&#8321;</a
-      ><a name="2220" class="Symbol"
+      ><a name="2221" href="Category.html#2221" class="Bound"
+      >f&#8321;&#8242;</a
+      ><a name="2224" class="Symbol"
       >}</a
-      ><a name="2221"
+      ><a name="2225"
       > </a
-      ><a name="2222" class="Symbol"
+      ><a name="2226" class="Symbol"
       >{</a
-      ><a name="2223" href="Category.html#2223" class="Bound"
-      >f&#8321;&#8242;</a
-      ><a name="2226" class="Symbol"
+      ><a name="2227" href="Category.html#2227" class="Bound"
+      >f&#8322;</a
+      ><a name="2229" class="Symbol"
       >}</a
-      ><a name="2227"
+      ><a name="2230"
       > </a
-      ><a name="2228" class="Symbol"
+      ><a name="2231" class="Symbol"
       >{</a
-      ><a name="2229" href="Category.html#2229" class="Bound"
-      >f&#8322;</a
-      ><a name="2231" class="Symbol"
+      ><a name="2232" href="Category.html#2232" class="Bound"
+      >f&#8322;&#8242;</a
+      ><a name="2235" class="Symbol"
       >}</a
-      ><a name="2232"
+      ><a name="2236"
       > </a
-      ><a name="2233" class="Symbol"
-      >{</a
-      ><a name="2234" href="Category.html#2234" class="Bound"
-      >f&#8322;&#8242;</a
-      ><a name="2237" class="Symbol"
-      >}</a
+      ><a name="2237" href="Category.html#2237" class="Bound"
+      >_</a
       ><a name="2238"
       > </a
       ><a name="2239" href="Category.html#2239" class="Bound"
       >_</a
       ><a name="2240"
       > </a
-      ><a name="2241" href="Category.html#2241" class="Bound"
-      >_</a
+      ><a name="2241" class="Symbol"
+      >&#8594;</a
       ><a name="2242"
       > </a
-      ><a name="2243" class="Symbol"
-      >&#8594;</a
-      ><a name="2244"
-      > </a
-      ><a name="2245" href="Category.html#1572" class="InductiveConstructor"
+      ><a name="2243" href="Category.html#1570" class="InductiveConstructor"
       >empty</a
-      ><a name="2250"
+      ><a name="2248"
       >
                      </a
-      ><a name="2272" class="Symbol"
+      ><a name="2270" class="Symbol"
       >;</a
-      ><a name="2273"
+      ><a name="2271"
       > </a
-      ><a name="2274" class="Field"
+      ><a name="2272" class="Field"
       >identity&#737;</a
+      ><a name="2281"
+      > </a
+      ><a name="2282" class="Symbol"
+      >=</a
       ><a name="2283"
       > </a
       ><a name="2284" class="Symbol"
-      >=</a
+      >&#955;</a
       ><a name="2285"
       > </a
       ><a name="2286" class="Symbol"
-      >&#955;</a
-      ><a name="2287"
+      >{</a
+      ><a name="2287" href="Category.html#2287" class="Bound"
+      >o&#8321;</a
+      ><a name="2289" class="Symbol"
+      >}</a
+      ><a name="2290"
       > </a
-      ><a name="2288" class="Symbol"
+      ><a name="2291" class="Symbol"
       >{</a
-      ><a name="2289" href="Category.html#2289" class="Bound"
-      >o&#8321;</a
-      ><a name="2291" class="Symbol"
+      ><a name="2292" href="Category.html#2292" class="Bound"
+      >o&#8322;</a
+      ><a name="2294" class="Symbol"
       >}</a
-      ><a name="2292"
+      ><a name="2295"
       > </a
-      ><a name="2293" class="Symbol"
-      >{</a
-      ><a name="2294" href="Category.html#2294" class="Bound"
-      >o&#8322;</a
-      ><a name="2296" class="Symbol"
-      >}</a
+      ><a name="2296" href="Category.html#2296" class="Bound"
+      >f</a
       ><a name="2297"
       > </a
-      ><a name="2298" href="Category.html#2298" class="Bound"
-      >f</a
+      ><a name="2298" class="Symbol"
+      >&#8594;</a
       ><a name="2299"
       > </a
-      ><a name="2300" class="Symbol"
-      >&#8594;</a
-      ><a name="2301"
-      > </a
-      ><a name="2302" href="Category.html#1572" class="InductiveConstructor"
+      ><a name="2300" href="Category.html#1570" class="InductiveConstructor"
       >empty</a
-      ><a name="2307"
+      ><a name="2305"
       >
                      </a
-      ><a name="2329" class="Symbol"
+      ><a name="2327" class="Symbol"
       >;</a
-      ><a name="2330"
+      ><a name="2328"
       > </a
-      ><a name="2331" class="Field"
+      ><a name="2329" class="Field"
       >identity&#691;</a
+      ><a name="2338"
+      > </a
+      ><a name="2339" class="Symbol"
+      >=</a
       ><a name="2340"
       > </a
       ><a name="2341" class="Symbol"
-      >=</a
+      >&#955;</a
       ><a name="2342"
       > </a
       ><a name="2343" class="Symbol"
-      >&#955;</a
-      ><a name="2344"
+      >{</a
+      ><a name="2344" href="Category.html#2344" class="Bound"
+      >o&#8321;</a
+      ><a name="2346" class="Symbol"
+      >}</a
+      ><a name="2347"
       > </a
-      ><a name="2345" class="Symbol"
+      ><a name="2348" class="Symbol"
       >{</a
-      ><a name="2346" href="Category.html#2346" class="Bound"
-      >o&#8321;</a
-      ><a name="2348" class="Symbol"
+      ><a name="2349" href="Category.html#2349" class="Bound"
+      >o&#8322;</a
+      ><a name="2351" class="Symbol"
       >}</a
-      ><a name="2349"
+      ><a name="2352"
       > </a
-      ><a name="2350" class="Symbol"
-      >{</a
-      ><a name="2351" href="Category.html#2351" class="Bound"
-      >o&#8322;</a
-      ><a name="2353" class="Symbol"
-      >}</a
+      ><a name="2353" href="Category.html#2353" class="Bound"
+      >f</a
       ><a name="2354"
       > </a
-      ><a name="2355" href="Category.html#2355" class="Bound"
-      >f</a
+      ><a name="2355" class="Symbol"
+      >&#8594;</a
       ><a name="2356"
       > </a
-      ><a name="2357" class="Symbol"
-      >&#8594;</a
-      ><a name="2358"
-      > </a
-      ><a name="2359" href="Category.html#1572" class="InductiveConstructor"
+      ><a name="2357" href="Category.html#1570" class="InductiveConstructor"
       >empty</a
-      ><a name="2364"
+      ><a name="2362"
       >
                      </a
-      ><a name="2386" class="Symbol"
+      ><a name="2384" class="Symbol"
       >;</a
-      ><a name="2387"
+      ><a name="2385"
       > </a
-      ><a name="2388" class="Field"
+      ><a name="2386" class="Field"
       >&#8728;-assoc</a
+      ><a name="2393"
+      > </a
+      ><a name="2394" class="Symbol"
+      >=</a
       ><a name="2395"
       > </a
       ><a name="2396" class="Symbol"
-      >=</a
+      >&#955;</a
       ><a name="2397"
       > </a
       ><a name="2398" class="Symbol"
-      >&#955;</a
-      ><a name="2399"
+      >{</a
+      ><a name="2399" href="Category.html#2399" class="Bound"
+      >o&#8321;</a
+      ><a name="2401" class="Symbol"
+      >}</a
+      ><a name="2402"
       > </a
-      ><a name="2400" class="Symbol"
+      ><a name="2403" class="Symbol"
       >{</a
-      ><a name="2401" href="Category.html#2401" class="Bound"
-      >o&#8321;</a
-      ><a name="2403" class="Symbol"
+      ><a name="2404" href="Category.html#2404" class="Bound"
+      >o&#8322;</a
+      ><a name="2406" class="Symbol"
       >}</a
-      ><a name="2404"
+      ><a name="2407"
       > </a
-      ><a name="2405" class="Symbol"
+      ><a name="2408" class="Symbol"
       >{</a
-      ><a name="2406" href="Category.html#2406" class="Bound"
-      >o&#8322;</a
-      ><a name="2408" class="Symbol"
+      ><a name="2409" href="Category.html#2409" class="Bound"
+      >o&#8323;</a
+      ><a name="2411" class="Symbol"
       >}</a
-      ><a name="2409"
+      ><a name="2412"
       > </a
-      ><a name="2410" class="Symbol"
+      ><a name="2413" class="Symbol"
       >{</a
-      ><a name="2411" href="Category.html#2411" class="Bound"
-      >o&#8323;</a
-      ><a name="2413" class="Symbol"
+      ><a name="2414" href="Category.html#2414" class="Bound"
+      >o&#8324;</a
+      ><a name="2416" class="Symbol"
       >}</a
-      ><a name="2414"
+      ><a name="2417"
       > </a
-      ><a name="2415" class="Symbol"
-      >{</a
-      ><a name="2416" href="Category.html#2416" class="Bound"
-      >o&#8324;</a
-      ><a name="2418" class="Symbol"
-      >}</a
-      ><a name="2419"
+      ><a name="2418" href="Category.html#2418" class="Bound"
+      >f&#8321;</a
+      ><a name="2420"
       > </a
-      ><a name="2420" href="Category.html#2420" class="Bound"
-      >f&#8321;</a
-      ><a name="2422"
+      ><a name="2421" href="Category.html#2421" class="Bound"
+      >f&#8322;</a
+      ><a name="2423"
       > </a
-      ><a name="2423" href="Category.html#2423" class="Bound"
-      >f&#8322;</a
-      ><a name="2425"
+      ><a name="2424" href="Category.html#2424" class="Bound"
+      >f&#8323;</a
+      ><a name="2426"
       > </a
-      ><a name="2426" href="Category.html#2426" class="Bound"
-      >f&#8323;</a
+      ><a name="2427" class="Symbol"
+      >&#8594;</a
       ><a name="2428"
       > </a
-      ><a name="2429" class="Symbol"
-      >&#8594;</a
-      ><a name="2430"
-      > </a
-      ><a name="2431" href="Category.html#1572" class="InductiveConstructor"
+      ><a name="2429" href="Category.html#1570" class="InductiveConstructor"
       >empty</a
-      ><a name="2436"
+      ><a name="2434"
       >
                      </a
-      ><a name="2458" class="Symbol"
+      ><a name="2456" class="Symbol"
       >}</a
-      ><a name="2459"
+      ><a name="2457"
       >
 
 </a
-      ><a name="2461" class="Comment"
+      ><a name="2459" class="Comment"
       >-- data Type : Set</a
-      ><a name="2479"
+      ><a name="2477"
       >
 </a
-      ><a name="2480" class="Comment"
+      ><a name="2478" class="Comment"
       >-- data Lang : Type &#8594; Set</a
-      ><a name="2505"
+      ><a name="2503"
       >
 </a
-      ><a name="2506" class="Comment"
+      ><a name="2504" class="Comment"
       >-- data Type  where</a
-      ><a name="2525"
+      ><a name="2523"
       >
 </a
-      ><a name="2526" class="Comment"
+      ><a name="2524" class="Comment"
       >--   cat  : Type</a
-      ><a name="2542"
+      ><a name="2540"
       >
 </a
-      ><a name="2543" class="Comment"
+      ><a name="2541" class="Comment"
       >--   morph : Lang cat &#8594; Lang cat &#8594; Type</a
-      ><a name="2582"
+      ><a name="2580"
       >
 
 </a
-      ><a name="2584" class="Comment"
+      ><a name="2582" class="Comment"
       >-- data Lang  where</a
-      ><a name="2603"
+      ><a name="2601"
       >
 </a
-      ><a name="2604" class="Comment"
+      ><a name="2602" class="Comment"
       >--    empty : Lang cat</a
-      ><a name="2626"
+      ><a name="2624"
       >
 </a
-      ><a name="2627" class="Comment"
+      ><a name="2625" class="Comment"
       >--    id : (o : Lang cat) &#8594; Lang (morph o o)</a
-      ><a name="2671"
+      ><a name="2669"
       >
 </a
-      ><a name="2672" class="Comment"
+      ><a name="2670" class="Comment"
       >--    op hom : Lang cat &#8594; Lang cat</a
-      ><a name="2706"
+      ><a name="2704"
       >
 </a
-      ><a name="2707" class="Comment"
+      ><a name="2705" class="Comment"
       >--    point : (c : Lang cat) &#8594; Lang (morph empty c)</a
-      ><a name="2758"
+      ><a name="2756"
       >
 </a
-      ><a name="2759" class="Comment"
+      ><a name="2757" class="Comment"
       >--    comp : (o&#8321; o&#8322; o&#8323; : Lang cat) (f&#8321; : Lang (morph o&#8322; o&#8323;)) (f&#8322; : Lang (morph o&#8321; o&#8322;)) &#8594; Lang (morph o&#8321; o&#8323;)</a
-      ><a name="2866"
+      ><a name="2864"
       >
    
    
 </a
-      ><a name="2875" class="Comment"
+      ><a name="2873" class="Comment"
       >-- {- &#1042; &#1085;&#1072;&#1096;&#1077;&#1084; &#1084;&#1080;&#1088;&#1077; &#1082;&#1072;&#1090;&#1077;&#1075;&#1086;&#1088;&#1080;&#1081; &#1087;&#1086;&#1103;&#1074;&#1080;&#1083;&#1072;&#1089;&#1100; &#1087;&#1077;&#1088;&#1074;&#1072;&#1103; &#1082;&#1072;&#1090;&#1077;&#1075;&#1086;&#1088;&#1080;&#1103;. &#1054;&#1085;&#1072; &#1078;&#1077; - &#1087;&#1077;&#1088;&#1074;&#1099;&#1081; &quot;&#1086;&#1073;&#1098;&#1077;&#1082;&#1090;&quot;. &#1058;&#1077;&#1087;&#1077;&#1088;&#1100; &#1089; &#1087;&#1086;&#1084;&#1086;&#1097;&#1100;&#1102; &#1101;&#1090;&#1086;&#1075;&#1086; </a
-      ><a name="2981"
+      ><a name="2979"
       >
 </a
-      ><a name="2982" class="Comment"
+      ><a name="2980" class="Comment"
       >--    &#1087;&#1077;&#1088;&#1074;&#1086;&#1075;&#1086; &#1086;&#1073;&#1098;&#1077;&#1082;&#1090;&#1072; &#1084;&#1099; &#1085;&#1072;&#1095;&#1085;&#1077;&#1084; &#1089;&#1090;&#1088;&#1086;&#1080;&#1090;&#1100; &#1076;&#1072;&#1083;&#1100;&#1096;&#1077;. &#1055;&#1086;&#1082;&#1072; &#1085;&#1072;&#1084; &#1089;&#1090;&#1088;&#1086;&#1080;&#1090;&#1100; &#1086;&#1089;&#1086;&#1073;&#1086; &#1085;&#1077; &#1080;&#1079; &#1095;&#1077;&#1075;&#1086; - &#1086;&#1073;&#1098;&#1077;&#1082;&#1090; &#1091; &#1085;&#1072;&#1089; &#1074;&#1089;&#1077;&#1075;&#1086; &#1086;&#1076;&#1080;&#1085;.</a
-      ><a name="3090"
+      ><a name="3088"
       >
 </a
-      ><a name="3091" class="Comment"
+      ><a name="3089" class="Comment"
       >--    &#1053;&#1086;, &#1082;&#1072;&#1082; &#1090;&#1086;&#1083;&#1100;&#1082;&#1086; &#1087;&#1086;&#1103;&#1074;&#1083;&#1103;&#1102;&#1090;&#1089;&#1103; &#1086;&#1073;&#1098;&#1077;&#1082;&#1090;&#1099;, &#1087;&#1086;&#1103;&#1074;&#1083;&#1103;&#1077;&#1090;&#1089;&#1103; &#1074;&#1086;&#1079;&#1084;&#1086;&#1078;&#1085;&#1086;&#1089;&#1090;&#1100; &#1075;&#1086;&#1074;&#1086;&#1088;&#1080;&#1090;&#1100; &#1086;&#1073; &#1086;&#1090;&#1086;&#1073;&#1088;&#1072;&#1078;&#1077;&#1085;&#1080;&#1103;&#1093; &#1084;&#1077;&#1078;&#1076;&#1091; &#1085;&#1080;&#1084;&#1080;. </a
-      ><a name="3192"
+      ><a name="3190"
       >
 </a
-      ><a name="3193" class="Comment"
+      ><a name="3191" class="Comment"
       >--    &#1053;&#1072;&#1084; &#1085;&#1091;&#1078;&#1085;&#1099; &#1086;&#1090;&#1086;&#1073;&#1088;&#1072;&#1078;&#1077;&#1085;&#1080;&#1103; &#1084;&#1077;&#1078;&#1076;&#1091; &#1082;&#1072;&#1090;&#1077;&#1075;&#1086;&#1088;&#1080;&#1103;&#1084;&#1080;. &#1058;&#1072;&#1082;&#1080;&#1077; &#1086;&#1090;&#1086;&#1073;&#1088;&#1072;&#1078;&#1077;&#1085;&#1080;&#1103; &#1084;&#1099; &#1085;&#1072;&#1079;&#1086;&#1074;&#1077;&#1084; &#1092;&#1091;&#1085;&#1082;&#1090;&#1086;&#1088;&#1072;&#1084;&#1080;. </a
-      ><a name="3281"
+      ><a name="3279"
       >
 </a
-      ><a name="3282" class="Comment"
+      ><a name="3280" class="Comment"
       >--  -}     </a
-      ><a name="3293"
+      ><a name="3291"
       >
 
 
 </a
-      ><a name="3296" class="Comment"
+      ><a name="3294" class="Comment"
       >-- -- ============= &#1042;&#1089;&#1077; &#1101;&#1090;&#1086; &#1073;&#1091;&#1076;&#1077;&#1090; &#1091;&#1073;&#1088;&#1072;&#1085;&#1086; &#1080; &#1074;&#1099;&#1088;&#1072;&#1078;&#1077;&#1085;&#1086; &#1074; &#1090;&#1077;&#1088;&#1084;&#1080;&#1085;&#1072;&#1093; &#1092;&#1091;&#1085;&#1082;&#1090;&#1086;&#1088;&#1086;&#1074; &#1080; &#1084;&#1086;&#1088;&#1092;&#1080;&#1079;&#1084;&#1086;&#1074; =============-</a
-      ><a name="3395"
+      ><a name="3393"
       >
 
 
 </a
-      ><a name="3398" class="Comment"
+      ><a name="3396" class="Comment"
       >-- -- {- &#1063;&#1091;&#1076;&#1077;&#1089;&#1085;&#1099;&#1084; &#1089;&#1074;&#1086;&#1081;&#1089;&#1090;&#1074;&#1086;&#1084; &#1082;&#1072;&#1090;&#1077;&#1075;&#1086;&#1088;&#1080;&#1081; (&#1080; &#1086;&#1087;&#1088;&#1077;&#1076;&#1077;&#1083;&#1103;&#1077;&#1084;&#1099;&#1093; &#1089; &#1080;&#1093; &#1087;&#1086;&#1084;&#1086;&#1097;&#1100;&#1102; &#1087;&#1086;&#1085;&#1103;&#1090;&#1080;&#1081;) &#1103;&#1074;&#1083;&#1103;&#1077;&#1090;&#1089;&#1103; &#1076;&#1091;&#1072;&#1083;&#1100;&#1085;&#1086;&#1089;&#1090;&#1100;.</a
-      ><a name="3494"
+      ><a name="3492"
       >
 </a
-      ><a name="3495" class="Comment"
+      ><a name="3493" class="Comment"
       >-- --  - &#1045;&#1089;&#1083;&#1080; &#1074;&#1079;&#1103;&#1090;&#1100; &#1083;&#1102;&#1073;&#1091;&#1102; &#1082;&#1072;&#1090;&#1077;&#1075;&#1086;&#1088;&#1080;&#1102; &#1080; &#1088;&#1072;&#1079;&#1074;&#1077;&#1088;&#1085;&#1091;&#1090;&#1100; &#1074;&#1089;&#1077; &#1084;&#1086;&#1088;&#1092;&#1080;&#1079;&#1084;&#1099;, &#1090;&#1086; &#1087;&#1086;&#1083;&#1091;&#1095;&#1080;&#1084; &#1086;&#1087;&#1103;&#1090;&#1100; &#1082;&#1072;&#1090;&#1077;&#1075;&#1086;&#1088;&#1080;&#1102;. </a
-      ><a name="3586"
+      ><a name="3584"
       >
 </a
-      ><a name="3587" class="Comment"
+      ><a name="3585" class="Comment"
       >-- --   - &#1058;&#1072;&#1082;&#1080;&#1084; &#1086;&#1073;&#1088;&#1072;&#1079;&#1086;&#1084;, &#1084;&#1086;&#1078;&#1077;&#1084; &#1088;&#1072;&#1089;&#1089;&#1084;&#1072;&#1090;&#1088;&#1080;&#1074;&#1072;&#1090;&#1100; &#1086;&#1087;&#1077;&#1088;&#1072;&#1094;&#1080;&#1102; Opposite. &#1042;&#1086;&#1079;&#1100;&#1084;&#1077;&#1084; &#1077;&#1097;&#1077; &#1085;&#1077;&#1084;&#1085;&#1086;&#1075;&#1086; Agda</a
-      ><a name="3675"
+      ><a name="3673"
       >
 </a
-      ><a name="3676" class="Comment"
+      ><a name="3674" class="Comment"
       >-- --    &#1076;&#1083;&#1103; &#1086;&#1087;&#1088;&#1077;&#1076;&#1077;&#1083;&#1077;&#1085;&#1080;&#1103; &#1085;&#1091;&#1078;&#1085;&#1099;&#1093; &#1085;&#1072;&#1084; &#1087;&#1086;&#1085;&#1103;&#1090;&#1080;&#1081; -} </a
-      ><a name="3723"
+      ><a name="3721"
       >
 
 </a
-      ><a name="3725" class="Comment"
+      ><a name="3723" class="Comment"
       >-- -- Operation : {&#8467; : _ } (A : Set &#8467;) &#8594; Set &#8467;</a
-      ><a name="3771"
+      ><a name="3769"
       >
 </a
-      ><a name="3772" class="Comment"
+      ><a name="3770" class="Comment"
       >-- -- Operation A = A &#8594; A</a
-      ><a name="3797"
+      ><a name="3795"
       >
 
 </a
-      ><a name="3799" class="Comment"
+      ><a name="3797" class="Comment"
       >-- -- open import PropositionalEquivalence</a
-      ><a name="3841"
+      ><a name="3839"
       >
 </a
-      ><a name="3842" class="Comment"
+      ><a name="3840" class="Comment"
       >-- -- Involutive : {&#8467; : _} {A : Set &#8467;} &#8594; Operation A &#8594; Set &#8467;</a
-      ><a name="3902"
+      ><a name="3900"
       >
 </a
-      ><a name="3903" class="Comment"
+      ><a name="3901" class="Comment"
       >-- -- Involutive op = &#8704; a &#8594; op (op a) &#8801; a</a
-      ><a name="3944"
+      ><a name="3942"
       >
 
 </a
-      ><a name="3946" class="Comment"
+      ><a name="3944" class="Comment"
       >-- -- flip : {&#8467;&#8321; &#8467;&#8322; : _}{A B  : Set &#8467;&#8321;} {C : Set &#8467;&#8322;} &#8594; (A &#8594; B &#8594; C) &#8594; (B &#8594; A &#8594; C)</a
-      ><a name="4026"
+      ><a name="4024"
       >
 </a
-      ><a name="4027" class="Comment"
+      ><a name="4025" class="Comment"
       >-- -- flip f b a = f a b</a
-      ><a name="4051"
+      ><a name="4049"
       >
 
 </a
-      ><a name="4053" class="Comment"
+      ><a name="4051" class="Comment"
       >-- -- {- &#1057;&#1086;&#1073;&#1089;&#1090;&#1074;&#1077;&#1085;&#1085;&#1086;, &#1089;&#1072;&#1084;&#1072; &#1086;&#1087;&#1077;&#1088;&#1072;&#1094;&#1080;&#1103; &#1088;&#1072;&#1079;&#1074;&#1086;&#1088;&#1086;&#1090;&#1072; &#1089;&#1090;&#1088;&#1077;&#1083;&#1086;&#1082; -}</a
-      ><a name="4108"
+      ><a name="4106"
       >
 </a
-      ><a name="4109" class="Comment"
+      ><a name="4107" class="Comment"
       >-- -- Opposite : &#8704; {&#8467;} &#8594; Operation (Category &#8467;)</a
-      ><a name="4156"
+      ><a name="4154"
       >
 </a
-      ><a name="4157" class="Comment"
+      ><a name="4155" class="Comment"
       >-- -- Opposite c = record</a
-      ><a name="4182"
+      ><a name="4180"
       >
 </a
-      ><a name="4183" class="Comment"
+      ><a name="4181" class="Comment"
       >-- --                { Obj = Obj         -- &#1086;&#1073;&#1098;&#1077;&#1082;&#1090;&#1099; &#1090;&#1077; &#1078;&#1077;, &#1095;&#1090;&#1086; &#1080; &#1074; &#1080;&#1089;&#1093;&#1086;&#1076;&#1085;&#1086;&#1081; &#1082;&#1072;&#1090;&#1077;&#1075;&#1086;&#1088;&#1080;&#1080;&#1080;</a
-      ><a name="4269"
+      ><a name="4267"
       >
 </a
-      ><a name="4270" class="Comment"
+      ><a name="4268" class="Comment"
       >-- --                ; _&#8658;_ = flip _&#8658;_     -- &#1072; &#1074;&#1086;&#1090; &#1089;&#1090;&#1088;&#1077;&#1083;&#1082;&#1080; &#1085;&#1072;&#1087;&#1088;&#1072;&#1074;&#1083;&#1077;&#1085;&#1099; &#1074; &#1076;&#1088;&#1091;&#1075;&#1091;&#1102; &#1089;&#1090;&#1086;&#1088;&#1086;&#1085;&#1091;</a
-      ><a name="4356"
+      ><a name="4354"
       >
 </a
-      ><a name="4357" class="Comment"
+      ><a name="4355" class="Comment"
       >-- --                ; _&#8776;_  = _&#8776;_                    -- &#1088;&#1072;&#1074;&#1077;&#1085;&#1089;&#1090;&#1074;&#1086; &#1085;&#1077; &#1080;&#1079;&#1084;&#1077;&#1085;&#1080;&#1083;&#1086;&#1089;&#1100;</a
-      ><a name="4436"
+      ><a name="4434"
       >
 </a
-      ><a name="4437" class="Comment"
+      ><a name="4435" class="Comment"
       >-- --                ; id =  id</a
-      ><a name="4468"
+      ><a name="4466"
       >
 </a
-      ><a name="4469" class="Comment"
+      ><a name="4467" class="Comment"
       >-- --                ; _&#8728;_ = flip _&#8728;_</a
-      ><a name="4506"
+      ><a name="4504"
       >
 </a
-      ><a name="4507" class="Comment"
+      ><a name="4505" class="Comment"
       >-- --                ; &#8776;-equivalence = &#8776;-equivalence</a
-      ><a name="4559"
+      ><a name="4557"
       >
 </a