agda-stdlib-doc 0.14-1 / usr / share / doc / agda-stdlib-doc / html / Function.Related.html

This file is indexed.

/usr/share/doc/agda-stdlib-doc/html/Function.Related.html is in agda-stdlib-doc 0.14-1.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below. 

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Function.Related</title><link rel="stylesheet" href="Agda.css"></head><body><pre><a id="1" class="Comment">------------------------------------------------------------------------</a>
<a id="74" class="Comment">-- The Agda standard library</a>
<a id="103" class="Comment">--</a>
<a id="106" class="Comment">-- A universe which includes several kinds of &quot;relatedness&quot; for sets,</a>
<a id="176" class="Comment">-- such as equivalences, surjections and bijections</a>
<a id="228" class="Comment">------------------------------------------------------------------------</a>

<a id="302" class="Keyword">module</a> <a id="309" href="Function.Related.html" class="Module">Function.Related</a> <a id="326" class="Keyword">where</a>

<a id="333" class="Keyword">open</a> <a id="338" class="Keyword">import</a> <a id="345" href="Level.html" class="Module">Level</a>
<a id="351" class="Keyword">open</a> <a id="356" class="Keyword">import</a> <a id="363" href="Function.html" class="Module">Function</a>
<a id="372" class="Keyword">open</a> <a id="377" class="Keyword">import</a> <a id="384" href="Function.Equality.html" class="Module">Function.Equality</a> <a id="402" class="Keyword">using</a> <a id="408" class="Symbol">(</a><a id="409" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">_⟨$⟩_</a><a id="414" class="Symbol">)</a>
<a id="416" class="Keyword">open</a> <a id="421" class="Keyword">import</a> <a id="428" href="Function.Equivalence.html" class="Module">Function.Equivalence</a> <a id="449" class="Symbol">as</a> <a id="452" class="Module">Eq</a>      <a id="460" class="Keyword">using</a> <a id="466" class="Symbol">(</a><a id="467" href="Function.Equivalence.html#Equivalence" class="Record">Equivalence</a><a id="478" class="Symbol">)</a>
<a id="480" class="Keyword">open</a> <a id="485" class="Keyword">import</a> <a id="492" href="Function.Injection.html" class="Module">Function.Injection</a>   <a id="513" class="Symbol">as</a> <a id="516" class="Module">Inj</a>     <a id="524" class="Keyword">using</a> <a id="530" class="Symbol">(</a><a id="531" href="Function.Injection.html#Injection" class="Record">Injection</a><a id="540" class="Symbol">;</a> <a id="542" href="Function.Injection.html#_%E2%86%A3_" class="Function Operator">_↣_</a><a id="545" class="Symbol">)</a>
<a id="547" class="Keyword">open</a> <a id="552" class="Keyword">import</a> <a id="559" href="Function.Inverse.html" class="Module">Function.Inverse</a>     <a id="580" class="Symbol">as</a> <a id="583" class="Module">Inv</a>     <a id="591" class="Keyword">using</a> <a id="597" class="Symbol">(</a><a id="598" href="Function.Inverse.html#Inverse" class="Record">Inverse</a><a id="605" class="Symbol">;</a> <a id="607" href="Function.Inverse.html#_%E2%86%94_" class="Function Operator">_↔_</a><a id="610" class="Symbol">)</a>
<a id="612" class="Keyword">open</a> <a id="617" class="Keyword">import</a> <a id="624" href="Function.LeftInverse.html" class="Module">Function.LeftInverse</a> <a id="645" class="Symbol">as</a> <a id="648" class="Module">LeftInv</a> <a id="656" class="Keyword">using</a> <a id="662" class="Symbol">(</a><a id="663" href="Function.LeftInverse.html#LeftInverse" class="Record">LeftInverse</a><a id="674" class="Symbol">)</a>
<a id="676" class="Keyword">open</a> <a id="681" class="Keyword">import</a> <a id="688" href="Function.Surjection.html" class="Module">Function.Surjection</a>  <a id="709" class="Symbol">as</a> <a id="712" class="Module">Surj</a>    <a id="720" class="Keyword">using</a> <a id="726" class="Symbol">(</a><a id="727" href="Function.Surjection.html#Surjection" class="Record">Surjection</a><a id="737" class="Symbol">)</a>
<a id="739" class="Keyword">open</a> <a id="744" class="Keyword">import</a> <a id="751" href="Relation.Binary.html" class="Module">Relation.Binary</a>
<a id="767" class="Keyword">open</a> <a id="772" class="Keyword">import</a> <a id="779" href="Relation.Binary.PropositionalEquality.html" class="Module">Relation.Binary.PropositionalEquality</a> <a id="817" class="Symbol">as</a> <a id="820" class="Module">P</a> <a id="822" class="Keyword">using</a> <a id="828" class="Symbol">(</a><a id="829" href="Agda.Builtin.Equality.html#_%E2%89%A1_" class="Datatype Operator">_≡_</a><a id="832" class="Symbol">)</a>

<a id="835" class="Comment">------------------------------------------------------------------------</a>
<a id="908" class="Comment">-- Wrapper types</a>

<a id="926" class="Comment">-- Synonyms which are used to make _∼[_]_ below &quot;constructor-headed&quot;</a>
<a id="995" class="Comment">-- (which implies that Agda can deduce the universe code from an</a>
<a id="1060" class="Comment">-- expression matching any of the right-hand sides).</a>

<a id="1114" class="Keyword">record</a> <a id="_←_" href="Function.Related.html#_%E2%86%90_" class="Record Operator">_←_</a> <a id="1125" class="Symbol">{</a><a id="1126" href="Function.Related.html#1126" class="Bound">a</a> <a id="1128" href="Function.Related.html#1128" class="Bound">b</a><a id="1129" class="Symbol">}</a> <a id="1131" class="Symbol">(</a><a id="1132" href="Function.Related.html#1132" class="Bound">A</a> <a id="1134" class="Symbol">:</a> <a id="1136" class="PrimitiveType">Set</a> <a id="1140" href="Function.Related.html#1126" class="Bound">a</a><a id="1141" class="Symbol">)</a> <a id="1143" class="Symbol">(</a><a id="1144" href="Function.Related.html#1144" class="Bound">B</a> <a id="1146" class="Symbol">:</a> <a id="1148" class="PrimitiveType">Set</a> <a id="1152" href="Function.Related.html#1128" class="Bound">b</a><a id="1153" class="Symbol">)</a> <a id="1155" class="Symbol">:</a> <a id="1157" class="PrimitiveType">Set</a> <a id="1161" class="Symbol">(</a><a id="1162" href="Function.Related.html#1126" class="Bound">a</a> <a id="1164" href="Agda.Primitive.html#_%E2%8A%94_" class="Primitive Operator">⊔</a> <a id="1166" href="Function.Related.html#1128" class="Bound">b</a><a id="1167" class="Symbol">)</a> <a id="1169" class="Keyword">where</a>
  <a id="1177" class="Keyword">constructor</a> <a id="_←_.lam" href="Function.Related.html#_%E2%86%90_.lam" class="InductiveConstructor">lam</a>
  <a id="1195" class="Keyword">field</a> <a id="_←_.app-←" href="Function.Related.html#_%E2%86%90_.app-%E2%86%90" class="Field">app-←</a> <a id="1207" class="Symbol">:</a> <a id="1209" href="Function.Related.html#1144" class="Bound">B</a> <a id="1211" class="Symbol">→</a> <a id="1213" href="Function.Related.html#1132" class="Bound">A</a>

<a id="1216" class="Keyword">open</a> <a id="1221" href="Function.Related.html#_%E2%86%90_" class="Module Operator">_←_</a> <a id="1225" class="Keyword">public</a>

<a id="1233" class="Keyword">record</a> <a id="_↢_" href="Function.Related.html#_%E2%86%A2_" class="Record Operator">_↢_</a> <a id="1244" class="Symbol">{</a><a id="1245" href="Function.Related.html#1245" class="Bound">a</a> <a id="1247" href="Function.Related.html#1247" class="Bound">b</a><a id="1248" class="Symbol">}</a> <a id="1250" class="Symbol">(</a><a id="1251" href="Function.Related.html#1251" class="Bound">A</a> <a id="1253" class="Symbol">:</a> <a id="1255" class="PrimitiveType">Set</a> <a id="1259" href="Function.Related.html#1245" class="Bound">a</a><a id="1260" class="Symbol">)</a> <a id="1262" class="Symbol">(</a><a id="1263" href="Function.Related.html#1263" class="Bound">B</a> <a id="1265" class="Symbol">:</a> <a id="1267" class="PrimitiveType">Set</a> <a id="1271" href="Function.Related.html#1247" class="Bound">b</a><a id="1272" class="Symbol">)</a> <a id="1274" class="Symbol">:</a> <a id="1276" class="PrimitiveType">Set</a> <a id="1280" class="Symbol">(</a><a id="1281" href="Function.Related.html#1245" class="Bound">a</a> <a id="1283" href="Agda.Primitive.html#_%E2%8A%94_" class="Primitive Operator">⊔</a> <a id="1285" href="Function.Related.html#1247" class="Bound">b</a><a id="1286" class="Symbol">)</a> <a id="1288" class="Keyword">where</a>
  <a id="1296" class="Keyword">constructor</a> <a id="_↢_.lam" href="Function.Related.html#_%E2%86%A2_.lam" class="InductiveConstructor">lam</a>
  <a id="1314" class="Keyword">field</a> <a id="_↢_.app-↢" href="Function.Related.html#_%E2%86%A2_.app-%E2%86%A2" class="Field">app-↢</a> <a id="1326" class="Symbol">:</a> <a id="1328" href="Function.Related.html#1263" class="Bound">B</a> <a id="1330" href="Function.Injection.html#_%E2%86%A3_" class="Function Operator">↣</a> <a id="1332" href="Function.Related.html#1251" class="Bound">A</a>

<a id="1335" class="Keyword">open</a> <a id="1340" href="Function.Related.html#_%E2%86%A2_" class="Module Operator">_↢_</a> <a id="1344" class="Keyword">public</a>

<a id="1352" class="Comment">------------------------------------------------------------------------</a>
<a id="1425" class="Comment">-- Relatedness</a>

<a id="1441" class="Comment">-- There are several kinds of &quot;relatedness&quot;.</a>

<a id="1487" class="Comment">-- The idea to include kinds other than equivalence and bijection came</a>
<a id="1558" class="Comment">-- from Simon Thompson and Bengt Nordström. /NAD</a>

<a id="1608" class="Keyword">data</a> <a id="Kind" href="Function.Related.html#Kind" class="Datatype">Kind</a> <a id="1618" class="Symbol">:</a> <a id="1620" class="PrimitiveType">Set</a> <a id="1624" class="Keyword">where</a>
  <a id="Kind.implication" href="Function.Related.html#Kind.implication" class="InductiveConstructor">implication</a> <a id="Kind.reverse-implication" href="Function.Related.html#Kind.reverse-implication" class="InductiveConstructor">reverse-implication</a>
    <a id="Kind.equivalence" href="Function.Related.html#Kind.equivalence" class="InductiveConstructor">equivalence</a>
    <a id="Kind.injection" href="Function.Related.html#Kind.injection" class="InductiveConstructor">injection</a> <a id="Kind.reverse-injection" href="Function.Related.html#Kind.reverse-injection" class="InductiveConstructor">reverse-injection</a>
    <a id="Kind.left-inverse" href="Function.Related.html#Kind.left-inverse" class="InductiveConstructor">left-inverse</a> <a id="Kind.surjection" href="Function.Related.html#Kind.surjection" class="InductiveConstructor">surjection</a>
    <a id="Kind.bijection" href="Function.Related.html#Kind.bijection" class="InductiveConstructor">bijection</a>
    <a id="1758" class="Symbol">:</a> <a id="1760" href="Function.Related.html#Kind" class="Datatype">Kind</a>

<a id="1766" class="Comment">-- Interpretation of the codes above. The code &quot;bijection&quot; is</a>
<a id="1828" class="Comment">-- interpreted as Inverse rather than Bijection; the two types are</a>
<a id="1895" class="Comment">-- equivalent.</a>

<a id="1911" class="Keyword">infix</a> <a id="1917" class="Number">4</a> <a id="1919" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">_∼[_]_</a>

<a id="_∼[_]_" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">_∼[_]_</a> <a id="1934" class="Symbol">:</a> <a id="1936" class="Symbol">∀</a> <a id="1938" class="Symbol">{</a><a id="1939" href="Function.Related.html#1939" class="Bound">ℓ₁</a> <a id="1942" href="Function.Related.html#1942" class="Bound">ℓ₂</a><a id="1944" class="Symbol">}</a> <a id="1946" class="Symbol">→</a> <a id="1948" class="PrimitiveType">Set</a> <a id="1952" href="Function.Related.html#1939" class="Bound">ℓ₁</a> <a id="1955" class="Symbol">→</a> <a id="1957" href="Function.Related.html#Kind" class="Datatype">Kind</a> <a id="1962" class="Symbol">→</a> <a id="1964" class="PrimitiveType">Set</a> <a id="1968" href="Function.Related.html#1942" class="Bound">ℓ₂</a> <a id="1971" class="Symbol">→</a> <a id="1973" class="PrimitiveType">Set</a> <a id="1977" class="Symbol">_</a>
<a id="1979" href="Function.Related.html#1979" class="Bound">A</a> <a id="1981" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="1984" href="Function.Related.html#Kind.implication" class="InductiveConstructor">implication</a>         <a id="2004" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="2006" href="Function.Related.html#2006" class="Bound">B</a> <a id="2008" class="Symbol">=</a> <a id="2010" href="Function.Related.html#1979" class="Bound">A</a> <a id="2012" class="Symbol">→</a> <a id="2014" href="Function.Related.html#2006" class="Bound">B</a>
<a id="2016" href="Function.Related.html#2016" class="Bound">A</a> <a id="2018" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="2021" href="Function.Related.html#Kind.reverse-implication" class="InductiveConstructor">reverse-implication</a> <a id="2041" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="2043" href="Function.Related.html#2043" class="Bound">B</a> <a id="2045" class="Symbol">=</a> <a id="2047" href="Function.Related.html#2016" class="Bound">A</a> <a id="2049" href="Function.Related.html#_%E2%86%90_" class="Record Operator">←</a> <a id="2051" href="Function.Related.html#2043" class="Bound">B</a>
<a id="2053" href="Function.Related.html#2053" class="Bound">A</a> <a id="2055" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="2058" href="Function.Related.html#Kind.equivalence" class="InductiveConstructor">equivalence</a>         <a id="2078" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="2080" href="Function.Related.html#2080" class="Bound">B</a> <a id="2082" class="Symbol">=</a> <a id="2084" href="Function.Equivalence.html#Equivalence" class="Record">Equivalence</a> <a id="2096" class="Symbol">(</a><a id="2097" href="Relation.Binary.PropositionalEquality.html#setoid" class="Function">P.setoid</a> <a id="2106" href="Function.Related.html#2053" class="Bound">A</a><a id="2107" class="Symbol">)</a> <a id="2109" class="Symbol">(</a><a id="2110" href="Relation.Binary.PropositionalEquality.html#setoid" class="Function">P.setoid</a> <a id="2119" href="Function.Related.html#2080" class="Bound">B</a><a id="2120" class="Symbol">)</a>
<a id="2122" href="Function.Related.html#2122" class="Bound">A</a> <a id="2124" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="2127" href="Function.Related.html#Kind.injection" class="InductiveConstructor">injection</a>           <a id="2147" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="2149" href="Function.Related.html#2149" class="Bound">B</a> <a id="2151" class="Symbol">=</a> <a id="2153" href="Function.Injection.html#Injection" class="Record">Injection</a>   <a id="2165" class="Symbol">(</a><a id="2166" href="Relation.Binary.PropositionalEquality.html#setoid" class="Function">P.setoid</a> <a id="2175" href="Function.Related.html#2122" class="Bound">A</a><a id="2176" class="Symbol">)</a> <a id="2178" class="Symbol">(</a><a id="2179" href="Relation.Binary.PropositionalEquality.html#setoid" class="Function">P.setoid</a> <a id="2188" href="Function.Related.html#2149" class="Bound">B</a><a id="2189" class="Symbol">)</a>
<a id="2191" href="Function.Related.html#2191" class="Bound">A</a> <a id="2193" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="2196" href="Function.Related.html#Kind.reverse-injection" class="InductiveConstructor">reverse-injection</a>   <a id="2216" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="2218" href="Function.Related.html#2218" class="Bound">B</a> <a id="2220" class="Symbol">=</a> <a id="2222" href="Function.Related.html#2191" class="Bound">A</a> <a id="2224" href="Function.Related.html#_%E2%86%A2_" class="Record Operator">↢</a> <a id="2226" href="Function.Related.html#2218" class="Bound">B</a>
<a id="2228" href="Function.Related.html#2228" class="Bound">A</a> <a id="2230" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="2233" href="Function.Related.html#Kind.left-inverse" class="InductiveConstructor">left-inverse</a>        <a id="2253" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="2255" href="Function.Related.html#2255" class="Bound">B</a> <a id="2257" class="Symbol">=</a> <a id="2259" href="Function.LeftInverse.html#LeftInverse" class="Record">LeftInverse</a> <a id="2271" class="Symbol">(</a><a id="2272" href="Relation.Binary.PropositionalEquality.html#setoid" class="Function">P.setoid</a> <a id="2281" href="Function.Related.html#2228" class="Bound">A</a><a id="2282" class="Symbol">)</a> <a id="2284" class="Symbol">(</a><a id="2285" href="Relation.Binary.PropositionalEquality.html#setoid" class="Function">P.setoid</a> <a id="2294" href="Function.Related.html#2255" class="Bound">B</a><a id="2295" class="Symbol">)</a>
<a id="2297" href="Function.Related.html#2297" class="Bound">A</a> <a id="2299" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="2302" href="Function.Related.html#Kind.surjection" class="InductiveConstructor">surjection</a>          <a id="2322" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="2324" href="Function.Related.html#2324" class="Bound">B</a> <a id="2326" class="Symbol">=</a> <a id="2328" href="Function.Surjection.html#Surjection" class="Record">Surjection</a>  <a id="2340" class="Symbol">(</a><a id="2341" href="Relation.Binary.PropositionalEquality.html#setoid" class="Function">P.setoid</a> <a id="2350" href="Function.Related.html#2297" class="Bound">A</a><a id="2351" class="Symbol">)</a> <a id="2353" class="Symbol">(</a><a id="2354" href="Relation.Binary.PropositionalEquality.html#setoid" class="Function">P.setoid</a> <a id="2363" href="Function.Related.html#2324" class="Bound">B</a><a id="2364" class="Symbol">)</a>
<a id="2366" href="Function.Related.html#2366" class="Bound">A</a> <a id="2368" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="2371" href="Function.Related.html#Kind.bijection" class="InductiveConstructor">bijection</a>           <a id="2391" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="2393" href="Function.Related.html#2393" class="Bound">B</a> <a id="2395" class="Symbol">=</a> <a id="2397" href="Function.Inverse.html#Inverse" class="Record">Inverse</a>     <a id="2409" class="Symbol">(</a><a id="2410" href="Relation.Binary.PropositionalEquality.html#setoid" class="Function">P.setoid</a> <a id="2419" href="Function.Related.html#2366" class="Bound">A</a><a id="2420" class="Symbol">)</a> <a id="2422" class="Symbol">(</a><a id="2423" href="Relation.Binary.PropositionalEquality.html#setoid" class="Function">P.setoid</a> <a id="2432" href="Function.Related.html#2393" class="Bound">B</a><a id="2433" class="Symbol">)</a>

<a id="2436" class="Comment">-- A non-infix synonym.</a>

<a id="Related" href="Function.Related.html#Related" class="Function">Related</a> <a id="2469" class="Symbol">:</a> <a id="2471" href="Function.Related.html#Kind" class="Datatype">Kind</a> <a id="2476" class="Symbol">→</a> <a id="2478" class="Symbol">∀</a> <a id="2480" class="Symbol">{</a><a id="2481" href="Function.Related.html#2481" class="Bound">ℓ₁</a> <a id="2484" href="Function.Related.html#2484" class="Bound">ℓ₂</a><a id="2486" class="Symbol">}</a> <a id="2488" class="Symbol">→</a> <a id="2490" class="PrimitiveType">Set</a> <a id="2494" href="Function.Related.html#2481" class="Bound">ℓ₁</a> <a id="2497" class="Symbol">→</a> <a id="2499" class="PrimitiveType">Set</a> <a id="2503" href="Function.Related.html#2484" class="Bound">ℓ₂</a> <a id="2506" class="Symbol">→</a> <a id="2508" class="PrimitiveType">Set</a> <a id="2512" class="Symbol">_</a>
<a id="2514" href="Function.Related.html#Related" class="Function">Related</a> <a id="2522" href="Function.Related.html#2522" class="Bound">k</a> <a id="2524" href="Function.Related.html#2524" class="Bound">A</a> <a id="2526" href="Function.Related.html#2526" class="Bound">B</a> <a id="2528" class="Symbol">=</a> <a id="2530" href="Function.Related.html#2524" class="Bound">A</a> <a id="2532" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="2535" href="Function.Related.html#2522" class="Bound">k</a> <a id="2537" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="2539" href="Function.Related.html#2526" class="Bound">B</a>

<a id="2542" class="Comment">-- The bijective equality implies any kind of relatedness.</a>

<a id="↔⇒" href="Function.Related.html#%E2%86%94%E2%87%92" class="Function">↔⇒</a> <a id="2605" class="Symbol">:</a> <a id="2607" class="Symbol">∀</a> <a id="2609" class="Symbol">{</a><a id="2610" href="Function.Related.html#2610" class="Bound">k</a> <a id="2612" href="Function.Related.html#2612" class="Bound">x</a> <a id="2614" href="Function.Related.html#2614" class="Bound">y</a><a id="2615" class="Symbol">}</a> <a id="2617" class="Symbol">{</a><a id="2618" href="Function.Related.html#2618" class="Bound">X</a> <a id="2620" class="Symbol">:</a> <a id="2622" class="PrimitiveType">Set</a> <a id="2626" href="Function.Related.html#2612" class="Bound">x</a><a id="2627" class="Symbol">}</a> <a id="2629" class="Symbol">{</a><a id="2630" href="Function.Related.html#2630" class="Bound">Y</a> <a id="2632" class="Symbol">:</a> <a id="2634" class="PrimitiveType">Set</a> <a id="2638" href="Function.Related.html#2614" class="Bound">y</a><a id="2639" class="Symbol">}</a> <a id="2641" class="Symbol">→</a>
     <a id="2648" href="Function.Related.html#2618" class="Bound">X</a> <a id="2650" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="2653" href="Function.Related.html#Kind.bijection" class="InductiveConstructor">bijection</a> <a id="2663" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="2665" href="Function.Related.html#2630" class="Bound">Y</a> <a id="2667" class="Symbol">→</a> <a id="2669" href="Function.Related.html#2618" class="Bound">X</a> <a id="2671" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="2674" href="Function.Related.html#2610" class="Bound">k</a> <a id="2676" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="2678" href="Function.Related.html#2630" class="Bound">Y</a>
<a id="2680" href="Function.Related.html#%E2%86%94%E2%87%92" class="Function">↔⇒</a> <a id="2683" class="Symbol">{</a><a id="2684" href="Function.Related.html#Kind.implication" class="InductiveConstructor">implication</a><a id="2695" class="Symbol">}</a>         <a id="2705" class="Symbol">=</a> <a id="2707" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">_⟨$⟩_</a> <a id="2713" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="2715" href="Function.Inverse.html#Inverse.to" class="Field">Inverse.to</a>
<a id="2726" href="Function.Related.html#%E2%86%94%E2%87%92" class="Function">↔⇒</a> <a id="2729" class="Symbol">{</a><a id="2730" href="Function.Related.html#Kind.reverse-implication" class="InductiveConstructor">reverse-implication</a><a id="2749" class="Symbol">}</a> <a id="2751" class="Symbol">=</a> <a id="2753" href="Function.Related.html#_%E2%86%90_.lam" class="InductiveConstructor">lam</a> <a id="2757" href="Function.html#_%E2%88%98%E2%80%B2_" class="Function Operator">∘′</a> <a id="2760" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">_⟨$⟩_</a> <a id="2766" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="2768" href="Function.Inverse.html#Inverse.from" class="Field">Inverse.from</a>
<a id="2781" href="Function.Related.html#%E2%86%94%E2%87%92" class="Function">↔⇒</a> <a id="2784" class="Symbol">{</a><a id="2785" href="Function.Related.html#Kind.equivalence" class="InductiveConstructor">equivalence</a><a id="2796" class="Symbol">}</a>         <a id="2806" class="Symbol">=</a> <a id="2808" href="Function.Surjection.html#1606" class="Function">Inverse.equivalence</a>
<a id="2828" href="Function.Related.html#%E2%86%94%E2%87%92" class="Function">↔⇒</a> <a id="2831" class="Symbol">{</a><a id="2832" href="Function.Related.html#Kind.injection" class="InductiveConstructor">injection</a><a id="2841" class="Symbol">}</a>           <a id="2853" class="Symbol">=</a> <a id="2855" href="Function.LeftInverse.html#1631" class="Function">Inverse.injection</a>
<a id="2873" href="Function.Related.html#%E2%86%94%E2%87%92" class="Function">↔⇒</a> <a id="2876" class="Symbol">{</a><a id="2877" href="Function.Related.html#Kind.reverse-injection" class="InductiveConstructor">reverse-injection</a><a id="2894" class="Symbol">}</a>   <a id="2898" class="Symbol">=</a> <a id="2900" href="Function.Related.html#_%E2%86%A2_.lam" class="InductiveConstructor">lam</a> <a id="2904" href="Function.html#_%E2%88%98%E2%80%B2_" class="Function Operator">∘′</a> <a id="2907" href="Function.LeftInverse.html#1631" class="Function">Inverse.injection</a> <a id="2925" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="2927" href="Function.Inverse.html#sym" class="Function">Inv.sym</a>
<a id="2935" href="Function.Related.html#%E2%86%94%E2%87%92" class="Function">↔⇒</a> <a id="2938" class="Symbol">{</a><a id="2939" href="Function.Related.html#Kind.left-inverse" class="InductiveConstructor">left-inverse</a><a id="2951" class="Symbol">}</a>        <a id="2960" class="Symbol">=</a> <a id="2962" href="Function.Inverse.html#Inverse.left-inverse" class="Function">Inverse.left-inverse</a>
<a id="2983" href="Function.Related.html#%E2%86%94%E2%87%92" class="Function">↔⇒</a> <a id="2986" class="Symbol">{</a><a id="2987" href="Function.Related.html#Kind.surjection" class="InductiveConstructor">surjection</a><a id="2997" class="Symbol">}</a>          <a id="3008" class="Symbol">=</a> <a id="3010" href="Function.Bijection.html#1364" class="Function">Inverse.surjection</a>
<a id="3029" href="Function.Related.html#%E2%86%94%E2%87%92" class="Function">↔⇒</a> <a id="3032" class="Symbol">{</a><a id="3033" href="Function.Related.html#Kind.bijection" class="InductiveConstructor">bijection</a><a id="3042" class="Symbol">}</a>           <a id="3054" class="Symbol">=</a> <a id="3056" href="Function.html#id" class="Function">id</a>

<a id="3060" class="Comment">-- Actual equality also implies any kind of relatedness.</a>

<a id="≡⇒" href="Function.Related.html#%E2%89%A1%E2%87%92" class="Function">≡⇒</a> <a id="3121" class="Symbol">:</a> <a id="3123" class="Symbol">∀</a> <a id="3125" class="Symbol">{</a><a id="3126" href="Function.Related.html#3126" class="Bound">k</a> <a id="3128" href="Function.Related.html#3128" class="Bound">ℓ</a><a id="3129" class="Symbol">}</a> <a id="3131" class="Symbol">{</a><a id="3132" href="Function.Related.html#3132" class="Bound">X</a> <a id="3134" href="Function.Related.html#3134" class="Bound">Y</a> <a id="3136" class="Symbol">:</a> <a id="3138" class="PrimitiveType">Set</a> <a id="3142" href="Function.Related.html#3128" class="Bound">ℓ</a><a id="3143" class="Symbol">}</a> <a id="3145" class="Symbol">→</a> <a id="3147" href="Function.Related.html#3132" class="Bound">X</a> <a id="3149" href="Agda.Builtin.Equality.html#_%E2%89%A1_" class="Datatype Operator">≡</a> <a id="3151" href="Function.Related.html#3134" class="Bound">Y</a> <a id="3153" class="Symbol">→</a> <a id="3155" href="Function.Related.html#3132" class="Bound">X</a> <a id="3157" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="3160" href="Function.Related.html#3126" class="Bound">k</a> <a id="3162" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="3164" href="Function.Related.html#3134" class="Bound">Y</a>
<a id="3166" href="Function.Related.html#%E2%89%A1%E2%87%92" class="Function">≡⇒</a> <a id="3169" href="Agda.Builtin.Equality.html#_%E2%89%A1_.refl" class="InductiveConstructor">P.refl</a> <a id="3176" class="Symbol">=</a> <a id="3178" href="Function.Related.html#%E2%86%94%E2%87%92" class="Function">↔⇒</a> <a id="3181" href="Function.Inverse.html#id" class="Function">Inv.id</a>

<a id="3189" class="Comment">------------------------------------------------------------------------</a>
<a id="3262" class="Comment">-- Special kinds of kinds</a>

<a id="3289" class="Comment">-- Kinds whose interpretation is symmetric.</a>

<a id="3334" class="Keyword">data</a> <a id="Symmetric-kind" href="Function.Related.html#Symmetric-kind" class="Datatype">Symmetric-kind</a> <a id="3354" class="Symbol">:</a> <a id="3356" class="PrimitiveType">Set</a> <a id="3360" class="Keyword">where</a>
  <a id="Symmetric-kind.equivalence" href="Function.Related.html#Symmetric-kind.equivalence" class="InductiveConstructor">equivalence</a> <a id="Symmetric-kind.bijection" href="Function.Related.html#Symmetric-kind.bijection" class="InductiveConstructor">bijection</a> <a id="3390" class="Symbol">:</a> <a id="3392" href="Function.Related.html#Symmetric-kind" class="Datatype">Symmetric-kind</a>

<a id="3408" class="Comment">-- Forgetful map.</a>

<a id="⌊_⌋" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌊_⌋</a> <a id="3431" class="Symbol">:</a> <a id="3433" href="Function.Related.html#Symmetric-kind" class="Datatype">Symmetric-kind</a> <a id="3448" class="Symbol">→</a> <a id="3450" href="Function.Related.html#Kind" class="Datatype">Kind</a>
<a id="3455" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌊</a> <a id="3457" href="Function.Related.html#Symmetric-kind.equivalence" class="InductiveConstructor">equivalence</a> <a id="3469" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌋</a> <a id="3471" class="Symbol">=</a> <a id="3473" href="Function.Related.html#Kind.equivalence" class="InductiveConstructor">equivalence</a>
<a id="3485" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌊</a> <a id="3487" href="Function.Related.html#Symmetric-kind.bijection" class="InductiveConstructor">bijection</a>   <a id="3499" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌋</a> <a id="3501" class="Symbol">=</a> <a id="3503" href="Function.Related.html#Kind.bijection" class="InductiveConstructor">bijection</a>

<a id="3514" class="Comment">-- The proof of symmetry can be found below.</a>

<a id="3560" class="Comment">-- Kinds whose interpretation include a function which &quot;goes in the</a>
<a id="3628" class="Comment">-- forward direction&quot;.</a>

<a id="3652" class="Keyword">data</a> <a id="Forward-kind" href="Function.Related.html#Forward-kind" class="Datatype">Forward-kind</a> <a id="3670" class="Symbol">:</a> <a id="3672" class="PrimitiveType">Set</a> <a id="3676" class="Keyword">where</a>
  <a id="Forward-kind.implication" href="Function.Related.html#Forward-kind.implication" class="InductiveConstructor">implication</a> <a id="Forward-kind.equivalence" href="Function.Related.html#Forward-kind.equivalence" class="InductiveConstructor">equivalence</a> <a id="Forward-kind.injection" href="Function.Related.html#Forward-kind.injection" class="InductiveConstructor">injection</a>
    <a id="Forward-kind.left-inverse" href="Function.Related.html#Forward-kind.left-inverse" class="InductiveConstructor">left-inverse</a> <a id="Forward-kind.surjection" href="Function.Related.html#Forward-kind.surjection" class="InductiveConstructor">surjection</a> <a id="Forward-kind.bijection" href="Function.Related.html#Forward-kind.bijection" class="InductiveConstructor">bijection</a> <a id="3756" class="Symbol">:</a> <a id="3758" href="Function.Related.html#Forward-kind" class="Datatype">Forward-kind</a>

<a id="3772" class="Comment">-- Forgetful map.</a>

<a id="⌊_⌋→" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%92" class="Function Operator">⌊_⌋→</a> <a id="3796" class="Symbol">:</a> <a id="3798" href="Function.Related.html#Forward-kind" class="Datatype">Forward-kind</a> <a id="3811" class="Symbol">→</a> <a id="3813" href="Function.Related.html#Kind" class="Datatype">Kind</a>
<a id="3818" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%92" class="Function Operator">⌊</a> <a id="3820" href="Function.Related.html#Forward-kind.implication" class="InductiveConstructor">implication</a>  <a id="3833" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%92" class="Function Operator">⌋→</a> <a id="3836" class="Symbol">=</a> <a id="3838" href="Function.Related.html#Kind.implication" class="InductiveConstructor">implication</a>
<a id="3850" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%92" class="Function Operator">⌊</a> <a id="3852" href="Function.Related.html#Forward-kind.equivalence" class="InductiveConstructor">equivalence</a>  <a id="3865" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%92" class="Function Operator">⌋→</a> <a id="3868" class="Symbol">=</a> <a id="3870" href="Function.Related.html#Kind.equivalence" class="InductiveConstructor">equivalence</a>
<a id="3882" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%92" class="Function Operator">⌊</a> <a id="3884" href="Function.Related.html#Forward-kind.injection" class="InductiveConstructor">injection</a>    <a id="3897" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%92" class="Function Operator">⌋→</a> <a id="3900" class="Symbol">=</a> <a id="3902" href="Function.Related.html#Kind.injection" class="InductiveConstructor">injection</a>
<a id="3912" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%92" class="Function Operator">⌊</a> <a id="3914" href="Function.Related.html#Forward-kind.left-inverse" class="InductiveConstructor">left-inverse</a> <a id="3927" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%92" class="Function Operator">⌋→</a> <a id="3930" class="Symbol">=</a> <a id="3932" href="Function.Related.html#Kind.left-inverse" class="InductiveConstructor">left-inverse</a>
<a id="3945" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%92" class="Function Operator">⌊</a> <a id="3947" href="Function.Related.html#Forward-kind.surjection" class="InductiveConstructor">surjection</a>   <a id="3960" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%92" class="Function Operator">⌋→</a> <a id="3963" class="Symbol">=</a> <a id="3965" href="Function.Related.html#Kind.surjection" class="InductiveConstructor">surjection</a>
<a id="3976" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%92" class="Function Operator">⌊</a> <a id="3978" href="Function.Related.html#Forward-kind.bijection" class="InductiveConstructor">bijection</a>    <a id="3991" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%92" class="Function Operator">⌋→</a> <a id="3994" class="Symbol">=</a> <a id="3996" href="Function.Related.html#Kind.bijection" class="InductiveConstructor">bijection</a>

<a id="4007" class="Comment">-- The function.</a>

<a id="⇒→" href="Function.Related.html#%E2%87%92%E2%86%92" class="Function">⇒→</a> <a id="4028" class="Symbol">:</a> <a id="4030" class="Symbol">∀</a> <a id="4032" class="Symbol">{</a><a id="4033" href="Function.Related.html#4033" class="Bound">k</a> <a id="4035" href="Function.Related.html#4035" class="Bound">x</a> <a id="4037" href="Function.Related.html#4037" class="Bound">y</a><a id="4038" class="Symbol">}</a> <a id="4040" class="Symbol">{</a><a id="4041" href="Function.Related.html#4041" class="Bound">X</a> <a id="4043" class="Symbol">:</a> <a id="4045" class="PrimitiveType">Set</a> <a id="4049" href="Function.Related.html#4035" class="Bound">x</a><a id="4050" class="Symbol">}</a> <a id="4052" class="Symbol">{</a><a id="4053" href="Function.Related.html#4053" class="Bound">Y</a> <a id="4055" class="Symbol">:</a> <a id="4057" class="PrimitiveType">Set</a> <a id="4061" href="Function.Related.html#4037" class="Bound">y</a><a id="4062" class="Symbol">}</a> <a id="4064" class="Symbol">→</a> <a id="4066" href="Function.Related.html#4041" class="Bound">X</a> <a id="4068" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="4071" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%92" class="Function Operator">⌊</a> <a id="4073" href="Function.Related.html#4033" class="Bound">k</a> <a id="4075" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%92" class="Function Operator">⌋→</a> <a id="4078" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="4080" href="Function.Related.html#4053" class="Bound">Y</a> <a id="4082" class="Symbol">→</a> <a id="4084" href="Function.Related.html#4041" class="Bound">X</a> <a id="4086" class="Symbol">→</a> <a id="4088" href="Function.Related.html#4053" class="Bound">Y</a>
<a id="4090" href="Function.Related.html#%E2%87%92%E2%86%92" class="Function">⇒→</a> <a id="4093" class="Symbol">{</a><a id="4094" href="Function.Related.html#Forward-kind.implication" class="InductiveConstructor">implication</a><a id="4105" class="Symbol">}</a>  <a id="4108" class="Symbol">=</a> <a id="4110" href="Function.html#id" class="Function">id</a>
<a id="4113" href="Function.Related.html#%E2%87%92%E2%86%92" class="Function">⇒→</a> <a id="4116" class="Symbol">{</a><a id="4117" href="Function.Related.html#Forward-kind.equivalence" class="InductiveConstructor">equivalence</a><a id="4128" class="Symbol">}</a>  <a id="4131" class="Symbol">=</a> <a id="4133" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">_⟨$⟩_</a> <a id="4139" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="4141" href="Function.Equivalence.html#Equivalence.to" class="Field">Equivalence.to</a>
<a id="4156" href="Function.Related.html#%E2%87%92%E2%86%92" class="Function">⇒→</a> <a id="4159" class="Symbol">{</a><a id="4160" href="Function.Related.html#Forward-kind.injection" class="InductiveConstructor">injection</a><a id="4169" class="Symbol">}</a>    <a id="4174" class="Symbol">=</a> <a id="4176" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">_⟨$⟩_</a> <a id="4182" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="4184" href="Function.Injection.html#Injection.to" class="Field">Injection.to</a>
<a id="4197" href="Function.Related.html#%E2%87%92%E2%86%92" class="Function">⇒→</a> <a id="4200" class="Symbol">{</a><a id="4201" href="Function.Related.html#Forward-kind.left-inverse" class="InductiveConstructor">left-inverse</a><a id="4213" class="Symbol">}</a> <a id="4215" class="Symbol">=</a> <a id="4217" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">_⟨$⟩_</a> <a id="4223" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="4225" href="Function.LeftInverse.html#LeftInverse.to" class="Field">LeftInverse.to</a>
<a id="4240" href="Function.Related.html#%E2%87%92%E2%86%92" class="Function">⇒→</a> <a id="4243" class="Symbol">{</a><a id="4244" href="Function.Related.html#Forward-kind.surjection" class="InductiveConstructor">surjection</a><a id="4254" class="Symbol">}</a>   <a id="4258" class="Symbol">=</a> <a id="4260" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">_⟨$⟩_</a> <a id="4266" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="4268" href="Function.Surjection.html#Surjection.to" class="Field">Surjection.to</a>
<a id="4282" href="Function.Related.html#%E2%87%92%E2%86%92" class="Function">⇒→</a> <a id="4285" class="Symbol">{</a><a id="4286" href="Function.Related.html#Forward-kind.bijection" class="InductiveConstructor">bijection</a><a id="4295" class="Symbol">}</a>    <a id="4300" class="Symbol">=</a> <a id="4302" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">_⟨$⟩_</a> <a id="4308" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="4310" href="Function.Inverse.html#Inverse.to" class="Field">Inverse.to</a>

<a id="4322" class="Comment">-- Kinds whose interpretation include a function which &quot;goes backwards&quot;.</a>

<a id="4396" class="Keyword">data</a> <a id="Backward-kind" href="Function.Related.html#Backward-kind" class="Datatype">Backward-kind</a> <a id="4415" class="Symbol">:</a> <a id="4417" class="PrimitiveType">Set</a> <a id="4421" class="Keyword">where</a>
  <a id="Backward-kind.reverse-implication" href="Function.Related.html#Backward-kind.reverse-implication" class="InductiveConstructor">reverse-implication</a> <a id="Backward-kind.equivalence" href="Function.Related.html#Backward-kind.equivalence" class="InductiveConstructor">equivalence</a> <a id="Backward-kind.reverse-injection" href="Function.Related.html#Backward-kind.reverse-injection" class="InductiveConstructor">reverse-injection</a>
    <a id="Backward-kind.left-inverse" href="Function.Related.html#Backward-kind.left-inverse" class="InductiveConstructor">left-inverse</a> <a id="Backward-kind.surjection" href="Function.Related.html#Backward-kind.surjection" class="InductiveConstructor">surjection</a> <a id="Backward-kind.bijection" href="Function.Related.html#Backward-kind.bijection" class="InductiveConstructor">bijection</a> <a id="4517" class="Symbol">:</a> <a id="4519" href="Function.Related.html#Backward-kind" class="Datatype">Backward-kind</a>

<a id="4534" class="Comment">-- Forgetful map.</a>

<a id="⌊_⌋←" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%90" class="Function Operator">⌊_⌋←</a> <a id="4558" class="Symbol">:</a> <a id="4560" href="Function.Related.html#Backward-kind" class="Datatype">Backward-kind</a> <a id="4574" class="Symbol">→</a> <a id="4576" href="Function.Related.html#Kind" class="Datatype">Kind</a>
<a id="4581" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%90" class="Function Operator">⌊</a> <a id="4583" href="Function.Related.html#Backward-kind.reverse-implication" class="InductiveConstructor">reverse-implication</a> <a id="4603" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%90" class="Function Operator">⌋←</a> <a id="4606" class="Symbol">=</a> <a id="4608" href="Function.Related.html#Kind.reverse-implication" class="InductiveConstructor">reverse-implication</a>
<a id="4628" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%90" class="Function Operator">⌊</a> <a id="4630" href="Function.Related.html#Backward-kind.equivalence" class="InductiveConstructor">equivalence</a>         <a id="4650" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%90" class="Function Operator">⌋←</a> <a id="4653" class="Symbol">=</a> <a id="4655" href="Function.Related.html#Kind.equivalence" class="InductiveConstructor">equivalence</a>
<a id="4667" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%90" class="Function Operator">⌊</a> <a id="4669" href="Function.Related.html#Backward-kind.reverse-injection" class="InductiveConstructor">reverse-injection</a>   <a id="4689" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%90" class="Function Operator">⌋←</a> <a id="4692" class="Symbol">=</a> <a id="4694" href="Function.Related.html#Kind.reverse-injection" class="InductiveConstructor">reverse-injection</a>
<a id="4712" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%90" class="Function Operator">⌊</a> <a id="4714" href="Function.Related.html#Backward-kind.left-inverse" class="InductiveConstructor">left-inverse</a>        <a id="4734" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%90" class="Function Operator">⌋←</a> <a id="4737" class="Symbol">=</a> <a id="4739" href="Function.Related.html#Kind.left-inverse" class="InductiveConstructor">left-inverse</a>
<a id="4752" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%90" class="Function Operator">⌊</a> <a id="4754" href="Function.Related.html#Backward-kind.surjection" class="InductiveConstructor">surjection</a>          <a id="4774" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%90" class="Function Operator">⌋←</a> <a id="4777" class="Symbol">=</a> <a id="4779" href="Function.Related.html#Kind.surjection" class="InductiveConstructor">surjection</a>
<a id="4790" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%90" class="Function Operator">⌊</a> <a id="4792" href="Function.Related.html#Backward-kind.bijection" class="InductiveConstructor">bijection</a>           <a id="4812" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%90" class="Function Operator">⌋←</a> <a id="4815" class="Symbol">=</a> <a id="4817" href="Function.Related.html#Kind.bijection" class="InductiveConstructor">bijection</a>

<a id="4828" class="Comment">-- The function.</a>

<a id="⇒←" href="Function.Related.html#%E2%87%92%E2%86%90" class="Function">⇒←</a> <a id="4849" class="Symbol">:</a> <a id="4851" class="Symbol">∀</a> <a id="4853" class="Symbol">{</a><a id="4854" href="Function.Related.html#4854" class="Bound">k</a> <a id="4856" href="Function.Related.html#4856" class="Bound">x</a> <a id="4858" href="Function.Related.html#4858" class="Bound">y</a><a id="4859" class="Symbol">}</a> <a id="4861" class="Symbol">{</a><a id="4862" href="Function.Related.html#4862" class="Bound">X</a> <a id="4864" class="Symbol">:</a> <a id="4866" class="PrimitiveType">Set</a> <a id="4870" href="Function.Related.html#4856" class="Bound">x</a><a id="4871" class="Symbol">}</a> <a id="4873" class="Symbol">{</a><a id="4874" href="Function.Related.html#4874" class="Bound">Y</a> <a id="4876" class="Symbol">:</a> <a id="4878" class="PrimitiveType">Set</a> <a id="4882" href="Function.Related.html#4858" class="Bound">y</a><a id="4883" class="Symbol">}</a> <a id="4885" class="Symbol">→</a> <a id="4887" href="Function.Related.html#4862" class="Bound">X</a> <a id="4889" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="4892" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%90" class="Function Operator">⌊</a> <a id="4894" href="Function.Related.html#4854" class="Bound">k</a> <a id="4896" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%86%90" class="Function Operator">⌋←</a> <a id="4899" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="4901" href="Function.Related.html#4874" class="Bound">Y</a> <a id="4903" class="Symbol">→</a> <a id="4905" href="Function.Related.html#4874" class="Bound">Y</a> <a id="4907" class="Symbol">→</a> <a id="4909" href="Function.Related.html#4862" class="Bound">X</a>
<a id="4911" href="Function.Related.html#%E2%87%92%E2%86%90" class="Function">⇒←</a> <a id="4914" class="Symbol">{</a><a id="4915" href="Function.Related.html#Backward-kind.reverse-implication" class="InductiveConstructor">reverse-implication</a><a id="4934" class="Symbol">}</a> <a id="4936" class="Symbol">=</a> <a id="4938" href="Function.Related.html#_%E2%86%90_.app-%E2%86%90" class="Field">app-←</a>
<a id="4944" href="Function.Related.html#%E2%87%92%E2%86%90" class="Function">⇒←</a> <a id="4947" class="Symbol">{</a><a id="4948" href="Function.Related.html#Backward-kind.equivalence" class="InductiveConstructor">equivalence</a><a id="4959" class="Symbol">}</a>         <a id="4969" class="Symbol">=</a> <a id="4971" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">_⟨$⟩_</a> <a id="4977" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="4979" href="Function.Equivalence.html#Equivalence.from" class="Field">Equivalence.from</a>
<a id="4996" href="Function.Related.html#%E2%87%92%E2%86%90" class="Function">⇒←</a> <a id="4999" class="Symbol">{</a><a id="5000" href="Function.Related.html#Backward-kind.reverse-injection" class="InductiveConstructor">reverse-injection</a><a id="5017" class="Symbol">}</a>   <a id="5021" class="Symbol">=</a> <a id="5023" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">_⟨$⟩_</a> <a id="5029" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="5031" href="Function.Injection.html#Injection.to" class="Field">Injection.to</a> <a id="5044" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="5046" href="Function.Related.html#_%E2%86%A2_.app-%E2%86%A2" class="Field">app-↢</a>
<a id="5052" href="Function.Related.html#%E2%87%92%E2%86%90" class="Function">⇒←</a> <a id="5055" class="Symbol">{</a><a id="5056" href="Function.Related.html#Backward-kind.left-inverse" class="InductiveConstructor">left-inverse</a><a id="5068" class="Symbol">}</a>        <a id="5077" class="Symbol">=</a> <a id="5079" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">_⟨$⟩_</a> <a id="5085" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="5087" href="Function.LeftInverse.html#LeftInverse.from" class="Field">LeftInverse.from</a>
<a id="5104" href="Function.Related.html#%E2%87%92%E2%86%90" class="Function">⇒←</a> <a id="5107" class="Symbol">{</a><a id="5108" href="Function.Related.html#Backward-kind.surjection" class="InductiveConstructor">surjection</a><a id="5118" class="Symbol">}</a>          <a id="5129" class="Symbol">=</a> <a id="5131" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">_⟨$⟩_</a> <a id="5137" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="5139" href="Function.Surjection.html#808" class="Function">Surjection.from</a>
<a id="5155" href="Function.Related.html#%E2%87%92%E2%86%90" class="Function">⇒←</a> <a id="5158" class="Symbol">{</a><a id="5159" href="Function.Related.html#Backward-kind.bijection" class="InductiveConstructor">bijection</a><a id="5168" class="Symbol">}</a>           <a id="5180" class="Symbol">=</a> <a id="5182" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">_⟨$⟩_</a> <a id="5188" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="5190" href="Function.Inverse.html#Inverse.from" class="Field">Inverse.from</a>

<a id="5204" class="Comment">-- Kinds whose interpretation include functions going in both</a>
<a id="5266" class="Comment">-- directions.</a>

<a id="5282" class="Keyword">data</a> <a id="Equivalence-kind" href="Function.Related.html#Equivalence-kind" class="Datatype">Equivalence-kind</a> <a id="5304" class="Symbol">:</a> <a id="5306" class="PrimitiveType">Set</a> <a id="5310" class="Keyword">where</a>
    <a id="Equivalence-kind.equivalence" href="Function.Related.html#Equivalence-kind.equivalence" class="InductiveConstructor">equivalence</a> <a id="Equivalence-kind.left-inverse" href="Function.Related.html#Equivalence-kind.left-inverse" class="InductiveConstructor">left-inverse</a> <a id="Equivalence-kind.surjection" href="Function.Related.html#Equivalence-kind.surjection" class="InductiveConstructor">surjection</a> <a id="Equivalence-kind.bijection" href="Function.Related.html#Equivalence-kind.bijection" class="InductiveConstructor">bijection</a> <a id="5366" class="Symbol">:</a> <a id="5368" href="Function.Related.html#Equivalence-kind" class="Datatype">Equivalence-kind</a>

<a id="5386" class="Comment">-- Forgetful map.</a>

<a id="⌊_⌋⇔" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%87%94" class="Function Operator">⌊_⌋⇔</a> <a id="5410" class="Symbol">:</a> <a id="5412" href="Function.Related.html#Equivalence-kind" class="Datatype">Equivalence-kind</a> <a id="5429" class="Symbol">→</a> <a id="5431" href="Function.Related.html#Kind" class="Datatype">Kind</a>
<a id="5436" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%87%94" class="Function Operator">⌊</a> <a id="5438" href="Function.Related.html#Equivalence-kind.equivalence" class="InductiveConstructor">equivalence</a>  <a id="5451" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%87%94" class="Function Operator">⌋⇔</a> <a id="5454" class="Symbol">=</a> <a id="5456" href="Function.Related.html#Kind.equivalence" class="InductiveConstructor">equivalence</a>
<a id="5468" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%87%94" class="Function Operator">⌊</a> <a id="5470" href="Function.Related.html#Equivalence-kind.left-inverse" class="InductiveConstructor">left-inverse</a> <a id="5483" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%87%94" class="Function Operator">⌋⇔</a> <a id="5486" class="Symbol">=</a> <a id="5488" href="Function.Related.html#Kind.left-inverse" class="InductiveConstructor">left-inverse</a>
<a id="5501" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%87%94" class="Function Operator">⌊</a> <a id="5503" href="Function.Related.html#Equivalence-kind.surjection" class="InductiveConstructor">surjection</a>   <a id="5516" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%87%94" class="Function Operator">⌋⇔</a> <a id="5519" class="Symbol">=</a> <a id="5521" href="Function.Related.html#Kind.surjection" class="InductiveConstructor">surjection</a>
<a id="5532" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%87%94" class="Function Operator">⌊</a> <a id="5534" href="Function.Related.html#Equivalence-kind.bijection" class="InductiveConstructor">bijection</a>    <a id="5547" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%87%94" class="Function Operator">⌋⇔</a> <a id="5550" class="Symbol">=</a> <a id="5552" href="Function.Related.html#Kind.bijection" class="InductiveConstructor">bijection</a>

<a id="5563" class="Comment">-- The functions.</a>

<a id="⇒⇔" href="Function.Related.html#%E2%87%92%E2%87%94" class="Function">⇒⇔</a> <a id="5585" class="Symbol">:</a> <a id="5587" class="Symbol">∀</a> <a id="5589" class="Symbol">{</a><a id="5590" href="Function.Related.html#5590" class="Bound">k</a> <a id="5592" href="Function.Related.html#5592" class="Bound">x</a> <a id="5594" href="Function.Related.html#5594" class="Bound">y</a><a id="5595" class="Symbol">}</a> <a id="5597" class="Symbol">{</a><a id="5598" href="Function.Related.html#5598" class="Bound">X</a> <a id="5600" class="Symbol">:</a> <a id="5602" class="PrimitiveType">Set</a> <a id="5606" href="Function.Related.html#5592" class="Bound">x</a><a id="5607" class="Symbol">}</a> <a id="5609" class="Symbol">{</a><a id="5610" href="Function.Related.html#5610" class="Bound">Y</a> <a id="5612" class="Symbol">:</a> <a id="5614" class="PrimitiveType">Set</a> <a id="5618" href="Function.Related.html#5594" class="Bound">y</a><a id="5619" class="Symbol">}</a> <a id="5621" class="Symbol">→</a>
     <a id="5628" href="Function.Related.html#5598" class="Bound">X</a> <a id="5630" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="5633" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%87%94" class="Function Operator">⌊</a> <a id="5635" href="Function.Related.html#5590" class="Bound">k</a> <a id="5637" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B%E2%87%94" class="Function Operator">⌋⇔</a> <a id="5640" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="5642" href="Function.Related.html#5610" class="Bound">Y</a> <a id="5644" class="Symbol">→</a> <a id="5646" href="Function.Related.html#5598" class="Bound">X</a> <a id="5648" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="5651" href="Function.Related.html#Kind.equivalence" class="InductiveConstructor">equivalence</a> <a id="5663" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="5665" href="Function.Related.html#5610" class="Bound">Y</a>
<a id="5667" href="Function.Related.html#%E2%87%92%E2%87%94" class="Function">⇒⇔</a> <a id="5670" class="Symbol">{</a><a id="5671" href="Function.Related.html#Equivalence-kind.equivalence" class="InductiveConstructor">equivalence</a><a id="5682" class="Symbol">}</a>  <a id="5685" class="Symbol">=</a> <a id="5687" href="Function.html#id" class="Function">id</a>
<a id="5690" href="Function.Related.html#%E2%87%92%E2%87%94" class="Function">⇒⇔</a> <a id="5693" class="Symbol">{</a><a id="5694" href="Function.Related.html#Equivalence-kind.left-inverse" class="InductiveConstructor">left-inverse</a><a id="5706" class="Symbol">}</a> <a id="5708" class="Symbol">=</a> <a id="5710" href="Function.LeftInverse.html#LeftInverse.equivalence" class="Function">LeftInverse.equivalence</a>
<a id="5734" href="Function.Related.html#%E2%87%92%E2%87%94" class="Function">⇒⇔</a> <a id="5737" class="Symbol">{</a><a id="5738" href="Function.Related.html#Equivalence-kind.surjection" class="InductiveConstructor">surjection</a><a id="5748" class="Symbol">}</a>   <a id="5752" class="Symbol">=</a> <a id="5754" href="Function.Surjection.html#Surjection.equivalence" class="Function">Surjection.equivalence</a>
<a id="5777" href="Function.Related.html#%E2%87%92%E2%87%94" class="Function">⇒⇔</a> <a id="5780" class="Symbol">{</a><a id="5781" href="Function.Related.html#Equivalence-kind.bijection" class="InductiveConstructor">bijection</a><a id="5790" class="Symbol">}</a>    <a id="5795" class="Symbol">=</a> <a id="5797" href="Function.Surjection.html#1606" class="Function">Inverse.equivalence</a>

<a id="5818" class="Comment">-- Conversions between special kinds.</a>

<a id="⇔⌊_⌋" href="Function.Related.html#%E2%87%94%E2%8C%8A_%E2%8C%8B" class="Function Operator">⇔⌊_⌋</a> <a id="5862" class="Symbol">:</a> <a id="5864" href="Function.Related.html#Symmetric-kind" class="Datatype">Symmetric-kind</a> <a id="5879" class="Symbol">→</a> <a id="5881" href="Function.Related.html#Equivalence-kind" class="Datatype">Equivalence-kind</a>
<a id="5898" href="Function.Related.html#%E2%87%94%E2%8C%8A_%E2%8C%8B" class="Function Operator">⇔⌊</a> <a id="5901" href="Function.Related.html#Symmetric-kind.equivalence" class="InductiveConstructor">equivalence</a> <a id="5913" href="Function.Related.html#%E2%87%94%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌋</a> <a id="5915" class="Symbol">=</a> <a id="5917" href="Function.Related.html#Equivalence-kind.equivalence" class="InductiveConstructor">equivalence</a>
<a id="5929" href="Function.Related.html#%E2%87%94%E2%8C%8A_%E2%8C%8B" class="Function Operator">⇔⌊</a> <a id="5932" href="Function.Related.html#Symmetric-kind.bijection" class="InductiveConstructor">bijection</a>   <a id="5944" href="Function.Related.html#%E2%87%94%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌋</a> <a id="5946" class="Symbol">=</a> <a id="5948" href="Function.Related.html#Equivalence-kind.bijection" class="InductiveConstructor">bijection</a>

<a id="→⌊_⌋" href="Function.Related.html#%E2%86%92%E2%8C%8A_%E2%8C%8B" class="Function Operator">→⌊_⌋</a> <a id="5964" class="Symbol">:</a> <a id="5966" href="Function.Related.html#Equivalence-kind" class="Datatype">Equivalence-kind</a> <a id="5983" class="Symbol">→</a> <a id="5985" href="Function.Related.html#Forward-kind" class="Datatype">Forward-kind</a>
<a id="5998" href="Function.Related.html#%E2%86%92%E2%8C%8A_%E2%8C%8B" class="Function Operator">→⌊</a> <a id="6001" href="Function.Related.html#Equivalence-kind.equivalence" class="InductiveConstructor">equivalence</a>  <a id="6014" href="Function.Related.html#%E2%86%92%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌋</a> <a id="6016" class="Symbol">=</a> <a id="6018" href="Function.Related.html#Forward-kind.equivalence" class="InductiveConstructor">equivalence</a>
<a id="6030" href="Function.Related.html#%E2%86%92%E2%8C%8A_%E2%8C%8B" class="Function Operator">→⌊</a> <a id="6033" href="Function.Related.html#Equivalence-kind.left-inverse" class="InductiveConstructor">left-inverse</a> <a id="6046" href="Function.Related.html#%E2%86%92%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌋</a> <a id="6048" class="Symbol">=</a> <a id="6050" href="Function.Related.html#Forward-kind.left-inverse" class="InductiveConstructor">left-inverse</a>
<a id="6063" href="Function.Related.html#%E2%86%92%E2%8C%8A_%E2%8C%8B" class="Function Operator">→⌊</a> <a id="6066" href="Function.Related.html#Equivalence-kind.surjection" class="InductiveConstructor">surjection</a>   <a id="6079" href="Function.Related.html#%E2%86%92%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌋</a> <a id="6081" class="Symbol">=</a> <a id="6083" href="Function.Related.html#Forward-kind.surjection" class="InductiveConstructor">surjection</a>
<a id="6094" href="Function.Related.html#%E2%86%92%E2%8C%8A_%E2%8C%8B" class="Function Operator">→⌊</a> <a id="6097" href="Function.Related.html#Equivalence-kind.bijection" class="InductiveConstructor">bijection</a>    <a id="6110" href="Function.Related.html#%E2%86%92%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌋</a> <a id="6112" class="Symbol">=</a> <a id="6114" href="Function.Related.html#Forward-kind.bijection" class="InductiveConstructor">bijection</a>

<a id="←⌊_⌋" href="Function.Related.html#%E2%86%90%E2%8C%8A_%E2%8C%8B" class="Function Operator">←⌊_⌋</a> <a id="6130" class="Symbol">:</a> <a id="6132" href="Function.Related.html#Equivalence-kind" class="Datatype">Equivalence-kind</a> <a id="6149" class="Symbol">→</a> <a id="6151" href="Function.Related.html#Backward-kind" class="Datatype">Backward-kind</a>
<a id="6165" href="Function.Related.html#%E2%86%90%E2%8C%8A_%E2%8C%8B" class="Function Operator">←⌊</a> <a id="6168" href="Function.Related.html#Equivalence-kind.equivalence" class="InductiveConstructor">equivalence</a>  <a id="6181" href="Function.Related.html#%E2%86%90%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌋</a> <a id="6183" class="Symbol">=</a> <a id="6185" href="Function.Related.html#Backward-kind.equivalence" class="InductiveConstructor">equivalence</a>
<a id="6197" href="Function.Related.html#%E2%86%90%E2%8C%8A_%E2%8C%8B" class="Function Operator">←⌊</a> <a id="6200" href="Function.Related.html#Equivalence-kind.left-inverse" class="InductiveConstructor">left-inverse</a> <a id="6213" href="Function.Related.html#%E2%86%90%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌋</a> <a id="6215" class="Symbol">=</a> <a id="6217" href="Function.Related.html#Backward-kind.left-inverse" class="InductiveConstructor">left-inverse</a>
<a id="6230" href="Function.Related.html#%E2%86%90%E2%8C%8A_%E2%8C%8B" class="Function Operator">←⌊</a> <a id="6233" href="Function.Related.html#Equivalence-kind.surjection" class="InductiveConstructor">surjection</a>   <a id="6246" href="Function.Related.html#%E2%86%90%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌋</a> <a id="6248" class="Symbol">=</a> <a id="6250" href="Function.Related.html#Backward-kind.surjection" class="InductiveConstructor">surjection</a>
<a id="6261" href="Function.Related.html#%E2%86%90%E2%8C%8A_%E2%8C%8B" class="Function Operator">←⌊</a> <a id="6264" href="Function.Related.html#Equivalence-kind.bijection" class="InductiveConstructor">bijection</a>    <a id="6277" href="Function.Related.html#%E2%86%90%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌋</a> <a id="6279" class="Symbol">=</a> <a id="6281" href="Function.Related.html#Backward-kind.bijection" class="InductiveConstructor">bijection</a>

<a id="6292" class="Comment">------------------------------------------------------------------------</a>
<a id="6365" class="Comment">-- Opposites</a>

<a id="6379" class="Comment">-- For every kind there is an opposite kind.</a>

<a id="_op" href="Function.Related.html#_op" class="Function Operator">_op</a> <a id="6429" class="Symbol">:</a> <a id="6431" href="Function.Related.html#Kind" class="Datatype">Kind</a> <a id="6436" class="Symbol">→</a> <a id="6438" href="Function.Related.html#Kind" class="Datatype">Kind</a>
<a id="6443" href="Function.Related.html#Kind.implication" class="InductiveConstructor">implication</a>         <a id="6463" href="Function.Related.html#_op" class="Function Operator">op</a> <a id="6466" class="Symbol">=</a> <a id="6468" href="Function.Related.html#Kind.reverse-implication" class="InductiveConstructor">reverse-implication</a>
<a id="6488" href="Function.Related.html#Kind.reverse-implication" class="InductiveConstructor">reverse-implication</a> <a id="6508" href="Function.Related.html#_op" class="Function Operator">op</a> <a id="6511" class="Symbol">=</a> <a id="6513" href="Function.Related.html#Kind.implication" class="InductiveConstructor">implication</a>
<a id="6525" href="Function.Related.html#Kind.equivalence" class="InductiveConstructor">equivalence</a>         <a id="6545" href="Function.Related.html#_op" class="Function Operator">op</a> <a id="6548" class="Symbol">=</a> <a id="6550" href="Function.Related.html#Kind.equivalence" class="InductiveConstructor">equivalence</a>
<a id="6562" href="Function.Related.html#Kind.injection" class="InductiveConstructor">injection</a>           <a id="6582" href="Function.Related.html#_op" class="Function Operator">op</a> <a id="6585" class="Symbol">=</a> <a id="6587" href="Function.Related.html#Kind.reverse-injection" class="InductiveConstructor">reverse-injection</a>
<a id="6605" href="Function.Related.html#Kind.reverse-injection" class="InductiveConstructor">reverse-injection</a>   <a id="6625" href="Function.Related.html#_op" class="Function Operator">op</a> <a id="6628" class="Symbol">=</a> <a id="6630" href="Function.Related.html#Kind.injection" class="InductiveConstructor">injection</a>
<a id="6640" href="Function.Related.html#Kind.left-inverse" class="InductiveConstructor">left-inverse</a>        <a id="6660" href="Function.Related.html#_op" class="Function Operator">op</a> <a id="6663" class="Symbol">=</a> <a id="6665" href="Function.Related.html#Kind.surjection" class="InductiveConstructor">surjection</a>
<a id="6676" href="Function.Related.html#Kind.surjection" class="InductiveConstructor">surjection</a>          <a id="6696" href="Function.Related.html#_op" class="Function Operator">op</a> <a id="6699" class="Symbol">=</a> <a id="6701" href="Function.Related.html#Kind.left-inverse" class="InductiveConstructor">left-inverse</a>
<a id="6714" href="Function.Related.html#Kind.bijection" class="InductiveConstructor">bijection</a>           <a id="6734" href="Function.Related.html#_op" class="Function Operator">op</a> <a id="6737" class="Symbol">=</a> <a id="6739" href="Function.Related.html#Kind.bijection" class="InductiveConstructor">bijection</a>

<a id="6750" class="Comment">-- For every morphism there is a corresponding reverse morphism of the</a>
<a id="6821" class="Comment">-- opposite kind.</a>

<a id="reverse" href="Function.Related.html#reverse" class="Function">reverse</a> <a id="6848" class="Symbol">:</a> <a id="6850" class="Symbol">∀</a> <a id="6852" class="Symbol">{</a><a id="6853" href="Function.Related.html#6853" class="Bound">k</a> <a id="6855" href="Function.Related.html#6855" class="Bound">a</a> <a id="6857" href="Function.Related.html#6857" class="Bound">b</a><a id="6858" class="Symbol">}</a> <a id="6860" class="Symbol">{</a><a id="6861" href="Function.Related.html#6861" class="Bound">A</a> <a id="6863" class="Symbol">:</a> <a id="6865" class="PrimitiveType">Set</a> <a id="6869" href="Function.Related.html#6855" class="Bound">a</a><a id="6870" class="Symbol">}</a> <a id="6872" class="Symbol">{</a><a id="6873" href="Function.Related.html#6873" class="Bound">B</a> <a id="6875" class="Symbol">:</a> <a id="6877" class="PrimitiveType">Set</a> <a id="6881" href="Function.Related.html#6857" class="Bound">b</a><a id="6882" class="Symbol">}</a> <a id="6884" class="Symbol">→</a>
          <a id="6896" href="Function.Related.html#6861" class="Bound">A</a> <a id="6898" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="6901" href="Function.Related.html#6853" class="Bound">k</a> <a id="6903" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="6905" href="Function.Related.html#6873" class="Bound">B</a> <a id="6907" class="Symbol">→</a> <a id="6909" href="Function.Related.html#6873" class="Bound">B</a> <a id="6911" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="6914" href="Function.Related.html#6853" class="Bound">k</a> <a id="6916" href="Function.Related.html#_op" class="Function Operator">op</a> <a id="6919" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="6921" href="Function.Related.html#6861" class="Bound">A</a>
<a id="6923" href="Function.Related.html#reverse" class="Function">reverse</a> <a id="6931" class="Symbol">{</a><a id="6932" href="Function.Related.html#Kind.implication" class="InductiveConstructor">implication</a><a id="6943" class="Symbol">}</a>         <a id="6953" class="Symbol">=</a> <a id="6955" href="Function.Related.html#_%E2%86%90_.lam" class="InductiveConstructor">lam</a>
<a id="6959" href="Function.Related.html#reverse" class="Function">reverse</a> <a id="6967" class="Symbol">{</a><a id="6968" href="Function.Related.html#Kind.reverse-implication" class="InductiveConstructor">reverse-implication</a><a id="6987" class="Symbol">}</a> <a id="6989" class="Symbol">=</a> <a id="6991" href="Function.Related.html#_%E2%86%90_.app-%E2%86%90" class="Field">app-←</a>
<a id="6997" href="Function.Related.html#reverse" class="Function">reverse</a> <a id="7005" class="Symbol">{</a><a id="7006" href="Function.Related.html#Kind.equivalence" class="InductiveConstructor">equivalence</a><a id="7017" class="Symbol">}</a>         <a id="7027" class="Symbol">=</a> <a id="7029" href="Function.Equivalence.html#sym" class="Function">Eq.sym</a>
<a id="7036" href="Function.Related.html#reverse" class="Function">reverse</a> <a id="7044" class="Symbol">{</a><a id="7045" href="Function.Related.html#Kind.injection" class="InductiveConstructor">injection</a><a id="7054" class="Symbol">}</a>           <a id="7066" class="Symbol">=</a> <a id="7068" href="Function.Related.html#_%E2%86%A2_.lam" class="InductiveConstructor">lam</a>
<a id="7072" href="Function.Related.html#reverse" class="Function">reverse</a> <a id="7080" class="Symbol">{</a><a id="7081" href="Function.Related.html#Kind.reverse-injection" class="InductiveConstructor">reverse-injection</a><a id="7098" class="Symbol">}</a>   <a id="7102" class="Symbol">=</a> <a id="7104" href="Function.Related.html#_%E2%86%A2_.app-%E2%86%A2" class="Field">app-↢</a>
<a id="7110" href="Function.Related.html#reverse" class="Function">reverse</a> <a id="7118" class="Symbol">{</a><a id="7119" href="Function.Related.html#Kind.left-inverse" class="InductiveConstructor">left-inverse</a><a id="7131" class="Symbol">}</a>        <a id="7140" class="Symbol">=</a> <a id="7142" href="Function.Surjection.html#fromRightInverse" class="Function">Surj.fromRightInverse</a>
<a id="7164" href="Function.Related.html#reverse" class="Function">reverse</a> <a id="7172" class="Symbol">{</a><a id="7173" href="Function.Related.html#Kind.surjection" class="InductiveConstructor">surjection</a><a id="7183" class="Symbol">}</a>          <a id="7194" class="Symbol">=</a> <a id="7196" href="Function.Surjection.html#Surjection.right-inverse" class="Function">Surjection.right-inverse</a>
<a id="7221" href="Function.Related.html#reverse" class="Function">reverse</a> <a id="7229" class="Symbol">{</a><a id="7230" href="Function.Related.html#Kind.bijection" class="InductiveConstructor">bijection</a><a id="7239" class="Symbol">}</a>           <a id="7251" class="Symbol">=</a> <a id="7253" href="Function.Inverse.html#sym" class="Function">Inv.sym</a>

<a id="7262" class="Comment">------------------------------------------------------------------------</a>
<a id="7335" class="Comment">-- Equational reasoning</a>

<a id="7360" class="Comment">-- Equational reasoning for related things.</a>

<a id="7405" class="Keyword">module</a> <a id="EquationalReasoning" href="Function.Related.html#EquationalReasoning" class="Module">EquationalReasoning</a> <a id="7432" class="Keyword">where</a>

  <a id="7441" class="Keyword">private</a>

    <a id="EquationalReasoning.refl" href="Function.Related.html#EquationalReasoning.refl" class="Function">refl</a> <a id="7459" class="Symbol">:</a> <a id="7461" class="Symbol">∀</a> <a id="7463" class="Symbol">{</a><a id="7464" href="Function.Related.html#7464" class="Bound">k</a> <a id="7466" href="Function.Related.html#7466" class="Bound">ℓ</a><a id="7467" class="Symbol">}</a> <a id="7469" class="Symbol">→</a> <a id="7471" href="Relation.Binary.Core.html#Reflexive" class="Function">Reflexive</a> <a id="7481" class="Symbol">(</a><a id="7482" href="Function.Related.html#Related" class="Function">Related</a> <a id="7490" href="Function.Related.html#7464" class="Bound">k</a> <a id="7492" class="Symbol">{</a><a id="7493" href="Function.Related.html#7466" class="Bound">ℓ</a><a id="7494" class="Symbol">})</a>
    <a id="7501" href="Function.Related.html#EquationalReasoning.refl" class="Function">refl</a> <a id="7506" class="Symbol">{</a><a id="7507" href="Function.Related.html#Kind.implication" class="InductiveConstructor">implication</a><a id="7518" class="Symbol">}</a>         <a id="7528" class="Symbol">=</a> <a id="7530" href="Function.html#id" class="Function">id</a>
    <a id="7537" href="Function.Related.html#EquationalReasoning.refl" class="Function">refl</a> <a id="7542" class="Symbol">{</a><a id="7543" href="Function.Related.html#Kind.reverse-implication" class="InductiveConstructor">reverse-implication</a><a id="7562" class="Symbol">}</a> <a id="7564" class="Symbol">=</a> <a id="7566" href="Function.Related.html#_%E2%86%90_.lam" class="InductiveConstructor">lam</a> <a id="7570" href="Function.html#id" class="Function">id</a>
    <a id="7577" href="Function.Related.html#EquationalReasoning.refl" class="Function">refl</a> <a id="7582" class="Symbol">{</a><a id="7583" href="Function.Related.html#Kind.equivalence" class="InductiveConstructor">equivalence</a><a id="7594" class="Symbol">}</a>         <a id="7604" class="Symbol">=</a> <a id="7606" href="Function.Equivalence.html#id" class="Function">Eq.id</a>
    <a id="7616" href="Function.Related.html#EquationalReasoning.refl" class="Function">refl</a> <a id="7621" class="Symbol">{</a><a id="7622" href="Function.Related.html#Kind.injection" class="InductiveConstructor">injection</a><a id="7631" class="Symbol">}</a>           <a id="7643" class="Symbol">=</a> <a id="7645" href="Function.Injection.html#id" class="Function">Inj.id</a>
    <a id="7656" href="Function.Related.html#EquationalReasoning.refl" class="Function">refl</a> <a id="7661" class="Symbol">{</a><a id="7662" href="Function.Related.html#Kind.reverse-injection" class="InductiveConstructor">reverse-injection</a><a id="7679" class="Symbol">}</a>   <a id="7683" class="Symbol">=</a> <a id="7685" href="Function.Related.html#_%E2%86%A2_.lam" class="InductiveConstructor">lam</a> <a id="7689" href="Function.Injection.html#id" class="Function">Inj.id</a>
    <a id="7700" href="Function.Related.html#EquationalReasoning.refl" class="Function">refl</a> <a id="7705" class="Symbol">{</a><a id="7706" href="Function.Related.html#Kind.left-inverse" class="InductiveConstructor">left-inverse</a><a id="7718" class="Symbol">}</a>        <a id="7727" class="Symbol">=</a> <a id="7729" href="Function.LeftInverse.html#id" class="Function">LeftInv.id</a>
    <a id="7744" href="Function.Related.html#EquationalReasoning.refl" class="Function">refl</a> <a id="7749" class="Symbol">{</a><a id="7750" href="Function.Related.html#Kind.surjection" class="InductiveConstructor">surjection</a><a id="7760" class="Symbol">}</a>          <a id="7771" class="Symbol">=</a> <a id="7773" href="Function.Surjection.html#id" class="Function">Surj.id</a>
    <a id="7785" href="Function.Related.html#EquationalReasoning.refl" class="Function">refl</a> <a id="7790" class="Symbol">{</a><a id="7791" href="Function.Related.html#Kind.bijection" class="InductiveConstructor">bijection</a><a id="7800" class="Symbol">}</a>           <a id="7812" class="Symbol">=</a> <a id="7814" href="Function.Inverse.html#id" class="Function">Inv.id</a>

    <a id="EquationalReasoning.trans" href="Function.Related.html#EquationalReasoning.trans" class="Function">trans</a> <a id="7832" class="Symbol">:</a> <a id="7834" class="Symbol">∀</a> <a id="7836" class="Symbol">{</a><a id="7837" href="Function.Related.html#7837" class="Bound">k</a> <a id="7839" href="Function.Related.html#7839" class="Bound">ℓ₁</a> <a id="7842" href="Function.Related.html#7842" class="Bound">ℓ₂</a> <a id="7845" href="Function.Related.html#7845" class="Bound">ℓ₃</a><a id="7847" class="Symbol">}</a> <a id="7849" class="Symbol">→</a>
            <a id="7863" href="Relation.Binary.Core.html#Trans" class="Function">Trans</a> <a id="7869" class="Symbol">(</a><a id="7870" href="Function.Related.html#Related" class="Function">Related</a> <a id="7878" href="Function.Related.html#7837" class="Bound">k</a> <a id="7880" class="Symbol">{</a><a id="7881" href="Function.Related.html#7839" class="Bound">ℓ₁</a><a id="7883" class="Symbol">}</a> <a id="7885" class="Symbol">{</a><a id="7886" href="Function.Related.html#7842" class="Bound">ℓ₂</a><a id="7888" class="Symbol">})</a>
                  <a id="7909" class="Symbol">(</a><a id="7910" href="Function.Related.html#Related" class="Function">Related</a> <a id="7918" href="Function.Related.html#7837" class="Bound">k</a> <a id="7920" class="Symbol">{</a><a id="7921" href="Function.Related.html#7842" class="Bound">ℓ₂</a><a id="7923" class="Symbol">}</a> <a id="7925" class="Symbol">{</a><a id="7926" href="Function.Related.html#7845" class="Bound">ℓ₃</a><a id="7928" class="Symbol">})</a>
                  <a id="7949" class="Symbol">(</a><a id="7950" href="Function.Related.html#Related" class="Function">Related</a> <a id="7958" href="Function.Related.html#7837" class="Bound">k</a> <a id="7960" class="Symbol">{</a><a id="7961" href="Function.Related.html#7839" class="Bound">ℓ₁</a><a id="7963" class="Symbol">}</a> <a id="7965" class="Symbol">{</a><a id="7966" href="Function.Related.html#7845" class="Bound">ℓ₃</a><a id="7968" class="Symbol">})</a>
    <a id="7975" href="Function.Related.html#EquationalReasoning.trans" class="Function">trans</a> <a id="7981" class="Symbol">{</a><a id="7982" href="Function.Related.html#Kind.implication" class="InductiveConstructor">implication</a><a id="7993" class="Symbol">}</a>         <a id="8003" class="Symbol">=</a> <a id="8005" href="Function.html#flip" class="Function">flip</a> <a id="8010" href="Function.html#_%E2%88%98%E2%80%B2_" class="Function Operator">_∘′_</a>
    <a id="8019" href="Function.Related.html#EquationalReasoning.trans" class="Function">trans</a> <a id="8025" class="Symbol">{</a><a id="8026" href="Function.Related.html#Kind.reverse-implication" class="InductiveConstructor">reverse-implication</a><a id="8045" class="Symbol">}</a> <a id="8047" class="Symbol">=</a> <a id="8049" class="Symbol">λ</a> <a id="8051" href="Function.Related.html#8051" class="Bound">f</a> <a id="8053" href="Function.Related.html#8053" class="Bound">g</a> <a id="8055" class="Symbol">→</a> <a id="8057" href="Function.Related.html#_%E2%86%90_.lam" class="InductiveConstructor">lam</a> <a id="8061" class="Symbol">(</a><a id="8062" href="Function.Related.html#_%E2%86%90_.app-%E2%86%90" class="Field">app-←</a> <a id="8068" href="Function.Related.html#8051" class="Bound">f</a> <a id="8070" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="8072" href="Function.Related.html#_%E2%86%90_.app-%E2%86%90" class="Field">app-←</a> <a id="8078" href="Function.Related.html#8053" class="Bound">g</a><a id="8079" class="Symbol">)</a>
    <a id="8085" href="Function.Related.html#EquationalReasoning.trans" class="Function">trans</a> <a id="8091" class="Symbol">{</a><a id="8092" href="Function.Related.html#Kind.equivalence" class="InductiveConstructor">equivalence</a><a id="8103" class="Symbol">}</a>         <a id="8113" class="Symbol">=</a> <a id="8115" href="Function.html#flip" class="Function">flip</a> <a id="8120" href="Function.Equivalence.html#_%E2%88%98_" class="Function Operator">Eq._∘_</a>
    <a id="8131" href="Function.Related.html#EquationalReasoning.trans" class="Function">trans</a> <a id="8137" class="Symbol">{</a><a id="8138" href="Function.Related.html#Kind.injection" class="InductiveConstructor">injection</a><a id="8147" class="Symbol">}</a>           <a id="8159" class="Symbol">=</a> <a id="8161" href="Function.html#flip" class="Function">flip</a> <a id="8166" href="Function.Injection.html#_%E2%88%98_" class="Function Operator">Inj._∘_</a>
    <a id="8178" href="Function.Related.html#EquationalReasoning.trans" class="Function">trans</a> <a id="8184" class="Symbol">{</a><a id="8185" href="Function.Related.html#Kind.reverse-injection" class="InductiveConstructor">reverse-injection</a><a id="8202" class="Symbol">}</a>   <a id="8206" class="Symbol">=</a> <a id="8208" class="Symbol">λ</a> <a id="8210" href="Function.Related.html#8210" class="Bound">f</a> <a id="8212" href="Function.Related.html#8212" class="Bound">g</a> <a id="8214" class="Symbol">→</a> <a id="8216" href="Function.Related.html#_%E2%86%A2_.lam" class="InductiveConstructor">lam</a> <a id="8220" class="Symbol">(</a><a id="8221" href="Function.Injection.html#_%E2%88%98_" class="Function Operator">Inj._∘_</a> <a id="8229" class="Symbol">(</a><a id="8230" href="Function.Related.html#_%E2%86%A2_.app-%E2%86%A2" class="Field">app-↢</a> <a id="8236" href="Function.Related.html#8210" class="Bound">f</a><a id="8237" class="Symbol">)</a> <a id="8239" class="Symbol">(</a><a id="8240" href="Function.Related.html#_%E2%86%A2_.app-%E2%86%A2" class="Field">app-↢</a> <a id="8246" href="Function.Related.html#8212" class="Bound">g</a><a id="8247" class="Symbol">))</a>
    <a id="8254" href="Function.Related.html#EquationalReasoning.trans" class="Function">trans</a> <a id="8260" class="Symbol">{</a><a id="8261" href="Function.Related.html#Kind.left-inverse" class="InductiveConstructor">left-inverse</a><a id="8273" class="Symbol">}</a>        <a id="8282" class="Symbol">=</a> <a id="8284" href="Function.html#flip" class="Function">flip</a> <a id="8289" href="Function.LeftInverse.html#_%E2%88%98_" class="Function Operator">LeftInv._∘_</a>
    <a id="8305" href="Function.Related.html#EquationalReasoning.trans" class="Function">trans</a> <a id="8311" class="Symbol">{</a><a id="8312" href="Function.Related.html#Kind.surjection" class="InductiveConstructor">surjection</a><a id="8322" class="Symbol">}</a>          <a id="8333" class="Symbol">=</a> <a id="8335" href="Function.html#flip" class="Function">flip</a> <a id="8340" href="Function.Surjection.html#_%E2%88%98_" class="Function Operator">Surj._∘_</a>
    <a id="8353" href="Function.Related.html#EquationalReasoning.trans" class="Function">trans</a> <a id="8359" class="Symbol">{</a><a id="8360" href="Function.Related.html#Kind.bijection" class="InductiveConstructor">bijection</a><a id="8369" class="Symbol">}</a>           <a id="8381" class="Symbol">=</a> <a id="8383" href="Function.html#flip" class="Function">flip</a> <a id="8388" href="Function.Inverse.html#_%E2%88%98_" class="Function Operator">Inv._∘_</a>

  <a id="EquationalReasoning.sym" href="Function.Related.html#EquationalReasoning.sym" class="Function">sym</a> <a id="8403" class="Symbol">:</a> <a id="8405" class="Symbol">∀</a> <a id="8407" class="Symbol">{</a><a id="8408" href="Function.Related.html#8408" class="Bound">k</a> <a id="8410" href="Function.Related.html#8410" class="Bound">ℓ₁</a> <a id="8413" href="Function.Related.html#8413" class="Bound">ℓ₂</a><a id="8415" class="Symbol">}</a> <a id="8417" class="Symbol">→</a>
        <a id="8427" href="Relation.Binary.Core.html#Sym" class="Function">Sym</a> <a id="8431" class="Symbol">(</a><a id="8432" href="Function.Related.html#Related" class="Function">Related</a> <a id="8440" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌊</a> <a id="8442" href="Function.Related.html#8408" class="Bound">k</a> <a id="8444" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌋</a> <a id="8446" class="Symbol">{</a><a id="8447" href="Function.Related.html#8410" class="Bound">ℓ₁</a><a id="8449" class="Symbol">}</a> <a id="8451" class="Symbol">{</a><a id="8452" href="Function.Related.html#8413" class="Bound">ℓ₂</a><a id="8454" class="Symbol">})</a>
            <a id="8469" class="Symbol">(</a><a id="8470" href="Function.Related.html#Related" class="Function">Related</a> <a id="8478" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌊</a> <a id="8480" href="Function.Related.html#8408" class="Bound">k</a> <a id="8482" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌋</a> <a id="8484" class="Symbol">{</a><a id="8485" href="Function.Related.html#8413" class="Bound">ℓ₂</a><a id="8487" class="Symbol">}</a> <a id="8489" class="Symbol">{</a><a id="8490" href="Function.Related.html#8410" class="Bound">ℓ₁</a><a id="8492" class="Symbol">})</a>
  <a id="8497" href="Function.Related.html#EquationalReasoning.sym" class="Function">sym</a> <a id="8501" class="Symbol">{</a><a id="8502" href="Function.Related.html#Symmetric-kind.equivalence" class="InductiveConstructor">equivalence</a><a id="8513" class="Symbol">}</a> <a id="8515" class="Symbol">=</a> <a id="8517" href="Function.Equivalence.html#sym" class="Function">Eq.sym</a>
  <a id="8526" href="Function.Related.html#EquationalReasoning.sym" class="Function">sym</a> <a id="8530" class="Symbol">{</a><a id="8531" href="Function.Related.html#Symmetric-kind.bijection" class="InductiveConstructor">bijection</a><a id="8540" class="Symbol">}</a>   <a id="8544" class="Symbol">=</a> <a id="8546" href="Function.Inverse.html#sym" class="Function">Inv.sym</a>

  <a id="8557" class="Keyword">infix</a>  <a id="8564" class="Number">3</a> <a id="8566" href="Function.Related.html#EquationalReasoning._%E2%88%8E" class="Function Operator">_∎</a>
  <a id="8571" class="Keyword">infixr</a> <a id="8578" class="Number">2</a> <a id="8580" href="Function.Related.html#EquationalReasoning._%E2%88%BC%E2%9F%A8_%E2%9F%A9_" class="Function Operator">_∼⟨_⟩_</a> <a id="8587" href="Function.Related.html#EquationalReasoning._%E2%86%94%E2%9F%A8_%E2%9F%A9_" class="Function Operator">_↔⟨_⟩_</a> <a id="8594" href="Function.Related.html#EquationalReasoning._%E2%86%94%E2%9F%A8%E2%9F%A9_" class="Function Operator">_↔⟨⟩_</a> <a id="8600" href="Function.Related.html#EquationalReasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">_≡⟨_⟩_</a>

  <a id="EquationalReasoning._∼⟨_⟩_" href="Function.Related.html#EquationalReasoning._%E2%88%BC%E2%9F%A8_%E2%9F%A9_" class="Function Operator">_∼⟨_⟩_</a> <a id="8617" class="Symbol">:</a> <a id="8619" class="Symbol">∀</a> <a id="8621" class="Symbol">{</a><a id="8622" href="Function.Related.html#8622" class="Bound">k</a> <a id="8624" href="Function.Related.html#8624" class="Bound">x</a> <a id="8626" href="Function.Related.html#8626" class="Bound">y</a> <a id="8628" href="Function.Related.html#8628" class="Bound">z</a><a id="8629" class="Symbol">}</a> <a id="8631" class="Symbol">(</a><a id="8632" href="Function.Related.html#8632" class="Bound">X</a> <a id="8634" class="Symbol">:</a> <a id="8636" class="PrimitiveType">Set</a> <a id="8640" href="Function.Related.html#8624" class="Bound">x</a><a id="8641" class="Symbol">)</a> <a id="8643" class="Symbol">{</a><a id="8644" href="Function.Related.html#8644" class="Bound">Y</a> <a id="8646" class="Symbol">:</a> <a id="8648" class="PrimitiveType">Set</a> <a id="8652" href="Function.Related.html#8626" class="Bound">y</a><a id="8653" class="Symbol">}</a> <a id="8655" class="Symbol">{</a><a id="8656" href="Function.Related.html#8656" class="Bound">Z</a> <a id="8658" class="Symbol">:</a> <a id="8660" class="PrimitiveType">Set</a> <a id="8664" href="Function.Related.html#8628" class="Bound">z</a><a id="8665" class="Symbol">}</a> <a id="8667" class="Symbol">→</a>
           <a id="8680" href="Function.Related.html#8632" class="Bound">X</a> <a id="8682" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="8685" href="Function.Related.html#8622" class="Bound">k</a> <a id="8687" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="8689" href="Function.Related.html#8644" class="Bound">Y</a> <a id="8691" class="Symbol">→</a> <a id="8693" href="Function.Related.html#8644" class="Bound">Y</a> <a id="8695" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="8698" href="Function.Related.html#8622" class="Bound">k</a> <a id="8700" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="8702" href="Function.Related.html#8656" class="Bound">Z</a> <a id="8704" class="Symbol">→</a> <a id="8706" href="Function.Related.html#8632" class="Bound">X</a> <a id="8708" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="8711" href="Function.Related.html#8622" class="Bound">k</a> <a id="8713" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="8715" href="Function.Related.html#8656" class="Bound">Z</a>
  <a id="8719" class="Symbol">_</a> <a id="8721" href="Function.Related.html#EquationalReasoning._%E2%88%BC%E2%9F%A8_%E2%9F%A9_" class="Function Operator">∼⟨</a> <a id="8724" href="Function.Related.html#8724" class="Bound">X↝Y</a> <a id="8728" href="Function.Related.html#EquationalReasoning._%E2%88%BC%E2%9F%A8_%E2%9F%A9_" class="Function Operator">⟩</a> <a id="8730" href="Function.Related.html#8730" class="Bound">Y↝Z</a> <a id="8734" class="Symbol">=</a> <a id="8736" href="Function.Related.html#EquationalReasoning.trans" class="Function">trans</a> <a id="8742" href="Function.Related.html#8724" class="Bound">X↝Y</a> <a id="8746" href="Function.Related.html#8730" class="Bound">Y↝Z</a>

  <a id="8753" class="Comment">-- Isomorphisms can be combined with any other kind of relatedness.</a>

  <a id="EquationalReasoning._↔⟨_⟩_" href="Function.Related.html#EquationalReasoning._%E2%86%94%E2%9F%A8_%E2%9F%A9_" class="Function Operator">_↔⟨_⟩_</a> <a id="8831" class="Symbol">:</a> <a id="8833" class="Symbol">∀</a> <a id="8835" class="Symbol">{</a><a id="8836" href="Function.Related.html#8836" class="Bound">k</a> <a id="8838" href="Function.Related.html#8838" class="Bound">x</a> <a id="8840" href="Function.Related.html#8840" class="Bound">y</a> <a id="8842" href="Function.Related.html#8842" class="Bound">z</a><a id="8843" class="Symbol">}</a> <a id="8845" class="Symbol">(</a><a id="8846" href="Function.Related.html#8846" class="Bound">X</a> <a id="8848" class="Symbol">:</a> <a id="8850" class="PrimitiveType">Set</a> <a id="8854" href="Function.Related.html#8838" class="Bound">x</a><a id="8855" class="Symbol">)</a> <a id="8857" class="Symbol">{</a><a id="8858" href="Function.Related.html#8858" class="Bound">Y</a> <a id="8860" class="Symbol">:</a> <a id="8862" class="PrimitiveType">Set</a> <a id="8866" href="Function.Related.html#8840" class="Bound">y</a><a id="8867" class="Symbol">}</a> <a id="8869" class="Symbol">{</a><a id="8870" href="Function.Related.html#8870" class="Bound">Z</a> <a id="8872" class="Symbol">:</a> <a id="8874" class="PrimitiveType">Set</a> <a id="8878" href="Function.Related.html#8842" class="Bound">z</a><a id="8879" class="Symbol">}</a> <a id="8881" class="Symbol">→</a>
           <a id="8894" href="Function.Related.html#8846" class="Bound">X</a> <a id="8896" href="Function.Inverse.html#_%E2%86%94_" class="Function Operator">↔</a> <a id="8898" href="Function.Related.html#8858" class="Bound">Y</a> <a id="8900" class="Symbol">→</a> <a id="8902" href="Function.Related.html#8858" class="Bound">Y</a> <a id="8904" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="8907" href="Function.Related.html#8836" class="Bound">k</a> <a id="8909" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="8911" href="Function.Related.html#8870" class="Bound">Z</a> <a id="8913" class="Symbol">→</a> <a id="8915" href="Function.Related.html#8846" class="Bound">X</a> <a id="8917" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="8920" href="Function.Related.html#8836" class="Bound">k</a> <a id="8922" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="8924" href="Function.Related.html#8870" class="Bound">Z</a>
  <a id="8928" href="Function.Related.html#8928" class="Bound">X</a> <a id="8930" href="Function.Related.html#EquationalReasoning._%E2%86%94%E2%9F%A8_%E2%9F%A9_" class="Function Operator">↔⟨</a> <a id="8933" href="Function.Related.html#8933" class="Bound">X↔Y</a> <a id="8937" href="Function.Related.html#EquationalReasoning._%E2%86%94%E2%9F%A8_%E2%9F%A9_" class="Function Operator">⟩</a> <a id="8939" href="Function.Related.html#8939" class="Bound">Y⇔Z</a> <a id="8943" class="Symbol">=</a> <a id="8945" href="Function.Related.html#8928" class="Bound">X</a> <a id="8947" href="Function.Related.html#EquationalReasoning._%E2%88%BC%E2%9F%A8_%E2%9F%A9_" class="Function Operator">∼⟨</a> <a id="8950" href="Function.Related.html#%E2%86%94%E2%87%92" class="Function">↔⇒</a> <a id="8953" href="Function.Related.html#8933" class="Bound">X↔Y</a> <a id="8957" href="Function.Related.html#EquationalReasoning._%E2%88%BC%E2%9F%A8_%E2%9F%A9_" class="Function Operator">⟩</a> <a id="8959" href="Function.Related.html#8939" class="Bound">Y⇔Z</a>

  <a id="EquationalReasoning._↔⟨⟩_" href="Function.Related.html#EquationalReasoning._%E2%86%94%E2%9F%A8%E2%9F%A9_" class="Function Operator">_↔⟨⟩_</a> <a id="8972" class="Symbol">:</a> <a id="8974" class="Symbol">∀</a> <a id="8976" class="Symbol">{</a><a id="8977" href="Function.Related.html#8977" class="Bound">k</a> <a id="8979" href="Function.Related.html#8979" class="Bound">x</a> <a id="8981" href="Function.Related.html#8981" class="Bound">y</a><a id="8982" class="Symbol">}</a> <a id="8984" class="Symbol">(</a><a id="8985" href="Function.Related.html#8985" class="Bound">X</a> <a id="8987" class="Symbol">:</a> <a id="8989" class="PrimitiveType">Set</a> <a id="8993" href="Function.Related.html#8979" class="Bound">x</a><a id="8994" class="Symbol">)</a> <a id="8996" class="Symbol">{</a><a id="8997" href="Function.Related.html#8997" class="Bound">Y</a> <a id="8999" class="Symbol">:</a> <a id="9001" class="PrimitiveType">Set</a> <a id="9005" href="Function.Related.html#8981" class="Bound">y</a><a id="9006" class="Symbol">}</a> <a id="9008" class="Symbol">→</a>
          <a id="9020" href="Function.Related.html#8985" class="Bound">X</a> <a id="9022" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="9025" href="Function.Related.html#8977" class="Bound">k</a> <a id="9027" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="9029" href="Function.Related.html#8997" class="Bound">Y</a> <a id="9031" class="Symbol">→</a> <a id="9033" href="Function.Related.html#8985" class="Bound">X</a> <a id="9035" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="9038" href="Function.Related.html#8977" class="Bound">k</a> <a id="9040" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="9042" href="Function.Related.html#8997" class="Bound">Y</a>
  <a id="9046" href="Function.Related.html#9046" class="Bound">X</a> <a id="9048" href="Function.Related.html#EquationalReasoning._%E2%86%94%E2%9F%A8%E2%9F%A9_" class="Function Operator">↔⟨⟩</a> <a id="9052" href="Function.Related.html#9052" class="Bound">X⇔Y</a> <a id="9056" class="Symbol">=</a> <a id="9058" href="Function.Related.html#9052" class="Bound">X⇔Y</a>

  <a id="EquationalReasoning._≡⟨_⟩_" href="Function.Related.html#EquationalReasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">_≡⟨_⟩_</a> <a id="9072" class="Symbol">:</a> <a id="9074" class="Symbol">∀</a> <a id="9076" class="Symbol">{</a><a id="9077" href="Function.Related.html#9077" class="Bound">k</a> <a id="9079" href="Function.Related.html#9079" class="Bound">ℓ</a> <a id="9081" href="Function.Related.html#9081" class="Bound">z</a><a id="9082" class="Symbol">}</a> <a id="9084" class="Symbol">(</a><a id="9085" href="Function.Related.html#9085" class="Bound">X</a> <a id="9087" class="Symbol">:</a> <a id="9089" class="PrimitiveType">Set</a> <a id="9093" href="Function.Related.html#9079" class="Bound">ℓ</a><a id="9094" class="Symbol">)</a> <a id="9096" class="Symbol">{</a><a id="9097" href="Function.Related.html#9097" class="Bound">Y</a> <a id="9099" class="Symbol">:</a> <a id="9101" class="PrimitiveType">Set</a> <a id="9105" href="Function.Related.html#9079" class="Bound">ℓ</a><a id="9106" class="Symbol">}</a> <a id="9108" class="Symbol">{</a><a id="9109" href="Function.Related.html#9109" class="Bound">Z</a> <a id="9111" class="Symbol">:</a> <a id="9113" class="PrimitiveType">Set</a> <a id="9117" href="Function.Related.html#9081" class="Bound">z</a><a id="9118" class="Symbol">}</a> <a id="9120" class="Symbol">→</a>
           <a id="9133" href="Function.Related.html#9085" class="Bound">X</a> <a id="9135" href="Agda.Builtin.Equality.html#_%E2%89%A1_" class="Datatype Operator">≡</a> <a id="9137" href="Function.Related.html#9097" class="Bound">Y</a> <a id="9139" class="Symbol">→</a> <a id="9141" href="Function.Related.html#9097" class="Bound">Y</a> <a id="9143" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="9146" href="Function.Related.html#9077" class="Bound">k</a> <a id="9148" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="9150" href="Function.Related.html#9109" class="Bound">Z</a> <a id="9152" class="Symbol">→</a> <a id="9154" href="Function.Related.html#9085" class="Bound">X</a> <a id="9156" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="9159" href="Function.Related.html#9077" class="Bound">k</a> <a id="9161" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="9163" href="Function.Related.html#9109" class="Bound">Z</a>
  <a id="9167" href="Function.Related.html#9167" class="Bound">X</a> <a id="9169" href="Function.Related.html#EquationalReasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">≡⟨</a> <a id="9172" href="Function.Related.html#9172" class="Bound">X≡Y</a> <a id="9176" href="Function.Related.html#EquationalReasoning._%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">⟩</a> <a id="9178" href="Function.Related.html#9178" class="Bound">Y⇔Z</a> <a id="9182" class="Symbol">=</a> <a id="9184" href="Function.Related.html#9167" class="Bound">X</a> <a id="9186" href="Function.Related.html#EquationalReasoning._%E2%88%BC%E2%9F%A8_%E2%9F%A9_" class="Function Operator">∼⟨</a> <a id="9189" href="Function.Related.html#%E2%89%A1%E2%87%92" class="Function">≡⇒</a> <a id="9192" href="Function.Related.html#9172" class="Bound">X≡Y</a> <a id="9196" href="Function.Related.html#EquationalReasoning._%E2%88%BC%E2%9F%A8_%E2%9F%A9_" class="Function Operator">⟩</a> <a id="9198" href="Function.Related.html#9178" class="Bound">Y⇔Z</a>

  <a id="EquationalReasoning._∎" href="Function.Related.html#EquationalReasoning._%E2%88%8E" class="Function Operator">_∎</a> <a id="9208" class="Symbol">:</a> <a id="9210" class="Symbol">∀</a> <a id="9212" class="Symbol">{</a><a id="9213" href="Function.Related.html#9213" class="Bound">k</a> <a id="9215" href="Function.Related.html#9215" class="Bound">x</a><a id="9216" class="Symbol">}</a> <a id="9218" class="Symbol">(</a><a id="9219" href="Function.Related.html#9219" class="Bound">X</a> <a id="9221" class="Symbol">:</a> <a id="9223" class="PrimitiveType">Set</a> <a id="9227" href="Function.Related.html#9215" class="Bound">x</a><a id="9228" class="Symbol">)</a> <a id="9230" class="Symbol">→</a> <a id="9232" href="Function.Related.html#9219" class="Bound">X</a> <a id="9234" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="9237" href="Function.Related.html#9213" class="Bound">k</a> <a id="9239" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="9241" href="Function.Related.html#9219" class="Bound">X</a>
  <a id="9245" href="Function.Related.html#9245" class="Bound">X</a> <a id="9247" href="Function.Related.html#EquationalReasoning._%E2%88%8E" class="Function Operator">∎</a> <a id="9249" class="Symbol">=</a> <a id="9251" href="Function.Related.html#EquationalReasoning.refl" class="Function">refl</a>

<a id="9257" class="Comment">-- For a symmetric kind and a fixed universe level we can construct a</a>
<a id="9327" class="Comment">-- setoid.</a>

<a id="setoid" href="Function.Related.html#setoid" class="Function">setoid</a> <a id="9346" class="Symbol">:</a> <a id="9348" href="Function.Related.html#Symmetric-kind" class="Datatype">Symmetric-kind</a> <a id="9363" class="Symbol">→</a> <a id="9365" class="Symbol">(</a><a id="9366" href="Function.Related.html#9366" class="Bound">ℓ</a> <a id="9368" class="Symbol">:</a> <a id="9370" href="Agda.Primitive.html#Level" class="Postulate">Level</a><a id="9375" class="Symbol">)</a> <a id="9377" class="Symbol">→</a> <a id="9379" href="Relation.Binary.html#Setoid" class="Record">Setoid</a> <a id="9386" class="Symbol">_</a> <a id="9388" class="Symbol">_</a>
<a id="9390" href="Function.Related.html#setoid" class="Function">setoid</a> <a id="9397" href="Function.Related.html#9397" class="Bound">k</a> <a id="9399" href="Function.Related.html#9399" class="Bound">ℓ</a> <a id="9401" class="Symbol">=</a> <a id="9403" class="Keyword">record</a>
  <a id="9412" class="Symbol">{</a> <a id="9414" class="Field">Carrier</a>       <a id="9428" class="Symbol">=</a> <a id="9430" class="PrimitiveType">Set</a> <a id="9434" href="Function.Related.html#9399" class="Bound">ℓ</a>
  <a id="9438" class="Symbol">;</a> <a id="9440" class="Field Operator">_≈_</a>           <a id="9454" class="Symbol">=</a> <a id="9456" href="Function.Related.html#Related" class="Function">Related</a> <a id="9464" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌊</a> <a id="9466" href="Function.Related.html#9397" class="Bound">k</a> <a id="9468" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌋</a>
  <a id="9472" class="Symbol">;</a> <a id="9474" class="Field">isEquivalence</a> <a id="9488" class="Symbol">=</a>
      <a id="9496" class="Keyword">record</a> <a id="9503" class="Symbol">{</a><a id="9504" class="Field">refl</a> <a id="9509" class="Symbol">=</a> <a id="9511" class="Symbol">_</a> <a id="9513" href="Function.Related.html#EquationalReasoning._%E2%88%8E" class="Function Operator">∎</a><a id="9514" class="Symbol">;</a> <a id="9516" class="Field">sym</a> <a id="9520" class="Symbol">=</a> <a id="9522" href="Function.Related.html#EquationalReasoning.sym" class="Function">sym</a><a id="9525" class="Symbol">;</a> <a id="9527" class="Field">trans</a> <a id="9533" class="Symbol">=</a> <a id="9535" href="Function.Related.html#EquationalReasoning._%E2%88%BC%E2%9F%A8_%E2%9F%A9_" class="Function Operator">_∼⟨_⟩_</a> <a id="9542" class="Symbol">_}</a>
  <a id="9547" class="Symbol">}</a> <a id="9549" class="Keyword">where</a> <a id="9555" class="Keyword">open</a> <a id="9560" href="Function.Related.html#EquationalReasoning" class="Module">EquationalReasoning</a>

<a id="9581" class="Comment">-- For an arbitrary kind and a fixed universe level we can construct a</a>
<a id="9652" class="Comment">-- preorder.</a>

<a id="preorder" href="Function.Related.html#preorder" class="Function">preorder</a> <a id="9675" class="Symbol">:</a> <a id="9677" href="Function.Related.html#Kind" class="Datatype">Kind</a> <a id="9682" class="Symbol">→</a> <a id="9684" class="Symbol">(</a><a id="9685" href="Function.Related.html#9685" class="Bound">ℓ</a> <a id="9687" class="Symbol">:</a> <a id="9689" href="Agda.Primitive.html#Level" class="Postulate">Level</a><a id="9694" class="Symbol">)</a> <a id="9696" class="Symbol">→</a> <a id="9698" href="Relation.Binary.html#Preorder" class="Record">Preorder</a> <a id="9707" class="Symbol">_</a> <a id="9709" class="Symbol">_</a> <a id="9711" class="Symbol">_</a>
<a id="9713" href="Function.Related.html#preorder" class="Function">preorder</a> <a id="9722" href="Function.Related.html#9722" class="Bound">k</a> <a id="9724" href="Function.Related.html#9724" class="Bound">ℓ</a> <a id="9726" class="Symbol">=</a> <a id="9728" class="Keyword">record</a>
  <a id="9737" class="Symbol">{</a> <a id="9739" class="Field">Carrier</a>    <a id="9750" class="Symbol">=</a> <a id="9752" class="PrimitiveType">Set</a> <a id="9756" href="Function.Related.html#9724" class="Bound">ℓ</a>
  <a id="9760" class="Symbol">;</a> <a id="9762" class="Field Operator">_≈_</a>        <a id="9773" class="Symbol">=</a> <a id="9775" href="Function.Inverse.html#_%E2%86%94_" class="Function Operator">_↔_</a>
  <a id="9781" class="Symbol">;</a> <a id="9783" class="Field Operator">_∼_</a>        <a id="9794" class="Symbol">=</a> <a id="9796" href="Function.Related.html#Related" class="Function">Related</a> <a id="9804" href="Function.Related.html#9722" class="Bound">k</a>
  <a id="9808" class="Symbol">;</a> <a id="9810" class="Field">isPreorder</a> <a id="9821" class="Symbol">=</a> <a id="9823" class="Keyword">record</a>
    <a id="9834" class="Symbol">{</a> <a id="9836" class="Field">isEquivalence</a> <a id="9850" class="Symbol">=</a> <a id="9852" href="Relation.Binary.html#Setoid.isEquivalence" class="Field">Setoid.isEquivalence</a> <a id="9873" class="Symbol">(</a><a id="9874" href="Function.Related.html#setoid" class="Function">setoid</a> <a id="9881" href="Function.Related.html#Symmetric-kind.bijection" class="InductiveConstructor">bijection</a> <a id="9891" href="Function.Related.html#9724" class="Bound">ℓ</a><a id="9892" class="Symbol">)</a>
    <a id="9898" class="Symbol">;</a> <a id="9900" class="Field">reflexive</a>     <a id="9914" class="Symbol">=</a> <a id="9916" href="Function.Related.html#%E2%86%94%E2%87%92" class="Function">↔⇒</a>
    <a id="9923" class="Symbol">;</a> <a id="9925" class="Field">trans</a>         <a id="9939" class="Symbol">=</a> <a id="9941" href="Function.Related.html#EquationalReasoning._%E2%88%BC%E2%9F%A8_%E2%9F%A9_" class="Function Operator">_∼⟨_⟩_</a> <a id="9948" class="Symbol">_</a>
    <a id="9954" class="Symbol">}</a>
  <a id="9958" class="Symbol">}</a> <a id="9960" class="Keyword">where</a> <a id="9966" class="Keyword">open</a> <a id="9971" href="Function.Related.html#EquationalReasoning" class="Module">EquationalReasoning</a>

<a id="9992" class="Comment">------------------------------------------------------------------------</a>
<a id="10065" class="Comment">-- Some induced relations</a>

<a id="10092" class="Comment">-- Every unary relation induces a preorder and, for symmetric kinds,</a>
<a id="10161" class="Comment">-- an equivalence. (No claim is made that these relations are unique.)</a>

<a id="InducedRelation₁" href="Function.Related.html#InducedRelation%E2%82%81" class="Function">InducedRelation₁</a> <a id="10250" class="Symbol">:</a> <a id="10252" href="Function.Related.html#Kind" class="Datatype">Kind</a> <a id="10257" class="Symbol">→</a> <a id="10259" class="Symbol">∀</a> <a id="10261" class="Symbol">{</a><a id="10262" href="Function.Related.html#10262" class="Bound">a</a> <a id="10264" href="Function.Related.html#10264" class="Bound">s</a><a id="10265" class="Symbol">}</a> <a id="10267" class="Symbol">{</a><a id="10268" href="Function.Related.html#10268" class="Bound">A</a> <a id="10270" class="Symbol">:</a> <a id="10272" class="PrimitiveType">Set</a> <a id="10276" href="Function.Related.html#10262" class="Bound">a</a><a id="10277" class="Symbol">}</a> <a id="10279" class="Symbol">→</a>
                   <a id="10300" class="Symbol">(</a><a id="10301" href="Function.Related.html#10268" class="Bound">A</a> <a id="10303" class="Symbol">→</a> <a id="10305" class="PrimitiveType">Set</a> <a id="10309" href="Function.Related.html#10264" class="Bound">s</a><a id="10310" class="Symbol">)</a> <a id="10312" class="Symbol">→</a> <a id="10314" href="Function.Related.html#10268" class="Bound">A</a> <a id="10316" class="Symbol">→</a> <a id="10318" href="Function.Related.html#10268" class="Bound">A</a> <a id="10320" class="Symbol">→</a> <a id="10322" class="PrimitiveType">Set</a> <a id="10326" class="Symbol">_</a>
<a id="10328" href="Function.Related.html#InducedRelation%E2%82%81" class="Function">InducedRelation₁</a> <a id="10345" href="Function.Related.html#10345" class="Bound">k</a> <a id="10347" href="Function.Related.html#10347" class="Bound">S</a> <a id="10349" class="Symbol">=</a> <a id="10351" class="Symbol">λ</a> <a id="10353" href="Function.Related.html#10353" class="Bound">x</a> <a id="10355" href="Function.Related.html#10355" class="Bound">y</a> <a id="10357" class="Symbol">→</a> <a id="10359" href="Function.Related.html#10347" class="Bound">S</a> <a id="10361" href="Function.Related.html#10353" class="Bound">x</a> <a id="10363" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="10366" href="Function.Related.html#10345" class="Bound">k</a> <a id="10368" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="10370" href="Function.Related.html#10347" class="Bound">S</a> <a id="10372" href="Function.Related.html#10355" class="Bound">y</a>

<a id="InducedPreorder₁" href="Function.Related.html#InducedPreorder%E2%82%81" class="Function">InducedPreorder₁</a> <a id="10392" class="Symbol">:</a> <a id="10394" href="Function.Related.html#Kind" class="Datatype">Kind</a> <a id="10399" class="Symbol">→</a> <a id="10401" class="Symbol">∀</a> <a id="10403" class="Symbol">{</a><a id="10404" href="Function.Related.html#10404" class="Bound">a</a> <a id="10406" href="Function.Related.html#10406" class="Bound">s</a><a id="10407" class="Symbol">}</a> <a id="10409" class="Symbol">{</a><a id="10410" href="Function.Related.html#10410" class="Bound">A</a> <a id="10412" class="Symbol">:</a> <a id="10414" class="PrimitiveType">Set</a> <a id="10418" href="Function.Related.html#10404" class="Bound">a</a><a id="10419" class="Symbol">}</a> <a id="10421" class="Symbol">→</a>
                   <a id="10442" class="Symbol">(</a><a id="10443" href="Function.Related.html#10410" class="Bound">A</a> <a id="10445" class="Symbol">→</a> <a id="10447" class="PrimitiveType">Set</a> <a id="10451" href="Function.Related.html#10406" class="Bound">s</a><a id="10452" class="Symbol">)</a> <a id="10454" class="Symbol">→</a> <a id="10456" href="Relation.Binary.html#Preorder" class="Record">Preorder</a> <a id="10465" class="Symbol">_</a> <a id="10467" class="Symbol">_</a> <a id="10469" class="Symbol">_</a>
<a id="10471" href="Function.Related.html#InducedPreorder%E2%82%81" class="Function">InducedPreorder₁</a> <a id="10488" href="Function.Related.html#10488" class="Bound">k</a> <a id="10490" href="Function.Related.html#10490" class="Bound">S</a> <a id="10492" class="Symbol">=</a> <a id="10494" class="Keyword">record</a>
  <a id="10503" class="Symbol">{</a> <a id="10505" class="Field Operator">_≈_</a>        <a id="10516" class="Symbol">=</a> <a id="10518" href="Agda.Builtin.Equality.html#_%E2%89%A1_" class="Datatype Operator">P._≡_</a>
  <a id="10526" class="Symbol">;</a> <a id="10528" class="Field Operator">_∼_</a>        <a id="10539" class="Symbol">=</a> <a id="10541" href="Function.Related.html#InducedRelation%E2%82%81" class="Function">InducedRelation₁</a> <a id="10558" href="Function.Related.html#10488" class="Bound">k</a> <a id="10560" href="Function.Related.html#10490" class="Bound">S</a>
  <a id="10564" class="Symbol">;</a> <a id="10566" class="Field">isPreorder</a> <a id="10577" class="Symbol">=</a> <a id="10579" class="Keyword">record</a>
    <a id="10590" class="Symbol">{</a> <a id="10592" class="Field">isEquivalence</a> <a id="10606" class="Symbol">=</a> <a id="10608" href="Relation.Binary.PropositionalEquality.Core.html#isEquivalence" class="Function">P.isEquivalence</a>
    <a id="10628" class="Symbol">;</a> <a id="10630" class="Field">reflexive</a>     <a id="10644" class="Symbol">=</a> <a id="10646" href="Relation.Binary.html#1160" class="Function">reflexive</a> <a id="10656" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a>
                      <a id="10680" href="Relation.Binary.Core.html#5012" class="Function">Setoid.reflexive</a> <a id="10697" class="Symbol">(</a><a id="10698" href="Function.Related.html#setoid" class="Function">setoid</a> <a id="10705" href="Function.Related.html#Symmetric-kind.bijection" class="InductiveConstructor">bijection</a> <a id="10715" class="Symbol">_)</a> <a id="10718" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a>
                      <a id="10742" href="Relation.Binary.PropositionalEquality.html#cong" class="Function">P.cong</a> <a id="10749" href="Function.Related.html#10490" class="Bound">S</a>
    <a id="10755" class="Symbol">;</a> <a id="10757" class="Field">trans</a>         <a id="10771" class="Symbol">=</a> <a id="10773" href="Relation.Binary.html#1190" class="Function">trans</a>
    <a id="10783" class="Symbol">}</a>
  <a id="10787" class="Symbol">}</a> <a id="10789" class="Keyword">where</a> <a id="10795" class="Keyword">open</a> <a id="10800" href="Relation.Binary.html#Preorder" class="Module">Preorder</a> <a id="10809" class="Symbol">(</a><a id="10810" href="Function.Related.html#preorder" class="Function">preorder</a> <a id="10819" class="Symbol">_</a> <a id="10821" class="Symbol">_)</a>

<a id="InducedEquivalence₁" href="Function.Related.html#InducedEquivalence%E2%82%81" class="Function">InducedEquivalence₁</a> <a id="10845" class="Symbol">:</a> <a id="10847" href="Function.Related.html#Symmetric-kind" class="Datatype">Symmetric-kind</a> <a id="10862" class="Symbol">→</a> <a id="10864" class="Symbol">∀</a> <a id="10866" class="Symbol">{</a><a id="10867" href="Function.Related.html#10867" class="Bound">a</a> <a id="10869" href="Function.Related.html#10869" class="Bound">s</a><a id="10870" class="Symbol">}</a> <a id="10872" class="Symbol">{</a><a id="10873" href="Function.Related.html#10873" class="Bound">A</a> <a id="10875" class="Symbol">:</a> <a id="10877" class="PrimitiveType">Set</a> <a id="10881" href="Function.Related.html#10867" class="Bound">a</a><a id="10882" class="Symbol">}</a> <a id="10884" class="Symbol">→</a>
                      <a id="10908" class="Symbol">(</a><a id="10909" href="Function.Related.html#10873" class="Bound">A</a> <a id="10911" class="Symbol">→</a> <a id="10913" class="PrimitiveType">Set</a> <a id="10917" href="Function.Related.html#10869" class="Bound">s</a><a id="10918" class="Symbol">)</a> <a id="10920" class="Symbol">→</a> <a id="10922" href="Relation.Binary.html#Setoid" class="Record">Setoid</a> <a id="10929" class="Symbol">_</a> <a id="10931" class="Symbol">_</a>
<a id="10933" href="Function.Related.html#InducedEquivalence%E2%82%81" class="Function">InducedEquivalence₁</a> <a id="10953" href="Function.Related.html#10953" class="Bound">k</a> <a id="10955" href="Function.Related.html#10955" class="Bound">S</a> <a id="10957" class="Symbol">=</a> <a id="10959" class="Keyword">record</a>
  <a id="10968" class="Symbol">{</a> <a id="10970" class="Field Operator">_≈_</a>           <a id="10984" class="Symbol">=</a> <a id="10986" href="Function.Related.html#InducedRelation%E2%82%81" class="Function">InducedRelation₁</a> <a id="11003" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌊</a> <a id="11005" href="Function.Related.html#10953" class="Bound">k</a> <a id="11007" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌋</a> <a id="11009" href="Function.Related.html#10955" class="Bound">S</a>
  <a id="11013" class="Symbol">;</a> <a id="11015" class="Field">isEquivalence</a> <a id="11029" class="Symbol">=</a> <a id="11031" class="Keyword">record</a> <a id="11038" class="Symbol">{</a><a id="11039" class="Field">refl</a> <a id="11044" class="Symbol">=</a> <a id="11046" href="Relation.Binary.Core.html#4934" class="Function">refl</a><a id="11050" class="Symbol">;</a> <a id="11052" class="Field">sym</a> <a id="11056" class="Symbol">=</a> <a id="11058" href="Relation.Binary.Core.html#4960" class="Function">sym</a><a id="11061" class="Symbol">;</a> <a id="11063" class="Field">trans</a> <a id="11069" class="Symbol">=</a> <a id="11071" href="Relation.Binary.Core.html#4986" class="Function">trans</a><a id="11076" class="Symbol">}</a>
  <a id="11080" class="Symbol">}</a> <a id="11082" class="Keyword">where</a> <a id="11088" class="Keyword">open</a> <a id="11093" href="Relation.Binary.html#Setoid" class="Module">Setoid</a> <a id="11100" class="Symbol">(</a><a id="11101" href="Function.Related.html#setoid" class="Function">setoid</a> <a id="11108" class="Symbol">_</a> <a id="11110" class="Symbol">_)</a>

<a id="11114" class="Comment">-- Every binary relation induces a preorder and, for symmetric kinds,</a>
<a id="11184" class="Comment">-- an equivalence. (No claim is made that these relations are unique.)</a>

<a id="InducedRelation₂" href="Function.Related.html#InducedRelation%E2%82%82" class="Function">InducedRelation₂</a> <a id="11273" class="Symbol">:</a> <a id="11275" href="Function.Related.html#Kind" class="Datatype">Kind</a> <a id="11280" class="Symbol">→</a> <a id="11282" class="Symbol">∀</a> <a id="11284" class="Symbol">{</a><a id="11285" href="Function.Related.html#11285" class="Bound">a</a> <a id="11287" href="Function.Related.html#11287" class="Bound">b</a> <a id="11289" href="Function.Related.html#11289" class="Bound">s</a><a id="11290" class="Symbol">}</a> <a id="11292" class="Symbol">{</a><a id="11293" href="Function.Related.html#11293" class="Bound">A</a> <a id="11295" class="Symbol">:</a> <a id="11297" class="PrimitiveType">Set</a> <a id="11301" href="Function.Related.html#11285" class="Bound">a</a><a id="11302" class="Symbol">}</a> <a id="11304" class="Symbol">{</a><a id="11305" href="Function.Related.html#11305" class="Bound">B</a> <a id="11307" class="Symbol">:</a> <a id="11309" class="PrimitiveType">Set</a> <a id="11313" href="Function.Related.html#11287" class="Bound">b</a><a id="11314" class="Symbol">}</a> <a id="11316" class="Symbol">→</a>
                   <a id="11337" class="Symbol">(</a><a id="11338" href="Function.Related.html#11293" class="Bound">A</a> <a id="11340" class="Symbol">→</a> <a id="11342" href="Function.Related.html#11305" class="Bound">B</a> <a id="11344" class="Symbol">→</a> <a id="11346" class="PrimitiveType">Set</a> <a id="11350" href="Function.Related.html#11289" class="Bound">s</a><a id="11351" class="Symbol">)</a> <a id="11353" class="Symbol">→</a> <a id="11355" href="Function.Related.html#11305" class="Bound">B</a> <a id="11357" class="Symbol">→</a> <a id="11359" href="Function.Related.html#11305" class="Bound">B</a> <a id="11361" class="Symbol">→</a> <a id="11363" class="PrimitiveType">Set</a> <a id="11367" class="Symbol">_</a>
<a id="11369" href="Function.Related.html#InducedRelation%E2%82%82" class="Function">InducedRelation₂</a> <a id="11386" href="Function.Related.html#11386" class="Bound">k</a> <a id="11388" href="Function.Related.html#11388" class="Bound Operator">_S_</a> <a id="11392" class="Symbol">=</a> <a id="11394" class="Symbol">λ</a> <a id="11396" href="Function.Related.html#11396" class="Bound">x</a> <a id="11398" href="Function.Related.html#11398" class="Bound">y</a> <a id="11400" class="Symbol">→</a> <a id="11402" class="Symbol">∀</a> <a id="11404" class="Symbol">{</a><a id="11405" href="Function.Related.html#11405" class="Bound">z</a><a id="11406" class="Symbol">}</a> <a id="11408" class="Symbol">→</a> <a id="11410" class="Symbol">(</a><a id="11411" href="Function.Related.html#11405" class="Bound">z</a> <a id="11413" href="Function.Related.html#11388" class="Bound Operator">S</a> <a id="11415" href="Function.Related.html#11396" class="Bound">x</a><a id="11416" class="Symbol">)</a> <a id="11418" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">∼[</a> <a id="11421" href="Function.Related.html#11386" class="Bound">k</a> <a id="11423" href="Function.Related.html#_%E2%88%BC%5B_%5D_" class="Function Operator">]</a> <a id="11425" class="Symbol">(</a><a id="11426" href="Function.Related.html#11405" class="Bound">z</a> <a id="11428" href="Function.Related.html#11388" class="Bound Operator">S</a> <a id="11430" href="Function.Related.html#11398" class="Bound">y</a><a id="11431" class="Symbol">)</a>

<a id="InducedPreorder₂" href="Function.Related.html#InducedPreorder%E2%82%82" class="Function">InducedPreorder₂</a> <a id="11451" class="Symbol">:</a> <a id="11453" href="Function.Related.html#Kind" class="Datatype">Kind</a> <a id="11458" class="Symbol">→</a> <a id="11460" class="Symbol">∀</a> <a id="11462" class="Symbol">{</a><a id="11463" href="Function.Related.html#11463" class="Bound">a</a> <a id="11465" href="Function.Related.html#11465" class="Bound">b</a> <a id="11467" href="Function.Related.html#11467" class="Bound">s</a><a id="11468" class="Symbol">}</a> <a id="11470" class="Symbol">{</a><a id="11471" href="Function.Related.html#11471" class="Bound">A</a> <a id="11473" class="Symbol">:</a> <a id="11475" class="PrimitiveType">Set</a> <a id="11479" href="Function.Related.html#11463" class="Bound">a</a><a id="11480" class="Symbol">}</a> <a id="11482" class="Symbol">{</a><a id="11483" href="Function.Related.html#11483" class="Bound">B</a> <a id="11485" class="Symbol">:</a> <a id="11487" class="PrimitiveType">Set</a> <a id="11491" href="Function.Related.html#11465" class="Bound">b</a><a id="11492" class="Symbol">}</a> <a id="11494" class="Symbol">→</a>
                   <a id="11515" class="Symbol">(</a><a id="11516" href="Function.Related.html#11471" class="Bound">A</a> <a id="11518" class="Symbol">→</a> <a id="11520" href="Function.Related.html#11483" class="Bound">B</a> <a id="11522" class="Symbol">→</a> <a id="11524" class="PrimitiveType">Set</a> <a id="11528" href="Function.Related.html#11467" class="Bound">s</a><a id="11529" class="Symbol">)</a> <a id="11531" class="Symbol">→</a> <a id="11533" href="Relation.Binary.html#Preorder" class="Record">Preorder</a> <a id="11542" class="Symbol">_</a> <a id="11544" class="Symbol">_</a> <a id="11546" class="Symbol">_</a>
<a id="11548" href="Function.Related.html#InducedPreorder%E2%82%82" class="Function">InducedPreorder₂</a> <a id="11565" href="Function.Related.html#11565" class="Bound">k</a> <a id="11567" href="Function.Related.html#11567" class="Bound Operator">_S_</a> <a id="11571" class="Symbol">=</a> <a id="11573" class="Keyword">record</a>
  <a id="11582" class="Symbol">{</a> <a id="11584" class="Field Operator">_≈_</a>        <a id="11595" class="Symbol">=</a> <a id="11597" href="Agda.Builtin.Equality.html#_%E2%89%A1_" class="Datatype Operator">P._≡_</a>
  <a id="11605" class="Symbol">;</a> <a id="11607" class="Field Operator">_∼_</a>        <a id="11618" class="Symbol">=</a> <a id="11620" href="Function.Related.html#InducedRelation%E2%82%82" class="Function">InducedRelation₂</a> <a id="11637" href="Function.Related.html#11565" class="Bound">k</a> <a id="11639" href="Function.Related.html#11567" class="Bound Operator">_S_</a>
  <a id="11645" class="Symbol">;</a> <a id="11647" class="Field">isPreorder</a> <a id="11658" class="Symbol">=</a> <a id="11660" class="Keyword">record</a>
    <a id="11671" class="Symbol">{</a> <a id="11673" class="Field">isEquivalence</a> <a id="11687" class="Symbol">=</a> <a id="11689" href="Relation.Binary.PropositionalEquality.Core.html#isEquivalence" class="Function">P.isEquivalence</a>
    <a id="11709" class="Symbol">;</a> <a id="11711" class="Field">reflexive</a>     <a id="11725" class="Symbol">=</a> <a id="11727" class="Symbol">λ</a> <a id="11729" href="Function.Related.html#11729" class="Bound">x≡y</a> <a id="11733" class="Symbol">{</a><a id="11734" href="Function.Related.html#11734" class="Bound">z</a><a id="11735" class="Symbol">}</a> <a id="11737" class="Symbol">→</a>
                        <a id="11763" href="Relation.Binary.html#1160" class="Function">reflexive</a> <a id="11773" href="Function.html#_%24_" class="Function Operator">$</a>
                        <a id="11799" href="Relation.Binary.Core.html#5012" class="Function">Setoid.reflexive</a> <a id="11816" class="Symbol">(</a><a id="11817" href="Function.Related.html#setoid" class="Function">setoid</a> <a id="11824" href="Function.Related.html#Symmetric-kind.bijection" class="InductiveConstructor">bijection</a> <a id="11834" class="Symbol">_)</a> <a id="11837" href="Function.html#_%24_" class="Function Operator">$</a>
                        <a id="11863" href="Relation.Binary.PropositionalEquality.html#cong" class="Function">P.cong</a> <a id="11870" class="Symbol">(</a><a id="11871" href="Function.Related.html#11567" class="Bound Operator">_S_</a> <a id="11875" href="Function.Related.html#11734" class="Bound">z</a><a id="11876" class="Symbol">)</a> <a id="11878" href="Function.Related.html#11729" class="Bound">x≡y</a>

    <a id="11887" class="Symbol">;</a> <a id="11889" class="Field">trans</a>         <a id="11903" class="Symbol">=</a> <a id="11905" class="Symbol">λ</a> <a id="11907" href="Function.Related.html#11907" class="Bound">i↝j</a> <a id="11911" href="Function.Related.html#11911" class="Bound">j↝k</a> <a id="11915" class="Symbol">→</a> <a id="11917" href="Relation.Binary.html#1190" class="Function">trans</a> <a id="11923" href="Function.Related.html#11907" class="Bound">i↝j</a> <a id="11927" href="Function.Related.html#11911" class="Bound">j↝k</a>
    <a id="11935" class="Symbol">}</a>
  <a id="11939" class="Symbol">}</a> <a id="11941" class="Keyword">where</a> <a id="11947" class="Keyword">open</a> <a id="11952" href="Relation.Binary.html#Preorder" class="Module">Preorder</a> <a id="11961" class="Symbol">(</a><a id="11962" href="Function.Related.html#preorder" class="Function">preorder</a> <a id="11971" class="Symbol">_</a> <a id="11973" class="Symbol">_)</a>

<a id="InducedEquivalence₂" href="Function.Related.html#InducedEquivalence%E2%82%82" class="Function">InducedEquivalence₂</a> <a id="11997" class="Symbol">:</a> <a id="11999" href="Function.Related.html#Symmetric-kind" class="Datatype">Symmetric-kind</a> <a id="12014" class="Symbol">→</a>
                      <a id="12038" class="Symbol">∀</a> <a id="12040" class="Symbol">{</a><a id="12041" href="Function.Related.html#12041" class="Bound">a</a> <a id="12043" href="Function.Related.html#12043" class="Bound">b</a> <a id="12045" href="Function.Related.html#12045" class="Bound">s</a><a id="12046" class="Symbol">}</a> <a id="12048" class="Symbol">{</a><a id="12049" href="Function.Related.html#12049" class="Bound">A</a> <a id="12051" class="Symbol">:</a> <a id="12053" class="PrimitiveType">Set</a> <a id="12057" href="Function.Related.html#12041" class="Bound">a</a><a id="12058" class="Symbol">}</a> <a id="12060" class="Symbol">{</a><a id="12061" href="Function.Related.html#12061" class="Bound">B</a> <a id="12063" class="Symbol">:</a> <a id="12065" class="PrimitiveType">Set</a> <a id="12069" href="Function.Related.html#12043" class="Bound">b</a><a id="12070" class="Symbol">}</a> <a id="12072" class="Symbol">→</a>
                      <a id="12096" class="Symbol">(</a><a id="12097" href="Function.Related.html#12049" class="Bound">A</a> <a id="12099" class="Symbol">→</a> <a id="12101" href="Function.Related.html#12061" class="Bound">B</a> <a id="12103" class="Symbol">→</a> <a id="12105" class="PrimitiveType">Set</a> <a id="12109" href="Function.Related.html#12045" class="Bound">s</a><a id="12110" class="Symbol">)</a> <a id="12112" class="Symbol">→</a> <a id="12114" href="Relation.Binary.html#Setoid" class="Record">Setoid</a> <a id="12121" class="Symbol">_</a> <a id="12123" class="Symbol">_</a>
<a id="12125" href="Function.Related.html#InducedEquivalence%E2%82%82" class="Function">InducedEquivalence₂</a> <a id="12145" href="Function.Related.html#12145" class="Bound">k</a> <a id="12147" href="Function.Related.html#12147" class="Bound Operator">_S_</a> <a id="12151" class="Symbol">=</a> <a id="12153" class="Keyword">record</a>
  <a id="12162" class="Symbol">{</a> <a id="12164" class="Field Operator">_≈_</a>           <a id="12178" class="Symbol">=</a> <a id="12180" href="Function.Related.html#InducedRelation%E2%82%82" class="Function">InducedRelation₂</a> <a id="12197" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌊</a> <a id="12199" href="Function.Related.html#12145" class="Bound">k</a> <a id="12201" href="Function.Related.html#%E2%8C%8A_%E2%8C%8B" class="Function Operator">⌋</a> <a id="12203" href="Function.Related.html#12147" class="Bound Operator">_S_</a>
  <a id="12209" class="Symbol">;</a> <a id="12211" class="Field">isEquivalence</a> <a id="12225" class="Symbol">=</a> <a id="12227" class="Keyword">record</a>
    <a id="12238" class="Symbol">{</a> <a id="12240" class="Field">refl</a>  <a id="12246" class="Symbol">=</a> <a id="12248" href="Relation.Binary.Core.html#4934" class="Function">refl</a>
    <a id="12257" class="Symbol">;</a> <a id="12259" class="Field">sym</a>   <a id="12265" class="Symbol">=</a> <a id="12267" class="Symbol">λ</a> <a id="12269" href="Function.Related.html#12269" class="Bound">i↝j</a> <a id="12273" class="Symbol">→</a> <a id="12275" href="Relation.Binary.Core.html#4960" class="Function">sym</a> <a id="12279" href="Function.Related.html#12269" class="Bound">i↝j</a>
    <a id="12287" class="Symbol">;</a> <a id="12289" class="Field">trans</a> <a id="12295" class="Symbol">=</a> <a id="12297" class="Symbol">λ</a> <a id="12299" href="Function.Related.html#12299" class="Bound">i↝j</a> <a id="12303" href="Function.Related.html#12303" class="Bound">j↝k</a> <a id="12307" class="Symbol">→</a> <a id="12309" href="Relation.Binary.Core.html#4986" class="Function">trans</a> <a id="12315" href="Function.Related.html#12299" class="Bound">i↝j</a> <a id="12319" href="Function.Related.html#12303" class="Bound">j↝k</a>
    <a id="12327" class="Symbol">}</a>
  <a id="12331" class="Symbol">}</a> <a id="12333" class="Keyword">where</a> <a id="12339" class="Keyword">open</a> <a id="12344" href="Relation.Binary.html#Setoid" class="Module">Setoid</a> <a id="12351" class="Symbol">(</a><a id="12352" href="Function.Related.html#setoid" class="Function">setoid</a> <a id="12359" class="Symbol">_</a> <a id="12361" class="Symbol">_)</a>
</pre></body></html>

APT Browse - Built by Thomas Orozco.