Commits

Pavel Perikov  committed 124ad62

Notion of opposite category

  • Participants
  • Parent commits 196edfd

Comments (0)

Files changed (4)

File Category.agda

     .∘-resp-≈ :  {o₁ o₂ o₃ : _} {f₁ f₁′ : o₂ ⇒ o₃} {f₂ f₂′ : o₁ ⇒ o₂} → f₁ ≈ f₁′ → f₂ ≈ f₂′ → (f₁ ∘ f₂) ≈ (f₁′ ∘ f₂′)
     .identityˡ :  {o₁ o₂ : _}(f : o₁ ⇒ o₂) → (id ∘ f) ≈ f 
     .identityʳ :  {o₁ o₂ : _}(f : o₁ ⇒ o₂) → (f ∘ id) ≈ f 
-    .-assoc : {o₁ o₂ o₃ o₄ : _} (f₁ : o₃ ⇒ o₄) (f₂ : o₂ ⇒ o₃) (f₃ : o₁ ⇒ o₂) → ((f₁ ∘ f₂) ∘ f₃) ≈ (f₁ ∘ (f₂ ∘ f₃))    
+    .-assoc : {o₁ o₂ o₃ o₄ : _} (f₁ : o₃ ⇒ o₄) (f₂ : o₂ ⇒ o₃) (f₃ : o₁ ⇒ o₂) → ((f₁ ∘ f₂) ∘ f₃) ≈ (f₁ ∘ (f₂ ∘ f₃))    
 
 {- С этого момента мы начинаем конструировать мир из категорий. Для начала (в терминах agda) убедимся,
   что существует пустая категория. В ней нет объектов. Как следствие, в ней нет стрелок -}
           ; ∘-resp-≈ = λ {o₁} {o₂} → λ {}
           ; identityˡ = λ {o₁} → λ {}
           ; identityʳ = λ {o₁} → λ {}
-          ; -assoc = λ {o₁} {o₂} {o₃} → λ {}
+          ; -assoc = λ {o₁} {o₂} {o₃} → λ {}
           }
  
 {- В нашем мире категорий появилась первая категория. Она же - первый "объект". Теперь с помощью этого 
    первого объекта мы начнем строить дальше -}     
+
+{- Чудесным свойством категорий (и определяемых с их помощью понятий) является дуальность.
+ - Если взять любую категорию и развернуть все морфизмы, то получим опять категорию. 
+  - Таким образом, можем рассматривать операцию 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 FirstConcepts.agda

   -- после слова where ничего нет. В этом типе нет элементов
 
   {- Нам потребуется важное понятие предикативности. Предикативность - это запрет использовать 
-    в определении квантификаци по типу (множеству), содержащему определяемое понятие. Импредикативность
+    в определении квантификации по типу (множеству), содержащему определяемое понятие. Импредикативность
     (нарушение предикативности) способно приводить к парадоксам. Например: 
     "Самое маленькое натуральное число - это такое натуральное число, которое меньше всех других натуральных чисел" 
     Определяя понятие "самое маленькое натуральное число" мы квантифицируем (используем квантор "для всех", ∀) по

File html/Category.html

       ><a name="756" class="Symbol"
       >.</a
       ><a name="757" href="Category.html#757" class="Field"
-      >&#8776;-assoc</a
+      >&#8728;-assoc</a
       ><a name="764"
       > </a
       ><a name="765" class="Symbol"
       >=</a
       ><a name="1175"
       > </a
-      ><a name="1176" href="FirstConcepts.html#2045" class="Datatype"
+      ><a name="1176" href="FirstConcepts.html#2046" class="Datatype"
       >&#8709;-type</a
       ><a name="1182"
       > </a
       ><a name="1476"
       > </a
       ><a name="1477" class="Field"
-      >&#8776;-assoc</a
+      >&#8728;-assoc</a
       ><a name="1484"
       > </a
       ><a name="1485" class="Symbol"
    &#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="1681" class="Comment"
-      >-- &#817;</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
+      ><a name="1995" class="Symbol"
+      >:</a
+      ><a name="1996"
+      > </a
+      ><a name="1997" class="Symbol"
+      >{</a
+      ><a name="1998" href="Category.html#1998" class="Bound"
+      >&#8467;</a
+      ><a name="1999"
+      > </a
+      ><a name="2000" class="Symbol"
+      >:</a
+      ><a name="2001"
+      > </a
+      ><a name="2002" class="Symbol"
+      >_</a
+      ><a name="2003"
+      > </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
+      ><a name="2047" class="Keyword"
+      >open</a
+      ><a name="2051"
+      > </a
+      ><a name="2052" class="Keyword"
+      >import</a
+      ><a name="2058"
+      > </a
+      ><a name="2059" href="PropositionalEquivalence.html#1" class="Module"
+      >PropositionalEquivalence</a
+      ><a name="2083"
+      >
+</a
+      ><a name="2084" href="Category.html#2084" class="Function"
+      >Involutive</a
+      ><a name="2094"
+      > </a
+      ><a name="2095" class="Symbol"
+      >:</a
+      ><a name="2096"
+      > </a
+      ><a name="2097" class="Symbol"
+      >{</a
+      ><a name="2098" href="Category.html#2098" class="Bound"
+      >&#8467;</a
+      ><a name="2099"
+      > </a
+      ><a name="2100" class="Symbol"
+      >:</a
+      ><a name="2101"
+      > </a
+      ><a name="2102" class="Symbol"
+      >_}</a
+      ><a name="2104"
+      > </a
+      ><a name="2105" class="Symbol"
+      >{</a
+      ><a name="2106" href="Category.html#2106" class="Bound"
+      >A</a
+      ><a name="2107"
+      > </a
+      ><a name="2108" class="Symbol"
+      >:</a
+      ><a name="2109"
+      > </a
+      ><a name="2110" class="PrimitiveType"
+      >Set</a
+      ><a name="2113"
+      > </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="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="2168" href="Category.html#2157" class="Bound"
+      >a</a
+      ><a name="2169" class="Symbol"
+      >)</a
+      ><a name="2170"
+      > </a
+      ><a name="2171" href="PropositionalEquivalence.html#45" class="Datatype Operator"
+      >&#8801;</a
+      ><a name="2172"
+      > </a
+      ><a name="2173" href="Category.html#2157" class="Bound"
+      >a</a
+      ><a name="2174"
+      >
+
+</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
+      ><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
+      ><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
+      ><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
+      ><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
+      ><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="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
       ></pre
     ></body
   ></html

File html/FirstConcepts.html

   </a
       ><a name="545" class="Comment"
       >{- &#1053;&#1072;&#1084; &#1087;&#1086;&#1090;&#1088;&#1077;&#1073;&#1091;&#1077;&#1090;&#1089;&#1103; &#1074;&#1072;&#1078;&#1085;&#1086;&#1077; &#1087;&#1086;&#1085;&#1103;&#1090;&#1080;&#1077; &#1087;&#1088;&#1077;&#1076;&#1080;&#1082;&#1072;&#1090;&#1080;&#1074;&#1085;&#1086;&#1089;&#1090;&#1080;. &#1055;&#1088;&#1077;&#1076;&#1080;&#1082;&#1072;&#1090;&#1080;&#1074;&#1085;&#1086;&#1089;&#1090;&#1100; - &#1101;&#1090;&#1086; &#1079;&#1072;&#1087;&#1088;&#1077;&#1090; &#1080;&#1089;&#1087;&#1086;&#1083;&#1100;&#1079;&#1086;&#1074;&#1072;&#1090;&#1100; 
-    &#1074; &#1086;&#1087;&#1088;&#1077;&#1076;&#1077;&#1083;&#1077;&#1085;&#1080;&#1080; &#1082;&#1074;&#1072;&#1085;&#1090;&#1080;&#1092;&#1080;&#1082;&#1072;&#1094;&#1080; &#1087;&#1086; &#1090;&#1080;&#1087;&#1091; (&#1084;&#1085;&#1086;&#1078;&#1077;&#1089;&#1090;&#1074;&#1091;), &#1089;&#1086;&#1076;&#1077;&#1088;&#1078;&#1072;&#1097;&#1077;&#1084;&#1091; &#1086;&#1087;&#1088;&#1077;&#1076;&#1077;&#1083;&#1103;&#1077;&#1084;&#1086;&#1077; &#1087;&#1086;&#1085;&#1103;&#1090;&#1080;&#1077;. &#1048;&#1084;&#1087;&#1088;&#1077;&#1076;&#1080;&#1082;&#1072;&#1090;&#1080;&#1074;&#1085;&#1086;&#1089;&#1090;&#1100;
+    &#1074; &#1086;&#1087;&#1088;&#1077;&#1076;&#1077;&#1083;&#1077;&#1085;&#1080;&#1080; &#1082;&#1074;&#1072;&#1085;&#1090;&#1080;&#1092;&#1080;&#1082;&#1072;&#1094;&#1080;&#1080; &#1087;&#1086; &#1090;&#1080;&#1087;&#1091; (&#1084;&#1085;&#1086;&#1078;&#1077;&#1089;&#1090;&#1074;&#1091;), &#1089;&#1086;&#1076;&#1077;&#1088;&#1078;&#1072;&#1097;&#1077;&#1084;&#1091; &#1086;&#1087;&#1088;&#1077;&#1076;&#1077;&#1083;&#1103;&#1077;&#1084;&#1086;&#1077; &#1087;&#1086;&#1085;&#1103;&#1090;&#1080;&#1077;. &#1048;&#1084;&#1087;&#1088;&#1077;&#1076;&#1080;&#1082;&#1072;&#1090;&#1080;&#1074;&#1085;&#1086;&#1089;&#1090;&#1100;
     (&#1085;&#1072;&#1088;&#1091;&#1096;&#1077;&#1085;&#1080;&#1077; &#1087;&#1088;&#1077;&#1076;&#1080;&#1082;&#1072;&#1090;&#1080;&#1074;&#1085;&#1086;&#1089;&#1090;&#1080;) &#1089;&#1087;&#1086;&#1089;&#1086;&#1073;&#1085;&#1086; &#1087;&#1088;&#1080;&#1074;&#1086;&#1076;&#1080;&#1090;&#1100; &#1082; &#1087;&#1072;&#1088;&#1072;&#1076;&#1086;&#1082;&#1089;&#1072;&#1084;. &#1053;&#1072;&#1087;&#1088;&#1080;&#1084;&#1077;&#1088;: 
     &quot;&#1057;&#1072;&#1084;&#1086;&#1077; &#1084;&#1072;&#1083;&#1077;&#1085;&#1100;&#1082;&#1086;&#1077; &#1085;&#1072;&#1090;&#1091;&#1088;&#1072;&#1083;&#1100;&#1085;&#1086;&#1077; &#1095;&#1080;&#1089;&#1083;&#1086; - &#1101;&#1090;&#1086; &#1090;&#1072;&#1082;&#1086;&#1077; &#1085;&#1072;&#1090;&#1091;&#1088;&#1072;&#1083;&#1100;&#1085;&#1086;&#1077; &#1095;&#1080;&#1089;&#1083;&#1086;, &#1082;&#1086;&#1090;&#1086;&#1088;&#1086;&#1077; &#1084;&#1077;&#1085;&#1100;&#1096;&#1077; &#1074;&#1089;&#1077;&#1093; &#1076;&#1088;&#1091;&#1075;&#1080;&#1093; &#1085;&#1072;&#1090;&#1091;&#1088;&#1072;&#1083;&#1100;&#1085;&#1099;&#1093; &#1095;&#1080;&#1089;&#1077;&#1083;&quot; 
     &#1054;&#1087;&#1088;&#1077;&#1076;&#1077;&#1083;&#1103;&#1103; &#1087;&#1086;&#1085;&#1103;&#1090;&#1080;&#1077; &quot;&#1089;&#1072;&#1084;&#1086;&#1077; &#1084;&#1072;&#1083;&#1077;&#1085;&#1100;&#1082;&#1086;&#1077; &#1085;&#1072;&#1090;&#1091;&#1088;&#1072;&#1083;&#1100;&#1085;&#1086;&#1077; &#1095;&#1080;&#1089;&#1083;&#1086;&quot; &#1084;&#1099; &#1082;&#1074;&#1072;&#1085;&#1090;&#1080;&#1092;&#1080;&#1094;&#1080;&#1088;&#1091;&#1077;&#1084; (&#1080;&#1089;&#1087;&#1086;&#1083;&#1100;&#1079;&#1091;&#1077;&#1084; &#1082;&#1074;&#1072;&#1085;&#1090;&#1086;&#1088; &quot;&#1076;&#1083;&#1103; &#1074;&#1089;&#1077;&#1093;&quot;, &#8704;) &#1087;&#1086;
     
     &#1069;&#1090;&#1086;, &#1087;&#1086;&#1078;&#1072;&#1083;&#1091;&#1081;, &#1077;&#1076;&#1080;&#1085;&#1089;&#1090;&#1074;&#1077;&#1085;&#1085;&#1072;&#1103; &#1095;&#1072;&#1089;&#1090;&#1100; &#1089;&#1090;&#1072;&#1085;&#1076;&#1072;&#1088;&#1090;&#1085;&#1086;&#1081; &#1073;&#1080;&#1073;&#1083;&#1080;&#1086;&#1090;&#1077;&#1082;&#1080;, &#1082;&#1086;&#1090;&#1086;&#1088;&#1086;&#1081; &#1084;&#1099; &#1074;&#1086;&#1089;&#1087;&#1086;&#1083;&#1100;&#1079;&#1091;&#1077;&#1084;&#1089;&#1103;
     -}</a
-      ><a name="1746"
+      ><a name="1747"
       >
 </a
-      ><a name="1747" class="Keyword"
+      ><a name="1748" class="Keyword"
       >open</a
-      ><a name="1751"
+      ><a name="1752"
       > </a
-      ><a name="1752" class="Keyword"
+      ><a name="1753" class="Keyword"
       >import</a
-      ><a name="1758"
+      ><a name="1759"
       > </a
-      ><a name="1759" href="Level.html#1" class="Module"
+      ><a name="1760" href="Level.html#1" class="Module"
       >Level</a
-      ><a name="1764"
+      ><a name="1765"
       >
   </a
-      ><a name="1767" class="Comment"
+      ><a name="1768" class="Comment"
       >{- &#1057;&#1090;&#1072;&#1085;&#1076;&#1072;&#1088;&#1085;&#1099;&#1081; &#1084;&#1086;&#1076;&#1091;&#1083;&#1100; Level &#1086;&#1087;&#1088;&#1077;&#1076;&#1077;&#1083;&#1103;&#1077;&#1090; &#1090;&#1080;&#1087; Level (&#1090;&#1080;&#1087; &#1091;&#1088;&#1086;&#1074;&#1085;&#1077;&#1081; &#1090;&#1080;&#1087;&#1086;&#1074;), &#1072; &#1090;&#1072;&#1082; &#1078;&#1077; &#1091;&#1088;&#1086;&#1074;&#1085;&#1080; 
      zero - &#1091;&#1088;&#1086;&#1074;&#1077;&#1085;&#1100; Set&#8320; &#1080; &#1082;&#1086;&#1085;&#1089;&#1090;&#1088;&#1091;&#1082;&#1094;&#1080;&#1102; suc (&#1089;&#1083;&#1077;&#1076;&#1091;&#1102;&#1097;&#1080;&#1081;). &#1090;&#1072;&#1082;&#1080;&#1084; &#1086;&#1073;&#1088;&#1072;&#1079;&#1086;&#1084; &#1084;&#1099; &#1084;&#1086;&#1078;&#1077;&#1084; &#1082;&#1086;&#1085;&#1089;&#1090;&#1088;&#1091;&#1080;&#1088;&#1086;&#1074;&#1072;&#1090;&#1100; &#1085;&#1086;&#1074;&#1099;&#1077; &#1091;&#1088;&#1086;&#1074;&#1085;&#1080;.
 
    &#1058;&#1077;&#1087;&#1077;&#1088;&#1100; &#1084;&#1099; &#1089;&#1085;&#1086;&#1074;&#1072; &#1086;&#1087;&#1088;&#1077;&#1076;&#1077;&#1083;&#1080;&#1084; &#1087;&#1091;&#1089;&#1090;&#1086;&#1081; &#1090;&#1080;&#1087;, &#1085;&#1086; &#1091;&#1078;&#1077; &#1076;&#1083;&#1103; &#1074;&#1089;&#1077;&#1093; &#1091;&#1088;&#1086;&#1074;&#1085;&#1077;&#1081; &#1089;&#1088;&#1072;&#1079;&#1091;:
   -}</a
-      ><a name="2038"
+      ><a name="2039"
       >
 
 </a
-      ><a name="2040" class="Keyword"
+      ><a name="2041" class="Keyword"
       >data</a
-      ><a name="2044"
+      ><a name="2045"
       > </a
-      ><a name="2045" href="FirstConcepts.html#2045" class="Datatype"
+      ><a name="2046" href="FirstConcepts.html#2046" class="Datatype"
       >&#8709;</a
-      ><a name="2046"
+      ><a name="2047"
       > </a
-      ><a name="2047" class="Symbol"
+      ><a name="2048" class="Symbol"
       >(</a
-      ><a name="2048" href="FirstConcepts.html#2048" class="Bound"
+      ><a name="2049" href="FirstConcepts.html#2049" class="Bound"
       >&#8467;</a
-      ><a name="2049"
+      ><a name="2050"
       > </a
-      ><a name="2050" class="Symbol"
+      ><a name="2051" class="Symbol"
       >:</a
-      ><a name="2051"
+      ><a name="2052"
       > </a
-      ><a name="2052" href="Agda.Primitive.html#379" class="Postulate"
+      ><a name="2053" href="Agda.Primitive.html#379" class="Postulate"
       >Level</a
-      ><a name="2057" class="Symbol"
+      ><a name="2058" class="Symbol"
       >)</a
-      ><a name="2058"
+      ><a name="2059"
       > </a
-      ><a name="2059" class="Symbol"
+      ><a name="2060" class="Symbol"
       >:</a
-      ><a name="2060"
+      ><a name="2061"
       > </a
-      ><a name="2061" class="PrimitiveType"
+      ><a name="2062" class="PrimitiveType"
       >Set</a
-      ><a name="2064"
+      ><a name="2065"
       > </a
-      ><a name="2065" href="FirstConcepts.html#2048" class="Bound"
+      ><a name="2066" href="FirstConcepts.html#2049" class="Bound"
       >&#8467;</a
-      ><a name="2066"
+      ><a name="2067"
       > </a
-      ><a name="2067" class="Keyword"
+      ><a name="2068" class="Keyword"
       >where</a
-      ><a name="2072"
+      ><a name="2073"
       >
 
 </a
-      ><a name="2074" class="Comment"
+      ><a name="2075" class="Comment"
       >-- &#1058;&#1072;&#1082;&#1080;&#1084; &#1086;&#1073;&#1088;&#1072;&#1079;&#1086;&#1084;, &#1076;&#1083;&#1103; &#1083;&#1102;&#1073;&#1086;&#1075;&#1086; &#1091;&#1088;&#1086;&#1074;&#1085;&#1103; &#8467; &#1080;&#1084;&#1077;&#1077;&#1090;&#1089;&#1103; &#1087;&#1091;&#1089;&#1090;&#1086;&#1081; &#1090;&#1080;&#1087; &#1085;&#1072; &#1101;&#1090;&#1086;&#1084; &#1091;&#1088;&#1086;&#1074;&#1085;&#1077;</a
-      ><a name="2145"
+      ><a name="2146"
       >