-
Notifications
You must be signed in to change notification settings - Fork 0
/
hyperlink_references.rst
430 lines (404 loc) · 37.7 KB
/
hyperlink_references.rst
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
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
.. _2015 post by Floris van Doorn: https://homotopytypetheory.org/2015/12/02/the-proof-assistant-lean/
.. _absolute value: https://en.wikipedia.org/wiki/Absolute_value
.. _agda2-mode: https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.html
.. _agda-algebras: https://github.com/ualib/agda-algebras
.. _`agda-algebras development team`: https://github.com/ualib/agda-algebras#the-agda-algebras-development-team
.. _`agda-algebras-everything`: https://github.com/ualib/agda-algebras/blob/master/src/agda-algebras-everything.html
.. _`agda-categories paper`: https://doi.org/10.1145/3437992.3439922
.. _agda-categories: https://github.com/agda/agda-categories
.. _agda-ualib: https://gitlab.com/ualib/ualib.gitlab.io
.. _Agda: https://wiki.portal.chalmers.se/agda/pmwiki.php
.. _Agda Language Reference: https://agda.readthedocs.io/en/v2.6.2/language
.. _Agda Language Reference Manual: https://agda.readthedocs.io/en/v2.6.1/language
.. _Agda Standard Library: https://agda.github.io/agda-stdlib/
.. _Agda Tools: https://agda.readthedocs.io/en/v2.6.2/tools/
.. _Agda Tutorial: https://people.inf.elte.hu/pgj/agda/tutorial/Index.html
.. _Agda Universal Algebra Library: https://ualib.org
.. _Agda Universal Algebra Library repository: https://github.com/ualib/agda-algebras/
.. _Agda User's Manual: https://agda.readthedocs.io/
.. _Agda Wiki: https://wiki.portal.chalmers.se/agda/pmwiki.php
.. _Algebraic Effects and Handlers: https://www.cs.uoregon.edu/research/summerschool/summer18/topics.php#Bauer
.. _Andreas Abel: http://www.cse.chalmers.se/~abela/
.. _Andrej Bauer: http://www.andrej.com/index.html
.. _Axioms and Computation: https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#
.. _basic module: https://gitlab.com/ualib/ualib.gitlab.io/-/blob/master/basic.lagda.rst
.. _basic.lean: https://gitlab.com/ualib/lean-ualib/tree/william/src/basic.lean
.. _`Bergman (2012)`: https://www.amazon.com/gp/product/1439851298/ref=as_li_tl?ie=UTF8&camp=1789&creative=9325&creativeASIN=1439851298&linkCode=as2&tag=typefunc-20&linkId=440725c9b1e60817d071c1167dff95fa
.. _Bill Lampe: https://math.hawaii.edu/wordpress/people/william/
.. _birkhoff module: https://gitlab.com/ualib/ualib.gitlab.io/-/blob/master/birkhoff.lagda.rst
.. _birkhoff.lean: https://gitlab.com/ualib/lean-ualib/tree/william/src/birkhoff.lean
.. _Category Theory in Context: http://www.math.jhu.edu/~eriehl/context.pdf
.. _categorytheory.gitlab.io: https://categorytheory.gitlab.io
.. _Charles University in Prague: https://cuni.cz/UKEN-1.html
.. _classes.lean: https://github.com/leanprover/lean/blob/master/library/init/algebra/classes.lean
.. _classical.lean: https://github.com/leanprover/lean/blob/master/library/init/classical.lean
.. _Clifford Bergman: https://orion.math.iastate.edu/cbergman/
.. _Cliff Bergman: https://orion.math.iastate.edu/cbergman/
.. _clone.lean: https://gitlab.com/ualib/lean-ualib/tree/william/src/clone.lean
.. _closure module: https://gitlab.com/ualib/ualib.gitlab.io/-/blob/master/congruences.lagda.rst
.. _`cmdoption-safe`: https://agda.readthedocs.io/en/v2.6.1/tools/command-line-options.html#cmdoption-safe
.. _Coercions using Type Classes: https://leanprover.github.io/theorem_proving_in_lean/type_classes.html#coercions-using-type-classes
.. _Computer Aided Formal Reasoning: http://www.cs.nott.ac.uk/~psztxa/g53cfr/
.. _congruences module: https://gitlab.com/ualib/ualib.gitlab.io/-/blob/master/congruences.lagda.rst
.. _constructive mathematics: https://ncatlab.org/nlab/show/constructive+mathematics
.. _Coq: http://coq.inria.fr
.. _core.lean: https://github.com/leanprover/lean/blob/master/library/init/core.lean
.. _Course on Univalent Foundations: https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes
.. _Department of Algebra: https://www.mff.cuni.cz/en/ka
.. _dependent types: https://en.wikipedia.org/wiki/Dependent_type
.. _Dependent Types at Work: http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf
.. _Dependently Typed Programming in Agda: http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf
.. _emacs: https://www.gnu.org/software/emacs/
.. _Emacs: https://www.gnu.org/software/emacs/
.. _Equality Section: https://leanprover.github.io/logic_and_proof/first_order_logic.html?highlight=equality#equality
.. _`Escardó`: https://www.cs.bham.ac.uk/~mhe
.. _`Escardó's notes`: https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes
.. _Formalization of Universal Algebra in Agda: http://www.sciencedirect.com/science/article/pii/S1571066118300768
.. _free.lean: https://gitlab.com/ualib/lean-ualib/tree/william/src/free.lean
.. _function extensionality: https://ncatlab.org/nlab/show/function+extensionality
.. _function.lean: https://github.com/leanprover/lean/blob/master/library/init/function.lean
.. _functions.lean: https://github.com/leanprover/lean/blob/master/library/init/algebra/functions.lean
.. _`git repository of the agda-algebras library`: https://github.com/ualib/agda-algebras
.. _homomorphisms module: https://gitlab.com/ualib/ualib.gitlab.io/-/blob/master/homomorphisms.lagda.rst
.. _Homotopy Type Theory: https://homotopytypetheory.org/
.. _HoTT: https://homotopytypetheory.org/
.. _HoTT book: https://homotopytypetheory.org/book/
.. _HoTT-UF-in-Agda: https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html
.. _HSP Theorem: https://en.wikipedia.org/wiki/Variety_(universal_algebra)#Birkhoff's_theorem
.. _Hyeyoung Shin: https://hyeyoungshin.github.io/
.. _Implicit Arguments: https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#implicit-arguments
.. _Inductive Types in Lean: https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html
.. _inductive types: https://en.wikipedia.org/wiki/Intuitionistic_type_theory#Inductive_types
.. _Introduction to Univalent Foundations of Mathematics with Agda: https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/index.html
.. _Jacques Carette: http://www.cas.mcmaster.ca/~carette/
.. _JB Nation: http://www.math.hawaii.edu/~jb/
.. _Jeremy Avigad: http://www.andrew.cmu.edu/user/avigad/
.. _lattice.lean: https://github.com/leanprover-community/mathlib/blob/master/src/data/set/lattice.lean
.. _Lean: https://leanprover.github.io/
.. _Lean 2: https://github.com/leanprover/lean2
.. _Lean 4: https://github.com/leanprover/lean4
.. _lean extension: https://github.com/leanprover/vscode-lean
.. _Lean github repository: https://github.com/leanprover/lean/
.. _Lean Reference Manual: https://leanprover.github.io/reference/
.. _Lean Standard Library: https://github.com/leanprover/lean
.. _Lean Tutorial: https://leanprover.github.io/tutorial/
.. _Lean Universal Algebra Library: https://github.com/UniversalAlgebra/lean-ualib/
.. _Libor Barto: http://www.karlin.mff.cuni.cz/~barto/
.. _`lean/library/init`: https://github.com/leanprover/lean/tree/master/library/init
.. _`lean/library/init/algebra`: https://github.com/leanprover/lean/blob/master/library/init/algebra
.. _`lean/library/init/data`: https://github.com/leanprover/lean/tree/master/library/init/data
.. _lean_src: https://github.com/leanprover/lean
.. _Logic and Proof: https://leanprover.github.io/logic_and_proof/
.. _logic.lean: https://github.com/leanprover/lean/blob/master/library/init/logic.lean
.. _`A Machine-checked proof of Birkhoff's Variety Theorem in Martin-Löf Type Theory`: https://arxiv.org/abs/2101.10166
.. _markdown: https://daringfireball.net/projects/markdown/
.. _`Martin Escardo`: https://www.cs.bham.ac.uk/~mhe
.. _`Martín Escardó`: https://www.cs.bham.ac.uk/~mhe
.. _`Martín Escardó's notes`: https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes
.. _`Martin Escardo's installation hints`: https://github.com/martinescardo/HoTT-UF-Agda-Lecture-Notes/blob/master/INSTALL.md
.. _`Martín Hötzel Escardó`: https://www.cs.bham.ac.uk/~mhe
.. _`Martin Hötzel Escardo`: https://www.cs.bham.ac.uk/~mhe
.. _`Martin-Löf dependent type theory`: https://ncatlab.org/nlab/show/Martin-L%C3%B6f+dependent+type+theory
.. _`Martin-Löf type theory`: https://ncatlab.org/nlab/show/Martin-L%C3%B6f+dependent+type+theory
.. _master: https://gitlab.com/ualib/lean-ualib/tree/master
.. _Mathlib: https://github.com/leanprover-community/mathlib/
.. _Mathlib documentation: https://leanprover-community.github.io/papers/mathlib-paper.pdf
.. _`mathlib/src/data/set/basic.lean`: https://github.com/leanprover-community/mathlib/blob/master/src/data/set/basic.lean
.. _`McKenzie, McNulty, Taylor (2018)`: https://www.amazon.com/gp/product/1470442957/ref=as_li_qf_asin_il_tl?ie=UTF8&tag=typefunc-20&creative=9325&linkCode=as2&creativeASIN=1470442957&linkId=b3109d9c28ceb872df7d4b84b1cc4f29
.. _merge request: https://github.com/ualib/agda-algebras/compare
.. _MHE: https://www.cs.bham.ac.uk/~mhe
.. _`Miklós Maróti`: http://www.math.u-szeged.hu/~mmaroti/
.. _Midlands Graduate School in the Foundations of Computing Science: http://events.cs.bham.ac.uk/mgs2019/
.. _MLTT: https://ncatlab.org/nlab/show/Martin-L%C3%B6f+dependent+type+theory
.. _More on Implicit Arguments: https://leanprover.github.io/theorem_proving_in_lean/interacting_with_lean.html?highlight=implicit#more-on-implicit-arguments
.. _`nat/`: https://github.com/leanprover/lean/blob/master/library/init/data/nat
.. _ncatlab: https://ncatlab.org
.. _`ncatlab.org`: https://ncatlab.org
.. _new issue: https://github.com/ualib/agda-algebras/issues/new/choose
.. _nlab: https://ncatlab.org
.. _NuPRL: http://www.nuprl.org/
.. _OPLSS 2018: https://www.cs.uoregon.edu/research/summerschool/summer18/topics.php#Bauer
.. _order.lean: https://github.com/leanprover/lean/blob/master/library/init/algebra/order.lean
.. _Pattern matching and equality: https://agda.readthedocs.io/en/v2.6.1/tools/command-line-options.html#pattern-matching-and-equality
.. _Peter Mayr: http://math.colorado.edu/~mayr/
.. _prod.lean: https://github.com/leanprover/lean/blob/master/library/init/data/prod.lean
.. _prelude module: https://gitlab.com/ualib/ualib.gitlab.io/-/blob/master/prelude.lagda.rst
.. _Programming Language Foundations in Agda: https://plfa.github.io/
.. _Programming Languages Foundations in Agda: https://plfa.github.io/
.. _proof assistant: https://en.wikipedia.org/wiki/Proof_assistant
.. _proof tactics: https://en.wikipedia.org/wiki/Tactic_(proof_assistant)
.. _propext.lean: https://github.com/leanprover/lean/blob/master/library/init/propext.lean
.. _quot.lean: https://github.com/leanprover/lean/blob/master/library/init/data/quot.lean
.. _quotient.lean: https://gitlab.com/ualib/lean-ualib/blob/william/src/quotient.lean
.. _Ralph Freese: https://math.hawaii.edu/~ralph/
.. _reading material: https://arxiv.org/abs/1807.05923
.. _section on axiom K: https://agda.readthedocs.io/en/v2.6.1/language/without-k.html
.. _section on level lifting and lowering: https://ualib.org/agda-algebras/Overture.Preliminaries.html#level-lifting-and-lowering
.. _set.lean: https://github.com/leanprover/lean/blob/master/library/init/data/set.lean
.. _setoid.lean: https://github.com/leanprover/lean/blob/master/library/init/data/setoid.lean
.. _`sigma/`: https://github.com/leanprover/lean/blob/master/library/init/data/sigma/
.. _`sigma/basic.lean`: https://github.com/leanprover/lean/blob/master/library/init/data/sigma/basic.lean
.. _Siva Somayyajula: http://www.cs.cmu.edu/~ssomayya/
.. _`Streicher's K axiom`: https://ncatlab.org/nlab/show/axiom+K+%28type+theory%29
.. _subuniverses module: https://gitlab.com/ualib/ualib.gitlab.io/-/blob/master/subuniverses.lagda.rst
.. _terms module: https://gitlab.com/ualib/ualib.gitlab.io/-/blob/master/terms.lagda.rst
.. _Theorem Proving in Lean: https://leanprover.github.io/theorem_proving_in_lean/index.html
.. _this gist: https://gist.github.com/andrejbauer/3cc438ab38646516e5e9278fdb22022c
.. _TPL: https://leanprover.github.io/theorem_proving_in_lean/
.. _type theory: https://en.wikipedia.org/wiki/Type_theory
.. _Type Theory and Formal Proof: <https://www.cambridge.org/vi/academic/subjects/computer-science/programming-languages-and-applied-logic/type-theory-and-formal-proof-introduction>`_
.. _Type Topology: <https://github.com/martinescardo/TypeTopology>`_
.. _Univalent Foundations of Mathematics with Agda: https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/index.html
.. _Univalent Foundations with Agda: https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#additionalexercisessol
.. _Venanzio Capretta: https://www.duplavis.com/venanzio/
.. _vscode: https://code.visualstudio.com/
.. _wf.lean: https://github.com/leanprover/lean/blob/master/library/init/wf.lean
.. _william: https://gitlab.com/ualib/lean-ualib/tree/william
.. _William DeMeo: https://williamdemeo.org
.. _`[email protected]`: mailto:[email protected]
.. _williamdemeo at gmail dot com: mailto:[email protected]
.. _williamdemeo.org: https://williamdemeo.gitlab.io/
.. _`williamdemeo@gitlab`: https://gitlab.com/williamdemeo
.. _`williamdemeo@github`: https://github.com/williamdemeo
.. _`Base`: Base.html
.. _`Base.Adjunction`: https://ualib.org/src/Base.Adjunction.html
.. _`Base.Adjunction.Closure`: https://ualib.org/src/Base.Adjunction.Closure.html
.. _`Base.Adjunction.Galois`: https://ualib.org/src/Base.Adjunction.Galois.html
.. _`Base.Adjunction.Residuation`: https://ualib.org/src/Base.Adjunction.Residuation.html
.. _`Base.Algebras`: https://ualib.org/src/Base.Algebras.html
.. _`Base.Algebras.Basic`: https://ualib.org/src/Base.Algebras.Basic.html
.. _`Base.Algebras.Congruences`: https://ualib.org/src/Base.Algebras.Congruences.html
.. _`Base.Algebras.Products`: https://ualib.org/src/Base.Algebras.Products.html
.. _`Base.Categories`: https://ualib.org/src/Base.Categories.html
.. _`Base.Categories.Functors`: https://ualib.org/src/Base.Categories.Functors.html
.. _`Base.Complexity`: https://ualib.org/src/Base.Complexity.html
.. _`Base.Complexity.Basic`: https://ualib.org/src/Base.Complexity.Basic.html
.. _`Base.Complexity.CSP`: https://ualib.org/src/Base.Complexity.CSP.html
.. _`Base.Equality`: https://ualib.org/src/Base.Equality.html
.. _`Base.Equality.Extensionality`: https://ualib.org/src/Base.Equality.Extensionality.html
.. _`Base.Equality.Truncation`: https://ualib.org/src/Base.Equality.Truncation.html
.. _`Base.Equality.Welldefined`: https://ualib.org/src/Base.Equality.Welldefined.html
.. _`Base.Functions.Injective`: https://ualib.org/src/Base.Functions.Injective.html
.. _`Base.Functions.Inverses`: https://ualib.org/src/Base.Functions.Inverses.html
.. _`Base.Functions.Preliminaries`: https://ualib.org/src/Base.Functions.Preliminaries.html
.. _`Base.Functions.Surjective`: https://ualib.org/src/Base.Functions.Surjective.html
.. _`Base.Functions.Transformers`: https://ualib.org/src/Base.Functions.Transformers.html
.. _`Base.Homomorphisms`: https://ualib.org/src/Base.Homomorphisms.html
.. _`Base.Homomorphisms.Basic`: https://ualib.org/src/Base.Homomorphisms.Basic.html
.. _`Base.Homomorphisms.Factor`: https://ualib.org/src/Base.Homomorphisms.Factor.html
.. _`Base.Homomorphisms.HomomorphicImages`: https://ualib.org/src/Base.Homomorphisms.HomomorphicImages.html
.. _`Base.Homomorphisms.Isomorphisms`: https://ualib.org/src/Base.Homomorphisms.Isomorphisms.html
.. _`Base.Homomorphisms.Kernels`: https://ualib.org/src/Base.Homomorphisms.Kernels.html
.. _`Base.Homomorphisms.Noether`: https://ualib.org/src/Base.Homomorphisms.Noether.html
.. _`Base.Homomorphisms.Products`: https://ualib.org/src/Base.Homomorphisms.Products.html
.. _`Base.Homomorphisms.Properties`: https://ualib.org/src/Base.Homomorphisms.Properties.html
.. _`Base.Relations`: https://ualib.org/src/Base.Relations.html
.. _`Base.Relations.Continuous`: https://ualib.org/src/Base.Relations.Continuous.html
.. _`Base.Relations.Discrete`: https://ualib.org/src/Base.Relations.Discrete.html
.. _`Base.Relations.Properties`: https://ualib.org/src/Base.Relations.Properties.html
.. _`Base.Relations.Quotients`: https://ualib.org/src/Base.Relations.Quotients.html
.. _`Base.Structures`: https://ualib.org/src/Base.Structures.html
.. _`Base.Structures.Basic`: https://ualib.org/src/Base.Structures.Basic.html
.. _`Base.Structures.Congruences`: https://ualib.org/src/Base.Structures.Congruences.html
.. _`Base.Structures.EquationalLogic`: https://ualib.org/src/Base.Structures.EquationalLogic.html
.. _`Base.Structures.Graphs`: https://ualib.org/src/Base.Structures.Graphs.html
.. _`Base.Structures.Graphs0`: https://ualib.org/src/Base.Structures.Graphs0.html
.. _`Base.Structures.Homs`: https://ualib.org/src/Base.Structures.Homs.html
.. _`Base.Structures.Isos`: https://ualib.org/src/Base.Structures.Isos.html
.. _`Base.Structures.Products`: https://ualib.org/src/Base.Structures.Products.html
.. _`Base.Structures.Sigma`: https://ualib.org/src/Base.Structures.Sigma.html
.. _`Base.Structures.Sigma.Basic`: https://ualib.org/src/Base.Structures.Sigma.Basic.html
.. _`Base.Structures.Sigma.Congruences`: https://ualib.org/src/Base.Structures.Sigma.Congruences.html
.. _`Base.Structures.Sigma.Homs`: https://ualib.org/src/Base.Structures.Sigma.Homs.html
.. _`Base.Structures.Sigma.Isos`: https://ualib.org/src/Base.Structures.Sigma.Isos.html
.. _`Base.Structures.Sigma.Products`: https://ualib.org/src/Base.Structures.Sigma.Products.html
.. _`Base.Structures.Substructures`: https://ualib.org/src/Base.Structures.Substructures.html
.. _`Base.Structures.Terms`: https://ualib.org/src/Base.Structures.Terms.html
.. _`Base.Subalgebras`: https://ualib.org/src/Base.Subalgebras.html
.. _`Base.Subalgebras.Properties`: https://ualib.org/src/Base.Subalgebras.Properties.html
.. _`Base.Subalgebras.Subalgebras`: https://ualib.org/src/Base.Subalgebras.Subalgebras.html
.. _`Base.Subalgebras.Subuniverses`: https://ualib.org/src/Base.Subalgebras.Subuniverses.html
.. _`Base.Terms`: https://ualib.org/src/Base.Terms.html
.. _`Base.Terms.Basic`: https://ualib.org/src/Base.Terms.Basic.html
.. _`Base.Terms.Operations`: https://ualib.org/src/Base.Terms.Operations.html
.. _`Base.Terms.Properties`: https://ualib.org/src/Base.Terms.Properties.html
.. _`Base.Varieties`: https://ualib.org/src/Base.Varieties.html
.. _`Base.Varieties.Closure`: https://ualib.org/src/Base.Varieties.Closure.html
.. _`Base.Varieties.EquationalLogic`: https://ualib.org/src/Base.Varieties.EquationalLogic.html
.. _`Base.Varieties.FreeAlgebras`: https://ualib.org/src/Base.Varieties.FreeAlgebras.html
.. _`Base.Varieties.Invariants`: https://ualib.org/src/Base.Varieties.Invariants.html
.. _`Base.Varieties.Preservation`: https://ualib.org/src/Base.Varieties.Preservation.html
.. _`Base.Varieties.Properties`: https://ualib.org/src/Base.Varieties.Properties.html
.. _Demos: https://ualib.org/src/Demos.html
.. _`Demos.HSP`: https://ualib.org/src/Demos.HSP.html
.. _`Demos.HSP-markdown`: https://ualib.org/src/Demos.HSP-markdown.html
.. _Examples: https://ualib.org/src/Examples.html
.. _`Examples.Categories.Functors`: https://ualib.org/src/Examples.Categories.Functors.html
.. _`Examples.Structures`: https://ualib.org/src/Examples.Structures.html
.. _`Examples.Structures.Signatures`: https://ualib.org/src/Examples.Structures.Signatures.html
.. _`Exercises.Complexity.FiniteCSP`: https://ualib.org/src/Exercises.Complexity.FiniteCSP.html
.. _`Overture`: https://ualib.org/src/Overture.html
.. _`Overture.Preface`: https://ualib.org/src/Overture.Preface.html
.. _`Overture.Basic`: https://ualib.org/src/Overture.Basic.html
.. _`Overture.Levels`: https://ualib.org/src/Overture.Levels.html
.. _`Overture.Signatures`: https://ualib.org/src/Overture.Signatures.html
.. _`Overture.Operations`: https://ualib.org/src/Overture.Operations.html
.. _`Setoid`: https://ualib.org/src/Setoid.html
.. _`Setoid.Algebras`: https://ualib.org/src/Setoid.Algebras.html
.. _`Setoid.Algebras.Basic`: https://ualib.org/src/Setoid.Algebras.Basic.html
.. _`Setoid.Algebras.Congruences`: https://ualib.org/src/Setoid.Algebras.Congruences.html
.. _`Setoid.Algebras.Products`: https://ualib.org/src/Setoid.Algebras.Products.html
.. _`Setoid.Functions.Bijective`: https://ualib.org/src/Setoid.Functions.Bijective.html
.. _`Setoid.Functions.Injective`: https://ualib.org/src/Setoid.Functions.Injective.html
.. _`Setoid.Functions.Inverses`: https://ualib.org/src/Setoid.Functions.Inverses.html
.. _`Setoid.Functions.Preliminaries`: https://ualib.org/src/Setoid.Functions.Preliminaries.html
.. _`Setoid.Functions.Surjective`: https://ualib.org/src/Setoid.Functions.Surjective.html
.. _`Setoid.Homomorphisms`: https://ualib.org/src/Setoid.Homomorphisms.html
.. _`Setoid.Homomorphisms.Basic`: https://ualib.org/src/Setoid.Homomorphisms.Basic.html
.. _`Setoid.Homomorphisms.Factor`: https://ualib.org/src/Setoid.Homomorphisms.Factor.html
.. _`Setoid.Homomorphisms.HomomorphicImages`: https://ualib.org/src/Setoid.Homomorphisms.HomomorphicImages.html
.. _`Setoid.Homomorphisms.Isomorphisms`: https://ualib.org/src/Setoid.Homomorphisms.Isomorphisms.html
.. _`Setoid.Homomorphisms.Kernels`: https://ualib.org/src/Setoid.Homomorphisms.Kernels.html
.. _`Setoid.Homomorphisms.Noether`: https://ualib.org/src/Setoid.Homomorphisms.Noether.html
.. _`Setoid.Homomorphisms.Products`: https://ualib.org/src/Setoid.Homomorphisms.Products.html
.. _`Setoid.Homomorphisms.Properties`: https://ualib.org/src/Setoid.Homomorphisms.Properties.html
.. _`Setoid.Relations`: https://ualib.org/src/Setoid.Relations.html
.. _`Setoid.Relations.Discrete`: https://ualib.org/src/Setoid.Relations.Discrete.html
.. _`Setoid.Relations.Quotients`: https://ualib.org/src/Setoid.Relations.Quotients.html
.. _`Setoid.Subalgebras`: https://ualib.org/src/Setoid.Subalgebras.html
.. _`Setoid.Subalgebras.Properties`: https://ualib.org/src/Setoid.Subalgebras.Properties.html
.. _`Setoid.Subalgebras.Subalgebras`: https://ualib.org/src/Setoid.Subalgebras.Subalgebras.html
.. _`Setoid.Subalgebras.Subuniverses`: https://ualib.org/src/Setoid.Subalgebras.Subuniverses.html
.. _`Setoid.Terms`: https://ualib.org/src/Setoid.Terms.html
.. _`Setoid.Terms.Basic`: https://ualib.org/src/Setoid.Terms.Basic.html
.. _`Setoid.Terms.Operations`: https://ualib.org/src/Setoid.Terms.Operations.html
.. _`Setoid.Terms.Properties`: https://ualib.org/src/Setoid.Terms.Properties.html
.. _`Setoid.Varieties`: https://ualib.org/src/Setoid.Varieties.html
.. _`Setoid.Varieties.Closure`: https://ualib.org/src/Setoid.Varieties.Closure.html
.. _`Setoid.Varieties.EquationalLogic`: https://ualib.org/src/Setoid.Varieties.EquationalLogic.html
.. _`Setoid.Varieties.FreeAlgebras`: https://ualib.org/src/Setoid.Varieties.FreeAlgebras.html
.. _`Setoid.Varieties.HSP`: https://ualib.org/src/Setoid.Varieties.HSP.html
.. _`Setoid.Varieties.Preservation`: https://ualib.org/src/Setoid.Varieties.Preservation.html
.. _`Setoid.Varieties.Properties`: https://ualib.org/src/Setoid.Varieties.Properties.html
.. _`Setoid.Varieties.SoundAndComplete`: https://ualib.org/src/Setoid.Varieties.SoundAndComplete.html
.. _`Base.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base.lagda.rst
.. _`Base/Adjunction.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Adjunction.lagda.rst
.. _`Base/Adjunction/Closure.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Adjunction/Closure.lagda.rst
.. _`Base/Adjunction/Galois.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Adjunction/Galois.lagda.rst
.. _`Base/Adjunction/Residuation.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Adjunction/Residuation.lagda.rst
.. _`Base/Algebras.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Algebras.lagda.rst
.. _`Base/Algebras/Basic.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Algebras/Basic.lagda.rst
.. _`Base/Algebras/Congruences.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Algebras/Congruences.lagda.rst
.. _`Base/Algebras/Products.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Algebras/Products.lagda.rst
.. _`Base/Categories.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Categories.lagda.rst
.. _`Base/Categories/Functors.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Categories/Functors.lagda.rst
.. _`Base/Complexity.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Complexity.lagda.rst
.. _`Base/Complexity/Basic.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Complexity/Basic.lagda.rst
.. _`Base/Complexity/CSP.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Complexity/CSP.lagda.rst
.. _`Base/Equality.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Equality.lagda.rst
.. _`Base/Equality/Extensionality.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Equality/Extensionality.lagda.rst
.. _`Base/Equality/Truncation.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Equality/Truncation.lagda.rst
.. _`Base/Equality/Welldefined.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Equality/Welldefined.lagda.rst
.. _`Base/Homomorphisms.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Homomorphisms.lagda.rst
.. _`Base/Homomorphisms/Basic.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Homomorphisms/Basic.lagda.rst
.. _`Base/Homomorphisms/Factor.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Homomorphisms/Factor.lagda.rst
.. _`Base/Homomorphisms/HomomorphicImages.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Homomorphisms/HomomorphicImages.lagda.rst
.. _`Base/Homomorphisms/Isomorphisms.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Homomorphisms/Isomorphisms.lagda.rst
.. _`Base/Homomorphisms/Kernels.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Homomorphisms/Kernels.lagda.rst
.. _`Base/Homomorphisms/Noether.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Homomorphisms/Noether.lagda.rst
.. _`Base/Homomorphisms/Products.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Homomorphisms/Products.lagda.rst
.. _`Base/Homomorphisms/Properties.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Homomorphisms/Properties.lagda.rst
.. _`Base/Functions.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Functions.lagda.rst
.. _`Base/Functions/Injective.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Functions/Injective.lagda.rst
.. _`Base/Functions/Inverses.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Functions/Inverses.lagda.rst
.. _`Base/Functions/Preliminaries.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Functions/Preliminaries.lagda.rst
.. _`Base/Functions/Surjective.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Functions/Surjective.lagda.rst
.. _`Base/Functions/Transformers.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Functions/Transformers.lagda.rst
.. _`Base/Relations.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Relations.lagda.rst
.. _`Base/Relations/Continuous.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Relations/Continuous.lagda.rst
.. _`Base/Relations/Discrete.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Relations/Discrete.lagda.rst
.. _`Base/Relations/Properties.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Relations/Properties.lagda.rst
.. _`Base/Relations/Quotients.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Relations/Quotients.lagda.rst
.. _`Base/Structures.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures.lagda.rst
.. _`Base/Structures/Basic.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Basic.lagda.rst
.. _`Base/Structures/Congruences.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Congruences.lagda.rst
.. _`Base/Structures/EquationalLogic.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/EquationalLogic.lagda.rst
.. _`Base/Structures/Graphs.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Graphs.lagda.rst
.. _`Base/Structures/Graphs0.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Graphs0.lagda.rst
.. _`Base/Structures/Homs.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Homs.lagda.rst
.. _`Base/Structures/Isos.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Isos.lagda.rst
.. _`Base/Structures/Products.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Products.lagda.rst
.. _`Base/Structures/Sigma.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Sigma.lagda.rst
.. _`Base/Structures/Sigma/Basic.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Sigma/Basic.lagda.rst
.. _`Base/Structures/Sigma/Congruences.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Sigma/Congruences.lagda.rst
.. _`Base/Structures/Sigma/Homs.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Sigma/Homs.lagda.rst
.. _`Base/Structures/Sigma/Isos.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Sigma/Isos.lagda.rst
.. _`Base/Structures/Sigma/Products.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Sigma/Products.lagda.rst
.. _`Base/Structures/Substructures.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Substructures.lagda.rst
.. _`Base/Structures/Terms.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Terms.lagda.rst
.. _`Base/Subalgebras.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Subalgebras.lagda.rst
.. _`Base/Subalgebras/Properties.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Subalgebras/Properties.lagda.rst
.. _`Base/Subalgebras/Subalgebras.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Subalgebras/Subalgebras.lagda.rst
.. _`Base/Subalgebras/Subuniverses.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Subalgebras/Subuniverses.lagda.rst
.. _`Base/Terms.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Terms.lagda.rst
.. _`Base/Terms/Basic.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Terms/Basic.lagda.rst
.. _`Base/Terms/Operations.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Terms/Operations.lagda.rst
.. _`Base/Terms/Properties.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Terms/Properties.lagda.rst
.. _`Base/Varieties.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Varieties.lagda.rst
.. _`Base/Varieties/Closure.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Varieties/Closure.lagda.rst
.. _`Base/Varieties/EquationalLogic.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Varieties/EquationalLogic.lagda.rst
.. _`Base/Varieties/FreeAlgebras.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Varieties/FreeAlgebras.lagda.rst
.. _`Base/Varieties/Invariants.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Varieties/Invariants.lagda.rst
.. _`Base/Varieties/Preservation.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Varieties/Preservation.lagda.rst
.. _`Base/Varieties/Properties.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Varieties/Properties.lagda.rst
.. _`Demos.ContraX`: https://github.com/ualib/agda-algebras/blob/master/src/Demos/ContraX.lagda.rst
.. _`Demos/HSP.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Demos/HSP.lagda.rst
.. _`Examples/Categories/Functors.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Examples/Categories/Functors.lagda.rst
.. _`Examples/Structures/Basic.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Examples/Structures/Basic.lagda.rst
.. _`Examples/Structures/Signatures.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Examples/Structures/Signatures.lagda.rst
.. _`Exercises/Complexity/FiniteCSP.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Exercises/Complexity/FiniteCSP.lagda.rst
.. _`Overture.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Overture.labda.rst
.. _`Overture/Preface.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Overture/Preface.lagda.rst
.. _`Overture/Basic.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Overture/Basic.lagda.rst
.. _`Overture/Levels.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Overture/Levels.lagda.rst
.. _`Overture/Signatures.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Overture/Signatures.lagda.rst
.. _`Overture/Operations.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Overture/Operations.lagda.rst
.. _`Setoid.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid.lagda.rst
.. _`Setoid/Algebras.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Algebras.lagda.rst
.. _`Setoid/Algebras/Basic.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Algebras/Basic.lagda.rst
.. _`Setoid/Algebras/Congruences.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Algebras/Congruences.lagda.rst
.. _`Setoid/Algebras/Products.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Algebras/Products.lagda.rst
.. _`Setoid/Homomorphisms.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Homomorphisms.lagda.rst
.. _`Setoid/Homomorphisms/Basic.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Homomorphisms/Basic.lagda.rst
.. _`Setoid/Homomorphisms/Factor.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Homomorphisms/Factor.lagda.rst
.. _`Setoid/Homomorphisms/HomomorphicImages.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Homomorphisms/HomomorphicImages.lagda.rst
.. _`Setoid/Homomorphisms/Isomorphisms.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Homomorphisms/Isomorphisms.lagda.rst
.. _`Setoid/Homomorphisms/Kernels.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Homomorphisms/Kernels.lagda.rst
.. _`Setoid/Homomorphisms/Noether.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Homomorphisms/Noether.lagda.rst
.. _`Setoid/Homomorphisms/Products.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Homomorphisms/Products.lagda.rst
.. _`Setoid/Homomorphisms/Properties.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Homomorphisms/Properties.lagda.rst
.. _`Setoid/Functions.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Functions.lagda.rst
.. _`Setoid/Functions/Bijective.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Functions/Bijective.lagda.rst
.. _`Setoid/Functions/Injective.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Functions/Injective.lagda.rst
.. _`Setoid/Functions/Inverses.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Functions/Inverses.lagda.rst
.. _`Setoid/Functions/Preliminaries.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Functions/Preliminaries.lagda.rst
.. _`Setoid/Functions/Surjective.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Functions/Surjective.lagda.rst
.. _`Setoid/Relations.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Relations.lagda.rst
.. _`Setoid/Relations/Discrete.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Relations/Discrete.lagda.rst
.. _`Setoid/Relations/Quotients.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Relations/Quotients.lagda.rst
.. _`Setoid/Subalgebras.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Subalgebras.lagda.rst
.. _`Setoid/Subalgebras/Properties.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Subalgebras/Properties.lagda.rst
.. _`Setoid/Subalgebras/Subalgebras.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Subalgebras/Subalgebras.lagda.rst
.. _`Setoid/Subalgebras/Subuniverses.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Subalgebras/Subuniverses.lagda.rst
.. _`Setoid/Terms.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Terms.lagda.rst
.. _`Setoid/Terms/Basic.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Terms/Basic.lagda.rst
.. _`Setoid/Terms/Operations.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Terms/Operations.lagda.rst
.. _`Setoid/Terms/Properties.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Terms/Properties.lagda.rst
.. _`Setoid/Varieties.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Varieties.lagda.rst
.. _`Setoid/Varieties/Closure.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Varieties/Closure.lagda.rst
.. _`Setoid/Varieties/EquationalLogic.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Varieties/EquationalLogic.lagda.rst
.. _`Setoid/Varieties/FreeAlgebras.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Varieties/FreeAlgebras.lagda.rst
.. _`Setoid/Varieties/HSP.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Varieties/HSP.lagda.rst
.. _`Setoid/Varieties/Preservation.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Varieties/Preservation.lagda.rst
.. _`Setoid/Varieties/Properties.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Varieties/Properties.lagda.rst
.. _`Setoid/Varieties/SoundAndComplete.lagda.rst`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Varieties/SoundAndComplete.lagda.rst