Commits

Pavel Perikov  committed 8efd99e

minors

  • Participants
  • Parent commits 124ad62

Comments (0)

Files changed (6)

File Category.agda

           ; identityʳ = λ {o₁} → λ {}
           ; ∘-assoc = λ {o₁} {o₂} {o₃} → λ {}
           }
- 
-{- В нашем мире категорий появилась первая категория. Она же - первый "объект". Теперь с помощью этого 
-   первого объекта мы начнем строить дальше -}     
+data OnlyEmpty {ℓ} : Category ℓ → Set ℓ where
+   empty : OnlyEmpty ∅
 
-{- Чудесным свойством категорий (и определяемых с их помощью понятий) является дуальность.
- - Если взять любую категорию и развернуть все морфизмы, то получим опять категорию. 
-  - Таким образом, можем рассматривать операцию Opposite. Возьмем еще немного Agda
-   для определения нужных нам понятий -} 
+CatWithEmpty  : {ℓ : _} →  Category (suc ℓ) 
+CatWithEmpty {ℓ} = record
+                     { Obj = OnlyEmpty ∅
+                     ; _⇒_ = λ { _ _ → OnlyEmpty ∅ }
+                     ; _≈_ = λ { _ _ → OnlyEmpty ∅ }
+                     ; id = λ {o} → empty
+                     ; _∘_ = λ {o₁} {o₂} {o₃} _ _ → empty
+                     ; ≈-equivalence = 
+                            record 
+                              { refl = λ {a} → empty
+                              ; sym = λ {a} {b} _ → empty
+                              ; trans = λ {a} {b} {c} _ _ → empty }
+                     ; ∘-resp-≈ = λ {o₁} {o₂} {o₃} {f₁} {f₁′} {f₂} {f₂′} _ _ → empty
+                     ; identityˡ = λ {o₁} {o₂} f → empty
+                     ; identityʳ = λ {o₁} {o₂} f → empty
+                     ; ∘-assoc = λ {o₁} {o₂} {o₃} {o₄} f₁ f₂ f₃ → empty
+                     }
 
-Operation : {ℓ : _ } (A : Set ℓ) → Set ℓ
-Operation A = A → A
+-- data Type : Set
+-- data Lang : Type → Set
+-- data Type  where
+--   cat  : Type
+--   morph : Lang cat → Lang cat → Type
 
-open import PropositionalEquivalence
-Involutive : {ℓ : _} {A : Set ℓ} → Operation A → Set ℓ
-Involutive op = ∀ a → op (op a) ≡ a
+-- data Lang  where
+--    empty : Lang cat
+--    id : (o : Lang cat) → Lang (morph o o)
+--    op hom : Lang cat → Lang cat
+--    point : (c : Lang cat) → Lang (morph empty c)
+--    comp : (o₁ o₂ o₃ : Lang cat) (f₁ : Lang (morph o₂ o₃)) (f₂ : Lang (morph o₁ o₂)) → Lang (morph o₁ o₃)
+   
+   
+-- {- В нашем мире категорий появилась первая категория. Она же - первый "объект". Теперь с помощью этого 
+--    первого объекта мы начнем строить дальше. Пока нам строить особо не из чего - объект у нас всего один.
+--    Но, как только появляются объекты, появляется возможность говорить об отображениях между ними. 
+--    Нам нужны отображения между категориями. Такие отображения мы назовем функторами. 
+--  -}     
 
-flip : {ℓ₁ ℓ₂ : _}{A B  : Set ℓ₁} {C : Set ℓ₂} → (A → B → C) → (B → A → C)
-flip f b a = f a b
 
-{- Собственно, сама операция разворота стрелок -}
-Opposite : ∀ {ℓ} → Operation (Category ℓ)
-Opposite c = record
-               { Obj = Obj         -- объекты те же, что и в исходной категориии
-               ; _⇒_ = flip _⇒_     -- а вот стрелки направлены в другую сторону
-               ; _≈_  = _≈_                    -- равенство не изменилось
-               ; id =  id
-               ; _∘_ = flip _∘_
-               ; ≈-equivalence = ≈-equivalence
-               ; ∘-resp-≈ =  flip ∘-resp-≈
-               ; identityˡ = identityʳ
-               ; identityʳ = identityˡ
-               ; ∘-assoc = λ f₁ f₂ f₃ → sym (∘-assoc _ _ _)
-               }
-         where
-           open Category c
-           open IsEquivalence {{...}}
+-- -- ============= Все это будет убрано и выражено в терминах функторов и морфизмов =============-
 
 
-{- Эта операция инволютивна -}
-opposite-involutive : ∀{ℓ} →  Involutive (Opposite {ℓ})
-opposite-involutive c =  ≡-refl
+-- -- {- Чудесным свойством категорий (и определяемых с их помощью понятий) является дуальность.
+-- --  - Если взять любую категорию и развернуть все морфизмы, то получим опять категорию. 
+-- --   - Таким образом, можем рассматривать операцию Opposite. Возьмем еще немного Agda
+-- --    для определения нужных нам понятий -} 
+
+-- -- Operation : {ℓ : _ } (A : Set ℓ) → Set ℓ
+-- -- Operation A = A → A
+
+-- -- open import PropositionalEquivalence
+-- -- Involutive : {ℓ : _} {A : Set ℓ} → Operation A → Set ℓ
+-- -- Involutive op = ∀ a → op (op a) ≡ a
+
+-- -- flip : {ℓ₁ ℓ₂ : _}{A B  : Set ℓ₁} {C : Set ℓ₂} → (A → B → C) → (B → A → C)
+-- -- flip f b a = f a b
+
+-- -- {- Собственно, сама операция разворота стрелок -}
+-- -- Opposite : ∀ {ℓ} → Operation (Category ℓ)
+-- -- Opposite c = record
+-- --                { Obj = Obj         -- объекты те же, что и в исходной категориии
+-- --                ; _⇒_ = flip _⇒_     -- а вот стрелки направлены в другую сторону
+-- --                ; _≈_  = _≈_                    -- равенство не изменилось
+-- --                ; id =  id
+-- --                ; _∘_ = flip _∘_
+-- --                ; ≈-equivalence = ≈-equivalence
+-- --                ; ∘-resp-≈ =  flip ∘-resp-≈
+-- --                ; identityˡ = identityʳ
+-- --                ; identityʳ = identityˡ
+-- --                ; ∘-assoc = λ f₁ f₂ f₃ → sym (∘-assoc _ _ _)
+-- --                }
+-- --          where
+-- --            open Category c
+-- --            open IsEquivalence {{...}}
+
+
+-- -- {- Эта операция инволютивна -}
+-- -- opposite-involutive : ∀{ℓ} →  Involutive (Opposite {ℓ})
+-- -- opposite-involutive c =  ≡-refl

File Equivalence.agda

 module Equivalence where
 open import Relations
 
+{- В этом модуле мы собираем свойства отношений в одну пачку, чтобы получить требования к отношению эквивалентности -}
+{- Отношение эквивалентности это такое бинарное отношение, которое является рефлексивным, транзитивным и симметричным -}
+
 record IsEquivalence {ℓ : _} {A : Set ℓ} (_≈_ : BinaryRelation A) : Set ℓ where
   open RelProperties _≈_
   field

File PropositionalEquivalence.agda

 module PropositionalEquivalence where
 
-data _≡_ {ℓ : _} {A : Set ℓ} (a : A) : A → Set ℓ where
-  ≡-refl : a ≡ a
+module _ {ℓ : _} {A : Set ℓ} where
 
-open import Relations
-module _ {ℓ : _} {A : Set ℓ} where
-   open RelProperties (_≡_ {ℓ} {A})
+   data _≡_ (a : A) : (b : A) → Set ℓ where
+      ≡-refl : a ≡ a
+
+   open import Relations
+   open RelProperties _≡_
 
    private
           ≡-reflexive : Reflexive 
           ≡-transitive ≡-refl ≡-refl = ≡-refl
   -- end private block
    open import Equivalence
-   ≡-is-equivalence : IsEquivalence (_≡_ {ℓ} {A})
+   ≡-is-equivalence : IsEquivalence _≡_ 
    ≡-is-equivalence = record
                     { refl = ≡-reflexive
                     ; sym = ≡-symmetric
                     ; trans = ≡-transitive }
 
-   subst : {ℓ : _} {A : Set ℓ} (P : A → Set ℓ)  {a b : A } (a≡b : a ≡ b) (pa : P a) → P b
+   subst :  (P : A → Set ℓ)  {a b : A } (a≡b : a ≡ b) (pa : P a) → P b
    subst P ≡-refl Pa = Pa
    
+cong : {ℓ : _} {A B : Set ℓ} (f : A → B) {a b : A} → a ≡ b → f a ≡ f b
+cong f ≡-refl = ≡-refl
+   
    

File html/Category.html

       >&#8594;</a
       ><a name="365"
       > </a
-      ><a name="366" href="Equivalence.html#56" class="Record"
+      ><a name="366" href="Equivalence.html#297" class="Record"
       >IsEquivalence</a
       ><a name="379"
       > </a
       >}</a
       ><a name="1522"
       >
- 
 </a
-      ><a name="1525" 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; 
-   &#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; -}</a
-      ><a name="1675"
-      >     
-
-</a
-      ><a name="1682" 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;.
- - &#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;. 
-  - &#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
-   &#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="1982"
-      > 
-
-</a
-      ><a name="1985" href="Category.html#1985" class="Function"
-      >Operation</a
-      ><a name="1994"
+      ><a name="1523" class="Keyword"
+      >data</a
+      ><a name="1527"
       > </a
-      ><a name="1995" class="Symbol"
+      ><a name="1528" href="Category.html#1528" class="Datatype"
+      >OnlyEmpty</a
+      ><a name="1537"
+      > </a
+      ><a name="1538" class="Symbol"
+      >{</a
+      ><a name="1539" href="Category.html#1539" class="Bound"
+      >&#8467;</a
+      ><a name="1540" class="Symbol"
+      >}</a
+      ><a name="1541"
+      > </a
+      ><a name="1542" class="Symbol"
       >:</a
-      ><a name="1996"
+      ><a name="1543"
       > </a
-      ><a name="1997" class="Symbol"
-      >{</a
-      ><a name="1998" href="Category.html#1998" class="Bound"
+      ><a name="1544" href="Category.html#97" class="Record"
+      >Category</a
+      ><a name="1552"
+      > </a
+      ><a name="1553" href="Category.html#1539" class="Bound"
       >&#8467;</a
-      ><a name="1999"
+      ><a name="1554"
       > </a
-      ><a name="2000" class="Symbol"
+      ><a name="1555" class="Symbol"
+      >&#8594;</a
+      ><a name="1556"
+      > </a
+      ><a name="1557" class="PrimitiveType"
+      >Set</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"
+      >where</a
+      ><a name="1568"
+      >
+   </a
+      ><a name="1572" href="Category.html#1572" class="InductiveConstructor"
+      >empty</a
+      ><a name="1577"
+      > </a
+      ><a name="1578" class="Symbol"
       >:</a
-      ><a name="2001"
+      ><a name="1579"
       > </a
-      ><a name="2002" class="Symbol"
-      >_</a
-      ><a name="2003"
+      ><a name="1580" href="Category.html#1528" class="Datatype"
+      >OnlyEmpty</a
+      ><a name="1589"
       > </a
-      ><a name="2004" class="Symbol"
-      >}</a
-      ><a name="2005"
-      > </a
-      ><a name="2006" class="Symbol"
-      >(</a
-      ><a name="2007" href="Category.html#2007" class="Bound"
-      >A</a
-      ><a name="2008"
-      > </a
-      ><a name="2009" class="Symbol"
-      >:</a
-      ><a name="2010"
-      > </a
-      ><a name="2011" class="PrimitiveType"
-      >Set</a
-      ><a name="2014"
-      > </a
-      ><a name="2015" href="Category.html#1998" class="Bound"
-      >&#8467;</a
-      ><a name="2016" class="Symbol"
-      >)</a
-      ><a name="2017"
-      > </a
-      ><a name="2018" class="Symbol"
-      >&#8594;</a
-      ><a name="2019"
-      > </a
-      ><a name="2020" class="PrimitiveType"
-      >Set</a
-      ><a name="2023"
-      > </a
-      ><a name="2024" href="Category.html#1998" class="Bound"
-      >&#8467;</a
-      ><a name="2025"
-      >
-</a
-      ><a name="2026" href="Category.html#1985" class="Function"
-      >Operation</a
-      ><a name="2035"
-      > </a
-      ><a name="2036" href="Category.html#2036" class="Bound"
-      >A</a
-      ><a name="2037"
-      > </a
-      ><a name="2038" class="Symbol"
-      >=</a
-      ><a name="2039"
-      > </a
-      ><a name="2040" href="Category.html#2036" class="Bound"
-      >A</a
-      ><a name="2041"
-      > </a
-      ><a name="2042" class="Symbol"
-      >&#8594;</a
-      ><a name="2043"
-      > </a
-      ><a name="2044" href="Category.html#2036" class="Bound"
-      >A</a
-      ><a name="2045"
+      ><a name="1590" href="Category.html#1118" class="Function"
+      >&#8709;</a
+      ><a name="1591"
       >
 
 </a
-      ><a name="2047" class="Keyword"
-      >open</a
-      ><a name="2051"
+      ><a name="1593" href="Category.html#1593" class="Function"
+      >CatWithEmpty</a
+      ><a name="1605"
+      >  </a
+      ><a name="1607" class="Symbol"
+      >:</a
+      ><a name="1608"
       > </a
-      ><a name="2052" class="Keyword"
-      >import</a
-      ><a name="2058"
+      ><a name="1609" class="Symbol"
+      >{</a
+      ><a name="1610" href="Category.html#1610" class="Bound"
+      >&#8467;</a
+      ><a name="1611"
       > </a
-      ><a name="2059" href="PropositionalEquivalence.html#1" class="Module"
-      >PropositionalEquivalence</a
+      ><a name="1612" class="Symbol"
+      >:</a
+      ><a name="1613"
+      > </a
+      ><a name="1614" class="Symbol"
+      >_}</a
+      ><a name="1616"
+      > </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
+      ><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"
+      >&#8467;</a
+      ><a name="1635" class="Symbol"
+      >)</a
+      ><a name="1636"
+      > 
+</a
+      ><a name="1638" href="Category.html#1593" class="Function"
+      >CatWithEmpty</a
+      ><a name="1650"
+      > </a
+      ><a name="1651" class="Symbol"
+      >{</a
+      ><a name="1652" href="Category.html#1652" class="Bound"
+      >&#8467;</a
+      ><a name="1653" class="Symbol"
+      >}</a
+      ><a name="1654"
+      > </a
+      ><a name="1655" class="Symbol"
+      >=</a
+      ><a name="1656"
+      > </a
+      ><a name="1657" class="Keyword"
+      >record</a
+      ><a name="1663"
+      >
+                     </a
+      ><a name="1685" class="Symbol"
+      >{</a
+      ><a name="1686"
+      > </a
+      ><a name="1687" class="Field"
+      >Obj</a
+      ><a name="1690"
+      > </a
+      ><a name="1691" class="Symbol"
+      >=</a
+      ><a name="1692"
+      > </a
+      ><a name="1693" href="Category.html#1528" class="Datatype"
+      >OnlyEmpty</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
+      ><a name="1727"
+      > </a
+      ><a name="1728" class="Field Operator"
+      >_&#8658;_</a
+      ><a name="1731"
+      > </a
+      ><a name="1732" class="Symbol"
+      >=</a
+      ><a name="1733"
+      > </a
+      ><a name="1734" class="Symbol"
+      >&#955;</a
+      ><a name="1735"
+      > </a
+      ><a name="1736" class="Symbol"
+      >{</a
+      ><a name="1737"
+      > </a
+      ><a name="1738" class="Symbol"
+      >_</a
+      ><a name="1739"
+      > </a
+      ><a name="1740" class="Symbol"
+      >_</a
+      ><a name="1741"
+      > </a
+      ><a name="1742" class="Symbol"
+      >&#8594;</a
+      ><a name="1743"
+      > </a
+      ><a name="1744" href="Category.html#1528" class="Datatype"
+      >OnlyEmpty</a
+      ><a name="1753"
+      > </a
+      ><a name="1754" href="Category.html#1118" class="Function"
+      >&#8709;</a
+      ><a name="1755"
+      > </a
+      ><a name="1756" class="Symbol"
+      >}</a
+      ><a name="1757"
+      >
+                     </a
+      ><a name="1779" class="Symbol"
+      >;</a
+      ><a name="1780"
+      > </a
+      ><a name="1781" class="Field Operator"
+      >_&#8776;_</a
+      ><a name="1784"
+      > </a
+      ><a name="1785" class="Symbol"
+      >=</a
+      ><a name="1786"
+      > </a
+      ><a name="1787" class="Symbol"
+      >&#955;</a
+      ><a name="1788"
+      > </a
+      ><a name="1789" class="Symbol"
+      >{</a
+      ><a name="1790"
+      > </a
+      ><a name="1791" class="Symbol"
+      >_</a
+      ><a name="1792"
+      > </a
+      ><a name="1793" class="Symbol"
+      >_</a
+      ><a name="1794"
+      > </a
+      ><a name="1795" class="Symbol"
+      >&#8594;</a
+      ><a name="1796"
+      > </a
+      ><a name="1797" href="Category.html#1528" class="Datatype"
+      >OnlyEmpty</a
+      ><a name="1806"
+      > </a
+      ><a name="1807" href="Category.html#1118" class="Function"
+      >&#8709;</a
+      ><a name="1808"
+      > </a
+      ><a name="1809" class="Symbol"
+      >}</a
+      ><a name="1810"
+      >
+                     </a
+      ><a name="1832" class="Symbol"
+      >;</a
+      ><a name="1833"
+      > </a
+      ><a name="1834" class="Field"
+      >id</a
+      ><a name="1836"
+      > </a
+      ><a name="1837" class="Symbol"
+      >=</a
+      ><a name="1838"
+      > </a
+      ><a name="1839" class="Symbol"
+      >&#955;</a
+      ><a name="1840"
+      > </a
+      ><a name="1841" class="Symbol"
+      >{</a
+      ><a name="1842" href="Category.html#1842" class="Bound"
+      >o</a
+      ><a name="1843" class="Symbol"
+      >}</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"
+      >empty</a
+      ><a name="1852"
+      >
+                     </a
+      ><a name="1874" class="Symbol"
+      >;</a
+      ><a name="1875"
+      > </a
+      ><a name="1876" class="Field Operator"
+      >_&#8728;_</a
+      ><a name="1879"
+      > </a
+      ><a name="1880" class="Symbol"
+      >=</a
+      ><a name="1881"
+      > </a
+      ><a name="1882" class="Symbol"
+      >&#955;</a
+      ><a name="1883"
+      > </a
+      ><a name="1884" class="Symbol"
+      >{</a
+      ><a name="1885" href="Category.html#1885" class="Bound"
+      >o&#8321;</a
+      ><a name="1887" class="Symbol"
+      >}</a
+      ><a name="1888"
+      > </a
+      ><a name="1889" class="Symbol"
+      >{</a
+      ><a name="1890" href="Category.html#1890" class="Bound"
+      >o&#8322;</a
+      ><a name="1892" class="Symbol"
+      >}</a
+      ><a name="1893"
+      > </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="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="1902"
+      > </a
+      ><a name="1903" class="Symbol"
+      >&#8594;</a
+      ><a name="1904"
+      > </a
+      ><a name="1905" href="Category.html#1572" class="InductiveConstructor"
+      >empty</a
+      ><a name="1910"
+      >
+                     </a
+      ><a name="1932" class="Symbol"
+      >;</a
+      ><a name="1933"
+      > </a
+      ><a name="1934" class="Field"
+      >&#8776;-equivalence</a
+      ><a name="1947"
+      > </a
+      ><a name="1948" class="Symbol"
+      >=</a
+      ><a name="1949"
+      > 
+                            </a
+      ><a name="1979" class="Keyword"
+      >record</a
+      ><a name="1985"
+      > 
+                              </a
+      ><a name="2017" class="Symbol"
+      >{</a
+      ><a name="2018"
+      > </a
+      ><a name="2019" class="Field"
+      >refl</a
+      ><a name="2023"
+      > </a
+      ><a name="2024" class="Symbol"
+      >=</a
+      ><a name="2025"
+      > </a
+      ><a name="2026" class="Symbol"
+      >&#955;</a
+      ><a name="2027"
+      > </a
+      ><a name="2028" class="Symbol"
+      >{</a
+      ><a name="2029" href="Category.html#2029" class="Bound"
+      >a</a
+      ><a name="2030" class="Symbol"
+      >}</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"
+      >empty</a
+      ><a name="2039"
+      >
+                              </a
+      ><a name="2070" class="Symbol"
+      >;</a
+      ><a name="2071"
+      > </a
+      ><a name="2072" class="Field"
+      >sym</a
+      ><a name="2075"
+      > </a
+      ><a name="2076" class="Symbol"
+      >=</a
+      ><a name="2077"
+      > </a
+      ><a name="2078" class="Symbol"
+      >&#955;</a
+      ><a name="2079"
+      > </a
+      ><a name="2080" class="Symbol"
+      >{</a
+      ><a name="2081" href="Category.html#2081" class="Bound"
+      >a</a
+      ><a name="2082" class="Symbol"
+      >}</a
       ><a name="2083"
+      > </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="2087"
+      > </a
+      ><a name="2088" href="Category.html#2088" class="Bound"
+      >_</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"
+      >empty</a
+      ><a name="2097"
       >
-</a
-      ><a name="2084" href="Category.html#2084" class="Function"
-      >Involutive</a
-      ><a name="2094"
+                              </a
+      ><a name="2128" class="Symbol"
+      >;</a
+      ><a name="2129"
       > </a
-      ><a name="2095" class="Symbol"
-      >:</a
-      ><a name="2096"
+      ><a name="2130" class="Field"
+      >trans</a
+      ><a name="2135"
       > </a
-      ><a name="2097" class="Symbol"
+      ><a name="2136" class="Symbol"
+      >=</a
+      ><a name="2137"
+      > </a
+      ><a name="2138" class="Symbol"
+      >&#955;</a
+      ><a name="2139"
+      > </a
+      ><a name="2140" class="Symbol"
       >{</a
-      ><a name="2098" href="Category.html#2098" class="Bound"
-      >&#8467;</a
-      ><a name="2099"
+      ><a name="2141" href="Category.html#2141" class="Bound"
+      >a</a
+      ><a name="2142" class="Symbol"
+      >}</a
+      ><a name="2143"
       > </a
-      ><a name="2100" class="Symbol"
-      >:</a
-      ><a name="2101"
+      ><a name="2144" class="Symbol"
+      >{</a
+      ><a name="2145" href="Category.html#2145" class="Bound"
+      >b</a
+      ><a name="2146" class="Symbol"
+      >}</a
+      ><a name="2147"
       > </a
-      ><a name="2102" class="Symbol"
-      >_}</a
-      ><a name="2104"
+      ><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="2151"
       > </a
-      ><a name="2105" class="Symbol"
-      >{</a
-      ><a name="2106" href="Category.html#2106" class="Bound"
-      >A</a
-      ><a name="2107"
+      ><a name="2152" href="Category.html#2152" class="Bound"
+      >_</a
+      ><a name="2153"
       > </a
-      ><a name="2108" class="Symbol"
-      >:</a
-      ><a name="2109"
+      ><a name="2154" href="Category.html#2154" class="Bound"
+      >_</a
+      ><a name="2155"
       > </a
-      ><a name="2110" class="PrimitiveType"
-      >Set</a
-      ><a name="2113"
+      ><a name="2156" class="Symbol"
+      >&#8594;</a
+      ><a name="2157"
       > </a
-      ><a name="2114" href="Category.html#2098" class="Bound"
-      >&#8467;</a
-      ><a name="2115" class="Symbol"
-      >}</a
-      ><a name="2116"
-      > </a
-      ><a name="2117" class="Symbol"
-      >&#8594;</a
-      ><a name="2118"
-      > </a
-      ><a name="2119" href="Category.html#1985" class="Function"
-      >Operation</a
-      ><a name="2128"
-      > </a
-      ><a name="2129" href="Category.html#2106" class="Bound"
-      >A</a
-      ><a name="2130"
-      > </a
-      ><a name="2131" class="Symbol"
-      >&#8594;</a
-      ><a name="2132"
-      > </a
-      ><a name="2133" class="PrimitiveType"
-      >Set</a
-      ><a name="2136"
-      > </a
-      ><a name="2137" href="Category.html#2098" class="Bound"
-      >&#8467;</a
-      ><a name="2138"
-      >
-</a
-      ><a name="2139" href="Category.html#2084" class="Function"
-      >Involutive</a
-      ><a name="2149"
-      > </a
-      ><a name="2150" href="Category.html#2150" class="Bound"
-      >op</a
-      ><a name="2152"
-      > </a
-      ><a name="2153" class="Symbol"
-      >=</a
-      ><a name="2154"
-      > </a
-      ><a name="2155" class="Symbol"
-      >&#8704;</a
-      ><a name="2156"
-      > </a
-      ><a name="2157" href="Category.html#2157" class="Bound"
-      >a</a
-      ><a name="2158"
-      > </a
-      ><a name="2159" class="Symbol"
-      >&#8594;</a
-      ><a name="2160"
-      > </a
-      ><a name="2161" href="Category.html#2150" class="Bound"
-      >op</a
+      ><a name="2158" href="Category.html#1572" class="InductiveConstructor"
+      >empty</a
       ><a name="2163"
       > </a
       ><a name="2164" class="Symbol"
-      >(</a
-      ><a name="2165" href="Category.html#2150" class="Bound"
-      >op</a
-      ><a name="2167"
+      >}</a
+      ><a name="2165"
+      >
+                     </a
+      ><a name="2187" class="Symbol"
+      >;</a
+      ><a name="2188"
       > </a
-      ><a name="2168" href="Category.html#2157" class="Bound"
-      >a</a
-      ><a name="2169" class="Symbol"
-      >)</a
-      ><a name="2170"
+      ><a name="2189" class="Field"
+      >&#8728;-resp-&#8776;</a
+      ><a name="2197"
       > </a
-      ><a name="2171" href="PropositionalEquivalence.html#45" class="Datatype Operator"
-      >&#8801;</a
-      ><a name="2172"
+      ><a name="2198" class="Symbol"
+      >=</a
+      ><a name="2199"
       > </a
-      ><a name="2173" href="Category.html#2157" class="Bound"
-      >a</a
-      ><a name="2174"
+      ><a name="2200" class="Symbol"
+      >&#955;</a
+      ><a name="2201"
+      > </a
+      ><a name="2202" class="Symbol"
+      >{</a
+      ><a name="2203" href="Category.html#2203" class="Bound"
+      >o&#8321;</a
+      ><a name="2205" class="Symbol"
+      >}</a
+      ><a name="2206"
+      > </a
+      ><a name="2207" class="Symbol"
+      >{</a
+      ><a name="2208" href="Category.html#2208" class="Bound"
+      >o&#8322;</a
+      ><a name="2210" class="Symbol"
+      >}</a
+      ><a name="2211"
+      > </a
+      ><a name="2212" class="Symbol"
+      >{</a
+      ><a name="2213" href="Category.html#2213" class="Bound"
+      >o&#8323;</a
+      ><a name="2215" class="Symbol"
+      >}</a
+      ><a name="2216"
+      > </a
+      ><a name="2217" class="Symbol"
+      >{</a
+      ><a name="2218" href="Category.html#2218" class="Bound"
+      >f&#8321;</a
+      ><a name="2220" class="Symbol"
+      >}</a
+      ><a name="2221"
+      > </a
+      ><a name="2222" class="Symbol"
+      >{</a
+      ><a name="2223" href="Category.html#2223" class="Bound"
+      >f&#8321;&#8242;</a
+      ><a name="2226" class="Symbol"
+      >}</a
+      ><a name="2227"
+      > </a
+      ><a name="2228" class="Symbol"
+      >{</a
+      ><a name="2229" href="Category.html#2229" class="Bound"
+      >f&#8322;</a
+      ><a name="2231" class="Symbol"
+      >}</a
+      ><a name="2232"
+      > </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="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="2242"
+      > </a
+      ><a name="2243" class="Symbol"
+      >&#8594;</a
+      ><a name="2244"
+      > </a
+      ><a name="2245" href="Category.html#1572" class="InductiveConstructor"
+      >empty</a
+      ><a name="2250"
+      >
+                     </a
+      ><a name="2272" class="Symbol"
+      >;</a
+      ><a name="2273"
+      > </a
+      ><a name="2274" class="Field"
+      >identity&#737;</a
+      ><a name="2283"
+      > </a
+      ><a name="2284" class="Symbol"
+      >=</a
+      ><a name="2285"
+      > </a
+      ><a name="2286" class="Symbol"
+      >&#955;</a
+      ><a name="2287"
+      > </a
+      ><a name="2288" class="Symbol"
+      >{</a
+      ><a name="2289" href="Category.html#2289" class="Bound"
+      >o&#8321;</a
+      ><a name="2291" class="Symbol"
+      >}</a
+      ><a name="2292"
+      > </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="2297"
+      > </a
+      ><a name="2298" href="Category.html#2298" class="Bound"
+      >f</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"
+      >empty</a
+      ><a name="2307"
+      >
+                     </a
+      ><a name="2329" class="Symbol"
+      >;</a
+      ><a name="2330"
+      > </a
+      ><a name="2331" class="Field"
+      >identity&#691;</a
+      ><a name="2340"
+      > </a
+      ><a name="2341" class="Symbol"
+      >=</a
+      ><a name="2342"
+      > </a
+      ><a name="2343" class="Symbol"
+      >&#955;</a
+      ><a name="2344"
+      > </a
+      ><a name="2345" class="Symbol"
+      >{</a
+      ><a name="2346" href="Category.html#2346" class="Bound"
+      >o&#8321;</a
+      ><a name="2348" class="Symbol"
+      >}</a
+      ><a name="2349"
+      > </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="2354"
+      > </a
+      ><a name="2355" href="Category.html#2355" class="Bound"
+      >f</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"
+      >empty</a
+      ><a name="2364"
+      >
+                     </a
+      ><a name="2386" class="Symbol"
+      >;</a
+      ><a name="2387"
+      > </a
+      ><a name="2388" class="Field"
+      >&#8728;-assoc</a
+      ><a name="2395"
+      > </a
+      ><a name="2396" class="Symbol"
+      >=</a
+      ><a name="2397"
+      > </a
+      ><a name="2398" class="Symbol"
+      >&#955;</a
+      ><a name="2399"
+      > </a
+      ><a name="2400" class="Symbol"
+      >{</a
+      ><a name="2401" href="Category.html#2401" class="Bound"
+      >o&#8321;</a
+      ><a name="2403" class="Symbol"
+      >}</a
+      ><a name="2404"
+      > </a
+      ><a name="2405" class="Symbol"
+      >{</a
+      ><a name="2406" href="Category.html#2406" class="Bound"
+      >o&#8322;</a
+      ><a name="2408" class="Symbol"
+      >}</a
+      ><a name="2409"
+      > </a
+      ><a name="2410" class="Symbol"
+      >{</a
+      ><a name="2411" href="Category.html#2411" class="Bound"
+      >o&#8323;</a
+      ><a name="2413" class="Symbol"
+      >}</a
+      ><a name="2414"
+      > </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
+      ><a name="2420" href="Category.html#2420" class="Bound"
+      >f&#8321;</a
+      ><a name="2422"
+      > </a
+      ><a name="2423" href="Category.html#2423" class="Bound"
+      >f&#8322;</a
+      ><a name="2425"
+      > </a
+      ><a name="2426" href="Category.html#2426" class="Bound"
+      >f&#8323;</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"
+      >empty</a
+      ><a name="2436"
+      >
+                     </a
+      ><a name="2458" class="Symbol"
+      >}</a
+      ><a name="2459"
       >
 
 </a
-      ><a name="2176" href="Category.html#2176" class="Function"
-      >flip</a
-      ><a name="2180"
-      > </a
-      ><a name="2181" class="Symbol"
-      >:</a
-      ><a name="2182"
-      > </a
-      ><a name="2183" class="Symbol"
-      >{</a
-      ><a name="2184" href="Category.html#2184" class="Bound"
-      >&#8467;&#8321;</a
-      ><a name="2186"
-      > </a
-      ><a name="2187" href="Category.html#2187" class="Bound"
-      >&#8467;&#8322;</a
-      ><a name="2189"
-      > </a
-      ><a name="2190" class="Symbol"
-      >:</a
-      ><a name="2191"
-      > </a
-      ><a name="2192" class="Symbol"
-      >_}{</a
-      ><a name="2195" href="Category.html#2195" class="Bound"
-      >A</a
-      ><a name="2196"
-      > </a
-      ><a name="2197" href="Category.html#2197" class="Bound"
-      >B</a
-      ><a name="2198"
-      >  </a
-      ><a name="2200" class="Symbol"
-      >:</a
-      ><a name="2201"
-      > </a
-      ><a name="2202" class="PrimitiveType"
-      >Set</a
-      ><a name="2205"
-      > </a
-      ><a name="2206" href="Category.html#2184" class="Bound"
-      >&#8467;&#8321;</a
-      ><a name="2208" class="Symbol"
-      >}</a
-      ><a name="2209"
-      > </a
-      ><a name="2210" class="Symbol"
-      >{</a
-      ><a name="2211" href="Category.html#2211" class="Bound"
-      >C</a
-      ><a name="2212"
-      > </a
-      ><a name="2213" class="Symbol"
-      >:</a
-      ><a name="2214"
-      > </a
-      ><a name="2215" class="PrimitiveType"
-      >Set</a
-      ><a name="2218"
-      > </a
-      ><a name="2219" href="Category.html#2187" class="Bound"
-      >&#8467;&#8322;</a
-      ><a name="2221" class="Symbol"
-      >}</a
-      ><a name="2222"
-      > </a
-      ><a name="2223" class="Symbol"
-      >&#8594;</a
-      ><a name="2224"
-      > </a
-      ><a name="2225" class="Symbol"
-      >(</a
-      ><a name="2226" href="Category.html#2195" class="Bound"
-      >A</a
-      ><a name="2227"
-      > </a
-      ><a name="2228" class="Symbol"
-      >&#8594;</a
-      ><a name="2229"
-      > </a
-      ><a name="2230" href="Category.html#2197" class="Bound"
-      >B</a
-      ><a name="2231"
-      > </a
-      ><a name="2232" class="Symbol"
-      >&#8594;</a
-      ><a name="2233"
-      > </a
-      ><a name="2234" href="Category.html#2211" class="Bound"
-      >C</a
-      ><a name="2235" class="Symbol"
-      >)</a
-      ><a name="2236"
-      > </a
-      ><a name="2237" class="Symbol"
-      >&#8594;</a
-      ><a name="2238"
-      > </a
-      ><a name="2239" class="Symbol"
-      >(</a
-      ><a name="2240" href="Category.html#2197" class="Bound"
-      >B</a
-      ><a name="2241"
-      > </a
-      ><a name="2242" class="Symbol"
-      >&#8594;</a
-      ><a name="2243"
-      > </a
-      ><a name="2244" href="Category.html#2195" class="Bound"
-      >A</a
-      ><a name="2245"
-      > </a
-      ><a name="2246" class="Symbol"
-      >&#8594;</a
-      ><a name="2247"
-      > </a
-      ><a name="2248" href="Category.html#2211" class="Bound"
-      >C</a
-      ><a name="2249" class="Symbol"
-      >)</a
-      ><a name="2250"
+      ><a name="2461" class="Comment"
+      >-- data Type : Set</a
+      ><a name="2479"
       >
 </a
-      ><a name="2251" href="Category.html#2176" class="Function"
-      >flip</a
-      ><a name="2255"
-      > </a
-      ><a name="2256" href="Category.html#2256" class="Bound"
-      >f</a
-      ><a name="2257"
-      > </a
-      ><a name="2258" href="Category.html#2258" class="Bound"
-      >b</a
-      ><a name="2259"
-      > </a
-      ><a name="2260" href="Category.html#2260" class="Bound"
-      >a</a
-      ><a name="2261"
-      > </a
-      ><a name="2262" class="Symbol"
-      >=</a
-      ><a name="2263"
-      > </a
-      ><a name="2264" href="Category.html#2256" class="Bound"
-      >f</a
-      ><a name="2265"
-      > </a
-      ><a name="2266" href="Category.html#2260" class="Bound"
-      >a</a
-      ><a name="2267"
-      > </a
-      ><a name="2268" href="Category.html#2258" class="Bound"
-      >b</a
-      ><a name="2269"
+      ><a name="2480" class="Comment"
+      >-- data Lang : Type &#8594; Set</a
+      ><a name="2505"
+      >
+</a
+      ><a name="2506" class="Comment"
+      >-- data Type  where</a
+      ><a name="2525"
+      >
+</a
+      ><a name="2526" class="Comment"
+      >--   cat  : Type</a
+      ><a name="2542"
+      >
+</a
+      ><a name="2543" class="Comment"
+      >--   morph : Lang cat &#8594; Lang cat &#8594; Type</a
+      ><a name="2582"
       >
 
 </a
-      ><a name="2271" 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="2320"
+      ><a name="2584" class="Comment"
+      >-- data Lang  where</a
+      ><a name="2603"
       >
 </a
-      ><a name="2321" href="Category.html#2321" class="Function"
-      >Opposite</a
-      ><a name="2329"
-      > </a
-      ><a name="2330" class="Symbol"
-      >:</a
-      ><a name="2331"
-      > </a
-      ><a name="2332" class="Symbol"
-      >&#8704;</a
-      ><a name="2333"
-      > </a
-      ><a name="2334" class="Symbol"
-      >{</a
-      ><a name="2335" href="Category.html#2335" class="Bound"
-      >&#8467;</a
-      ><a name="2336" class="Symbol"
-      >}</a
-      ><a name="2337"
-      > </a
-      ><a name="2338" class="Symbol"
-      >&#8594;</a
-      ><a name="2339"
-      > </a
-      ><a name="2340" href="Category.html#1985" class="Function"
-      >Operation</a
-      ><a name="2349"
-      > </a
-      ><a name="2350" class="Symbol"
-      >(</a
-      ><a name="2351" href="Category.html#97" class="Record"
-      >Category</a
-      ><a name="2359"
-      > </a
-      ><a name="2360" href="Category.html#2335" class="Bound"
-      >&#8467;</a
-      ><a name="2361" class="Symbol"
-      >)</a
-      ><a name="2362"
+      ><a name="2604" class="Comment"
+      >--    empty : Lang cat</a
+      ><a name="2626"
       >
 </a
-      ><a name="2363" href="Category.html#2321" class="Function"
-      >Opposite</a
-      ><a name="2371"
-      > </a
-      ><a name="2372" href="Category.html#2372" class="Bound"
-      >c</a
-      ><a name="2373"
-      > </a
-      ><a name="2374" class="Symbol"
-      >=</a
-      ><a name="2375"
-      > </a
-      ><a name="2376" class="Keyword"
-      >record</a
-      ><a name="2382"
-      >
-               </a
-      ><a name="2398" class="Symbol"
-      >{</a
-      ><a name="2399"
-      > </a
-      ><a name="2400" class="Field"
-      >Obj</a
-      ><a name="2403"
-      > </a
-      ><a name="2404" class="Symbol"
-      >=</a
-      ><a name="2405"
-      > </a
-      ><a name="2406" href="Category.html#148" class="Function"
-      >Obj</a
-      ><a name="2409"
-      >         </a
-      ><a name="2418" class="Comment"
-      >-- &#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="2463"
-      >
-               </a
-      ><a name="2479" class="Symbol"
-      >;</a
-      ><a name="2480"
-      > </a
-      ><a name="2481" class="Field Operator"
-      >_&#8658;_</a
-      ><a name="2484"
-      > </a
-      ><a name="2485" class="Symbol"
-      >=</a
-      ><a name="2486"
-      > </a
-      ><a name="2487" href="Category.html#2176" class="Function"
-      >flip</a
-      ><a name="2491"
-      > </a
-      ><a name="2492" href="Category.html#166" class="Function Operator"
-      >_&#8658;_</a
-      ><a name="2495"
-      >     </a
-      ><a name="2500" class="Comment"
-      >-- &#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="2544"
-      >
-               </a
-      ><a name="2560" class="Symbol"
-      >;</a
-      ><a name="2561"
-      > </a
-      ><a name="2562" class="Field Operator"
-      >_&#8776;_</a
-      ><a name="2565"
-      >  </a
-      ><a name="2567" class="Symbol"
-      >=</a
-      ><a name="2568"
-      > </a
-      ><a name="2569" href="Category.html#196" class="Function Operator"
-      >_&#8776;_</a
-      ><a name="2572"
-      >                    </a
-      ><a name="2592" class="Comment"
-      >-- &#1088;&#1072;&#1074;&#1077;&#1085;&#1089;&#1090;&#1074;&#1086; &#1085;&#1077; &#1080;&#1079;&#1084;&#1077;&#1085;&#1080;&#1083;&#1086;&#1089;&#1100;</a
-      ><a name="2618"
-      >
-               </a
-      ><a name="2634" class="Symbol"
-      >;</a
-      ><a name="2635"
-      > </a
-      ><a name="2636" class="Field"
-      >id</a
-      ><a name="2638"
-      > </a
-      ><a name="2639" class="Symbol"
-      >=</a
-      ><a name="2640"
-      >  </a
-      ><a name="2642" href="Category.html#409" class="Function"
-      >id</a
-      ><a name="2644"
-      >
-               </a
-      ><a name="2660" class="Symbol"
-      >;</a
-      ><a name="2661"
-      > </a
-      ><a name="2662" class="Field Operator"
-      >_&#8728;_</a
-      ><a name="2665"
-      > </a
-      ><a name="2666" class="Symbol"
-      >=</a
-      ><a name="2667"
-      > </a
-      ><a name="2668" href="Category.html#2176" class="Function"
-      >flip</a
-      ><a name="2672"
-      > </a
-      ><a name="2673" href="Category.html#427" class="Function Operator"
-      >_&#8728;_</a
-      ><a name="2676"
-      >
-               </a
-      ><a name="2692" class="Symbol"
-      >;</a
-      ><a name="2693"
-      > </a
-      ><a name="2694" class="Field"
-      >&#8776;-equivalence</a
-      ><a name="2707"
-      > </a
-      ><a name="2708" class="Symbol"
-      >=</a
-      ><a name="2709"
-      > </a
-      ><a name="2710" href="Category.html#480" class="Function"
-      >&#8776;-equivalence</a
-      ><a name="2723"
-      >
-               </a
-      ><a name="2739" class="Symbol"
-      >;</a
-      ><a name="2740"
-      > </a
-      ><a name="2741" class="Field"
-      >&#8728;-resp-&#8776;</a
-      ><a name="2749"
-      > </a
-      ><a name="2750" class="Symbol"
-      >=</a
-      ><a name="2751"
-      >  </a
-      ><a name="2753" href="Category.html#2176" class="Function"
-      >flip</a
-      ><a name="2757"
-      > </a
-      ><a name="2758" href="Category.html#521" class="Function"
-      >&#8728;-resp-&#8776;</a
-      ><a name="2766"
-      >
-               </a
-      ><a name="2782" class="Symbol"
-      >;</a
-      ><a name="2783"
-      > </a
-      ><a name="2784" class="Field"
-      >identity&#737;</a
-      ><a name="2793"
-      > </a
-      ><a name="2794" class="Symbol"
-      >=</a
-      ><a name="2795"
-      > </a
-      ><a name="2796" href="Category.html#698" class="Function"
-      >identity&#691;</a
-      ><a name="2805"
-      >
-               </a
-      ><a name="2821" class="Symbol"
-      >;</a
-      ><a name="2822"
-      > </a
-      ><a name="2823" class="Field"
-      >identity&#691;</a
-      ><a name="2832"
-      > </a
-      ><a name="2833" class="Symbol"
-      >=</a
-      ><a name="2834"
-      > </a
-      ><a name="2835" href="Category.html#639" class="Function"
-      >identity&#737;</a
-      ><a name="2844"
-      >
-               </a
-      ><a name="2860" class="Symbol"
-      >;</a
-      ><a name="2861"
-      > </a
-      ><a name="2862" class="Field"
-      >&#8728;-assoc</a
-      ><a name="2869"
-      > </a
-      ><a name="2870" class="Symbol"
-      >=</a
-      ><a name="2871"
-      > </a
-      ><a name="2872" class="Symbol"
-      >&#955;</a
-      ><a name="2873"
-      > </a
-      ><a name="2874" href="Category.html#2874" class="Bound"
-      >f&#8321;</a
-      ><a name="2876"
-      > </a
-      ><a name="2877" href="Category.html#2877" class="Bound"
-      >f&#8322;</a
-      ><a name="2879"
-      > </a
-      ><a name="2880" href="Category.html#2880" class="Bound"
-      >f&#8323;</a
-      ><a name="2882"
-      > </a
-      ><a name="2883" class="Symbol"
-      >&#8594;</a
-      ><a name="2884"
-      > </a
-      ><a name="2885" href="Equivalence.html#188" class="Function"
-      >sym</a
-      ><a name="2888"
-      > </a
-      ><a name="2889" class="Symbol"
-      >(</a
-      ><a name="2890" href="Category.html#757" class="Function"
-      >&#8728;-assoc</a
-      ><a name="2897"
-      > </a
-      ><a name="2898" class="Symbol"
-      >_</a
-      ><a name="2899"
-      > </a
-      ><a name="2900" class="Symbol"
-      >_</a
-      ><a name="2901"
-      > </a
-      ><a name="2902" class="Symbol"
-      >_)</a
-      ><a name="2904"
-      >
-               </a
-      ><a name="2920" class="Symbol"
-      >}</a
-      ><a name="2921"
-      >
-         </a
-      ><a name="2931" class="Keyword"
-      >where</a
-      ><a name="2936"
-      >
-           </a
-      ><a name="2948" class="Keyword"
-      >open</a
-      ><a name="2952"
-      > </a
-      ><a name="2953" href="Category.html#97" class="Module"
-      >Category</a
-      ><a name="2961"
-      > </a
-      ><a name="2962" href="Category.html#2372" class="Bound"
-      >c</a
-      ><a name="2963"
-      >
-           </a
-      ><a name="2975" class="Keyword"
-      >open</a
-      ><a name="2979"
-      > </a
-      ><a name="2980" href="Equivalence.html#56" class="Module"
-      >IsEquivalence</a
-      ><a name="2993"
-      > </a
-      ><a name="2994" class="Symbol"
-      >{{...}}</a
-      ><a name="3001"
-      >
-
-
-</a
-      ><a name="3004" class="Comment"
-      >{- &#1069;&#1090;&#1072; &#1086;&#1087;&#1077;&#1088;&#1072;&#1094;&#1080;&#1103; &#1080;&#1085;&#1074;&#1086;&#1083;&#1102;&#1090;&#1080;&#1074;&#1085;&#1072; -}</a
-      ><a name="3034"
+      ><a name="2627" class="Comment"
+      >--    id : (o : Lang cat) &#8594; Lang (morph o o)</a
+      ><a name="2671"
       >
 </a
-      ><a name="3035" href="Category.html#3035" class="Function"
-      >opposite-involutive</a
-      ><a name="3054"
-      > </a
-      ><a name="3055" class="Symbol"
-      >:</a
-      ><a name="3056"
-      > </a
-      ><a name="3057" class="Symbol"
-      >&#8704;{</a
-      ><a name="3059" href="Category.html#3059" class="Bound"
-      >&#8467;</a
-      ><a name="3060" class="Symbol"
-      >}</a
-      ><a name="3061"
-      > </a
-      ><a name="3062" class="Symbol"
-      >&#8594;</a
-      ><a name="3063"
-      >  </a
-      ><a name="3065" href="Category.html#2084" class="Function"
-      >Involutive</a
-      ><a name="3075"
-      > </a
-      ><a name="3076" class="Symbol"
-      >(</a
-      ><a name="3077" href="Category.html#2321" class="Function"
-      >Opposite</a
-      ><a name="3085"
-      > </a
-      ><a name="3086" class="Symbol"
-      >{</a
-      ><a name="3087" href="Category.html#3059" class="Bound"
-      >&#8467;</a
-      ><a name="3088" class="Symbol"
-      >})</a
+      ><a name="2672" class="Comment"
+      >--    op hom : Lang cat &#8594; Lang cat</a
+      ><a name="2706"
+      >
+</a
+      ><a name="2707" class="Comment"
+      >--    point : (c : Lang cat) &#8594; Lang (morph empty c)</a
+      ><a name="2758"
+      >
+</a
+      ><a name="2759" 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
+      ><a name="2875" 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
+      ><a name="2982" 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
-      ><a name="3091" href="Category.html#3035" class="Function"
-      >opposite-involutive</a
-      ><a name="3110"
-      > </a
-      ><a name="3111" href="Category.html#3111" class="Bound"
-      >c</a
-      ><a name="3112"
-      > </a
-      ><a name="3113" class="Symbol"
-      >=</a
-      ><a name="3114"
-      >  </a
-      ><a name="3116" href="PropositionalEquivalence.html#97" class="InductiveConstructor"
-      >&#8801;-refl</a
+      ><a name="3091" 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
+      ><a name="3193" 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
+      ><a name="3282" class="Comment"
+      >--  -}     </a
+      ><a name="3293"
+      >
+
+
+</a
+      ><a name="3296" 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
+      ><a name="3398" 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
+      ><a name="3495" 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
+      ><a name="3587" 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
+      ><a name="3676" 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
+      ><a name="3725" class="Comment"
+      >-- -- Operation : {&#8467; : _ } (A : Set &#8467;) &#8594; Set &#8467;</a
+      ><a name="3771"
+      >
+</a
+      ><a name="3772" class="Comment"
+      >-- -- Operation A = A &#8594; A</a
+      ><a name="3797"
+      >
+
+</a
+      ><a name="3799" class="Comment"
+      >-- -- open import PropositionalEquivalence</a
+      ><a name="3841"
+      >
+</a
+      ><a name="3842" class="Comment"
+      >-- -- Involutive : {&#8467; : _} {A : Set &#8467;} &#8594; Operation A &#8594; Set &#8467;</a
+      ><a name="3902"
+      >
+</a
+      ><a name="3903" class="Comment"
+      >-- -- Involutive op = &#8704; a &#8594; op (op a) &#8801; a</a
+      ><a name="3944"
+      >
+
+</a
+      ><a name="3946" 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
+      ><a name="4027" class="Comment"
+      >-- -- flip f b a = f a b</a
+      ><a name="4051"
+      >
+
+</a
+      ><a name="4053" 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
+      ><a name="4109" class="Comment"
+      >-- -- Opposite : &#8704; {&#8467;} &#8594; Operation (Category &#8467;)</a
+      ><a name="4156"
+      >
+</a
+      ><a name="4157" class="Comment"
+      >-- -- Opposite c = record</a
+      ><a name="4182"
+      >
+</a
+      ><a name="4183" 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
+      ><a name="4270" 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
+      ><a name="4357" 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
+      ><a name="4437" class="Comment"
+      >-- --                ; id =  id</a
+      ><a name="4468"
+      >
+</a
+      ><a name="4469" class="Comment"
+      >-- --                ; _&#8728;_ = flip _&#8728;_</a
+      ><a name="4506"
+      >
+</a
+      ><a name="4507" class="Comment"
+      >-- --                ; &#8776;-equivalence = &#8776;-equivalence</a
+      ><a name="4559"
+      >
+</a
+      ><a name="4560" class="Comment"
+      >-- --                ; &#8728;-resp-&#8776; =  flip &#8728;-resp-&#8776;</a
+      ><a name="4608"
+      >
+</a
+      ><a name="4609" class="Comment"
+      >-- --                ; identity&#737; = identity&#691;</a
+      ><a name="4653"
+      >
+</a
+      ><a name="4654" class="Comment"
+      >-- --                ; identity&#691; = identity&#737;</a
+      ><a name="4698"
+      >
+</a
+      ><a name="4699" class="Comment"
+      >-- --                ; &#8728;-assoc = &#955; f&#8321; f&#8322; f&#8323; &#8594; sym (&#8728;-assoc _ _ _)</a
+      ><a name="4764"
+      >
+</a
+      ><a name="4765" class="Comment"
+      >-- --                }</a
+      ><a name="4787"
+      >
+</a
+      ><a name="4788" class="Comment"
+      >-- --          where</a
+      ><a name="4808"
+      >
+</a
+      ><a name="4809" class="Comment"
+      >-- --            open Category c</a
+      ><a name="4841"
+      >
+</a
+      ><a name="4842" class="Comment"
+      >-- --            open IsEquivalence {{...}}</a
+      ><a name="4885"
+      >
+
+
+</a
+      ><a name="4888" class="Comment"
+      >-- -- {- &#1069;&#1090;&#1072; &#1086;&#1087;&#1077;&#1088;&#1072;&#1094;&#1080;&#1103; &#1080;&#1085;&#1074;&#1086;&#1083;&#1102;&#1090;&#1080;&#1074;&#1085;&#1072; -}</a
+      ><a name="4924"
+      >
+</a
+      ><a name="4925" class="Comment"
+      >-- -- opposite-involutive : &#8704;{&#8467;} &#8594;  Involutive (Opposite {&#8467;})</a
+      ><a name="4986"
+      >
+</a
+      ><a name="4987" class="Comment"
+      >-- -- opposite-involutive c =  &#8801;-refl</a
       ></pre
     ></body
   ></html

File html/Equivalence.html

       >
 
 </a
-      ><a name="49" class="Keyword"
+      ><a name="49" class="Comment"
+      >{- &#1042; &#1101;&#1090;&#1086;&#1084; &#1084;&#1086;&#1076;&#1091;&#1083;&#1077; &#1084;&#1099; &#1089;&#1086;&#1073;&#1080;&#1088;&#1072;&#1077;&#1084; &#1089;&#1074;&#1086;&#1081;&#1089;&#1090;&#1074;&#1072; &#1086;&#1090;&#1085;&#1086;&#1096;&#1077;&#1085;&#1080;&#1081; &#1074; &#1086;&#1076;&#1085;&#1091; &#1087;&#1072;&#1095;&#1082;&#1091;, &#1095;&#1090;&#1086;&#1073;&#1099; &#1087;&#1086;&#1083;&#1091;&#1095;&#1080;&#1090;&#1100; &#1090;&#1088;&#1077;&#1073;&#1086;&#1074;&#1072;&#1085;&#1080;&#1103; &#1082; &#1086;&#1090;&#1085;&#1086;&#1096;&#1077;&#1085;&#1080;&#1102; &#1101;&#1082;&#1074;&#1080;&#1074;&#1072;&#1083;&#1077;&#1085;&#1090;&#1085;&#1086;&#1089;&#1090;&#1080; -}</a
+      ><a name="167"
+      >
+</a
+      ><a name="168" class="Comment"
+      >{- &#1054;&#1090;&#1085;&#1086;&#1096;&#1077;&#1085;&#1080;&#1077; &#1101;&#1082;&#1074;&#1080;&#1074;&#1072;&#1083;&#1077;&#1085;&#1090;&#1085;&#1086;&#1089;&#1090;&#1080; &#1101;&#1090;&#1086; &#1090;&#1072;&#1082;&#1086;&#1077; &#1073;&#1080;&#1085;&#1072;&#1088;&#1085;&#1086;&#1077; &#1086;&#1090;&#1085;&#1086;&#1096;&#1077;&#1085;&#1080;&#1077;, &#1082;&#1086;&#1090;&#1086;&#1088;&#1086;&#1077; &#1103;&#1074;&#1083;&#1103;&#1077;&#1090;&#1089;&#1103; &#1088;&#1077;&#1092;&#1083;&#1077;&#1082;&#1089;&#1080;&#1074;&#1085;&#1099;&#1084;, &#1090;&#1088;&#1072;&#1085;&#1079;&#1080;&#1090;&#1080;&#1074;&#1085;&#1099;&#1084; &#1080; &#1089;&#1080;&#1084;&#1084;&#1077;&#1090;&#1088;&#1080;&#1095;&#1085;&#1099;&#1084; -}</a
+      ><a name="288"
+      >
+
+</a
+      ><a name="290" class="Keyword"
       >record</a
-      ><a name="55"
+      ><a name="296"
       > </a
-      ><a name="56" href="Equivalence.html#56" class="Record"
+      ><a name="297" href="Equivalence.html#297" class="Record"
       >IsEquivalence</a
-      ><a name="69"
+      ><a name="310"
       > </a
-      ><a name="70" class="Symbol"
+      ><a name="311" class="Symbol"
       >{</a
-      ><a name="71" href="Equivalence.html#71" class="Bound"
+      ><a name="312" href="Equivalence.html#312" class="Bound"
       >&#8467;</a
-      ><a name="72"
+      ><a name="313"
       > </a
-      ><a name="73" class="Symbol"
+      ><a name="314" class="Symbol"
       >:</a
-      ><a name="74"
+      ><a name="315"
       > </a
-      ><a name="75" class="Symbol"
+      ><a name="316" class="Symbol"
       >_}</a
-      ><a name="77"
+      ><a name="318"
       > </a
-      ><a name="78" class="Symbol"
+      ><a name="319" class="Symbol"
       >{</a
-      ><a name="79" href="Equivalence.html#79" class="Bound"
+      ><a name="320" href="Equivalence.html#320" class="Bound"
       >A</a
-      ><a name="80"
+      ><a name="321"
       > </a
-      ><a name="81" class="Symbol"
+      ><a name="322" class="Symbol"
       >:</a
-      ><a name="82"
+      ><a name="323"
       > </a
-      ><a name="83" class="PrimitiveType"
+      ><a name="324" class="PrimitiveType"
       >Set</a
-      ><a name="86"
+      ><a name="327"
       > </a
-      ><a name="87" href="Equivalence.html#71" class="Bound"
+      ><a name="328" href="Equivalence.html#312" class="Bound"
       >&#8467;</a
-      ><a name="88" class="Symbol"
+      ><a name="329" class="Symbol"
       >}</a
-      ><a name="89"
+      ><a name="330"
       > </a
-      ><a name="90" class="Symbol"
+      ><a name="331" class="Symbol"
       >(</a
-      ><a name="91" href="Equivalence.html#91" class="Bound Operator"
+      ><a name="332" href="Equivalence.html#332" class="Bound Operator"
       >_&#8776;_</a
-      ><a name="94"
+      ><a name="335"
       > </a
-      ><a name="95" class="Symbol"
+      ><a name="336" class="Symbol"
       >:</a
-      ><a name="96"
+      ><a name="337"
       > </a
-      ><a name="97" href="Relations.html#841" class="Function"
+      ><a name="338" href="Relations.html#841" class="Function"
       >BinaryRelation</a
-      ><a name="111"
+      ><a name="352"
       > </a
-      ><a name="112" href="Equivalence.html#79" class="Bound"
+      ><a name="353" href="Equivalence.html#320" class="Bound"
       >A</a
-      ><a name="113" class="Symbol"
+      ><a name="354" class="Symbol"
       >)</a
-      ><a name="114"
+      ><a name="355"
       > </a
-      ><a name="115" class="Symbol"
+      ><a name="356" class="Symbol"
       >:</a
-      ><a name="116"
+      ><a name="357"
       > </a
-      ><a name="117" class="PrimitiveType"
+      ><a name="358" class="PrimitiveType"
       >Set</a
-      ><a name="120"
+      ><a name="361"
       > </a
-      ><a name="121" href="Equivalence.html#71" class="Bound"
+      ><a name="362" href="Equivalence.html#312" class="Bound"
       >&#8467;</a
-      ><a name="122"
+      ><a name="363"
       > </a
-      ><a name="123" class="Keyword"
+      ><a name="364" class="Keyword"
       >where</a
-      ><a name="128"
+      ><a name="369"
       >
   </a
-      ><a name="131" class="Keyword"
+      ><a name="372" class="Keyword"
       >open</a
-      ><a name="135"
+      ><a name="376"
       > </a
-      ><a name="136" href="Relations.html#1193" class="Module"
+      ><a name="377" href="Relations.html#1193" class="Module"
       >RelProperties</a
-      ><a name="149"
+      ><a name="390"
       > </a
-      ><a name="150" href="Equivalence.html#91" class="Bound Operator"
+      ><a name="391" href="Equivalence.html#332" class="Bound Operator"
       >_&#8776;_</a
-      ><a name="153"
+      ><a name="394"
       >
   </a
-      ><a name="156" class="Keyword"
+      ><a name="397" class="Keyword"
       >field</a
-      ><a name="161"
+      ><a name="402"
       >
     </a
-      ><a name="166" href="Equivalence.html#166" class="Field"
+      ><a name="407" href="Equivalence.html#407" class="Field"
       >refl</a
-      ><a name="170"
+      ><a name="411"
       > </a
-      ><a name="171" class="Symbol"
+      ><a name="412" class="Symbol"
       >:</a
-      ><a name="172"
+      ><a name="413"
       > </a
-      ><a name="173" href="Relations.html#1260" class="Function"
+      ><a name="414" href="Relations.html#1260" class="Function"
       >Reflexive</a
-      ><a name="182"
+      ><a name="423"
       >