links.rst

.. _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-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
.. _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

.. _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
.. _`williamdemeo@gmail.com`: mailto:williamdemeo@gmail.com
.. _williamdemeo at gmail dot com: mailto:williamdemeo@gmail.com
.. _williamdemeo.org: https://williamdemeo.gitlab.io/
.. _`williamdemeo@gitlab`: https://gitlab.com/williamdemeo
.. _`williamdemeo@github`: https://github.com/williamdemeo



.. _`Base`: https://ualib.org/Base.html
.. _`Base.Adjunction`: https://ualib.org/Base.Adjunction.html
.. _`Base.Adjunction.Closure`: https://ualib.org/Base.Adjunction.Closure.html
.. _`Base.Adjunction.Galois`: https://ualib.org/Base.Adjunction.Galois.html
.. _`Base.Adjunction.Residuation`: https://ualib.org/Base.Adjunction.Residuation.html
.. _`Base.Algebras`: https://ualib.org/Base.Algebras.html
.. _`Base.Algebras.Basic`: https://ualib.org/Base.Algebras.Basic.html
.. _`Base.Algebras.Congruences`: https://ualib.org/Base.Algebras.Congruences.html
.. _`Base.Algebras.Products`: https://ualib.org/Base.Algebras.Products.html
.. _`Base.Categories`: https://ualib.org/Base.Categories.html
.. _`Base.Categories.Functors`: https://ualib.org/Base.Categories.Functors.html
.. _`Base.Complexity`: https://ualib.org/Base.Complexity.html
.. _`Base.Complexity.Basic`: https://ualib.org/Base.Complexity.Basic.html
.. _`Base.Complexity.CSP`: https://ualib.org/Base.Complexity.CSP.html
.. _`Base.Equality`: https://ualib.org/Base.Equality.html
.. _`Base.Equality.Extensionality`: https://ualib.org/Base.Equality.Extensionality.html
.. _`Base.Equality.Truncation`: https://ualib.org/Base.Equality.Truncation.html
.. _`Base.Equality.Welldefined`: https://ualib.org/Base.Equality.Welldefined.html
.. _`Base.Homomorphisms`: https://ualib.org/Base.Homomorphisms.html
.. _`Base.Homomorphisms.Basic`: https://ualib.org/Base.Homomorphisms.Basic.html
.. _`Base.Homomorphisms.Factor`: https://ualib.org/Base.Homomorphisms.Factor.html
.. _`Base.Homomorphisms.HomomorphicImages`: https://ualib.org/Base.Homomorphisms.HomomorphicImages.html
.. _`Base.Homomorphisms.Isomorphisms`: https://ualib.org/Base.Homomorphisms.Isomorphisms.html
.. _`Base.Homomorphisms.Kernels`: https://ualib.org/Base.Homomorphisms.Kernels.html
.. _`Base.Homomorphisms.Noether`: https://ualib.org/Base.Homomorphisms.Noether.html
.. _`Base.Homomorphisms.Products`: https://ualib.org/Base.Homomorphisms.Products.html
.. _`Base.Homomorphisms.Properties`: https://ualib.org/Base.Homomorphisms.Properties.html
.. _`Base.Overture`: https://ualib.org/Base.Overture.html
.. _`Base.Overture.Injective`: https://ualib.org/Base.Overture.Injective.html
.. _`Base.Overture.Inverses`: https://ualib.org/Base.Overture.Inverses.html
.. _`Base.Overture.Preliminaries`: https://ualib.org/Base.Overture.Preliminaries.html
.. _`Base.Overture.Surjective`: https://ualib.org/Base.Overture.Surjective.html
.. _`Base.Overture.Transformers`: https://ualib.org/Base.Overture.Transformers.html
.. _`Base.Relations`: https://ualib.org/Base.Relations.html
.. _`Base.Relations.Continuous`: https://ualib.org/Base.Relations.Continuous.html
.. _`Base.Relations.Discrete`: https://ualib.org/Base.Relations.Discrete.html
.. _`Base.Relations.Properties`: https://ualib.org/Base.Relations.Properties.html
.. _`Base.Relations.Quotients`: https://ualib.org/Base.Relations.Quotients.html
.. _`Base.Structures`: https://ualib.org/Base.Structures.html
.. _`Base.Structures.Basic`: https://ualib.org/Base.Structures.Basic.html
.. _`Base.Structures.Congruences`: https://ualib.org/Base.Structures.Congruences.html
.. _`Base.Structures.EquationalLogic`: https://ualib.org/Base.Structures.EquationalLogic.html
.. _`Base.Structures.Graphs`: https://ualib.org/Base.Structures.Graphs.html
.. _`Base.Structures.Graphs0`: https://ualib.org/Base.Structures.Graphs0.html
.. _`Base.Structures.Homs`: https://ualib.org/Base.Structures.Homs.html
.. _`Base.Structures.Isos`: https://ualib.org/Base.Structures.Isos.html
.. _`Base.Structures.Products`: https://ualib.org/Base.Structures.Products.html
.. _`Base.Structures.Sigma`: https://ualib.org/Base.Structures.Sigma.html
.. _`Base.Structures.Sigma.Basic`: https://ualib.org/Base.Structures.Sigma.Basic.html
.. _`Base.Structures.Sigma.Congruences`: https://ualib.org/Base.Structures.Sigma.Congruences.html
.. _`Base.Structures.Sigma.Homs`: https://ualib.org/Base.Structures.Sigma.Homs.html
.. _`Base.Structures.Sigma.Isos`: https://ualib.org/Base.Structures.Sigma.Isos.html
.. _`Base.Structures.Sigma.Products`: https://ualib.org/Base.Structures.Sigma.Products.html
.. _`Base.Structures.Substructures`: https://ualib.org/Base.Structures.Substructures.html
.. _`Base.Structures.Terms`: https://ualib.org/Base.Structures.Terms.html
.. _`Base.Subalgebras`: https://ualib.org/Base.Subalgebras.html
.. _`Base.Subalgebras.Properties`: https://ualib.org/Base.Subalgebras.Properties.html
.. _`Base.Subalgebras.Subalgebras`: https://ualib.org/Base.Subalgebras.Subalgebras.html
.. _`Base.Subalgebras.Subuniverses`: https://ualib.org/Base.Subalgebras.Subuniverses.html
.. _`Base.Terms`: https://ualib.org/Base.Terms.html
.. _`Base.Terms.Basic`: https://ualib.org/Base.Terms.Basic.html
.. _`Base.Terms.Operations`: https://ualib.org/Base.Terms.Operations.html
.. _`Base.Terms.Properties`: https://ualib.org/Base.Terms.Properties.html
.. _`Base.Varieties`: https://ualib.org/Base.Varieties.html
.. _`Base.Varieties.Closure`: https://ualib.org/Base.Varieties.Closure.html
.. _`Base.Varieties.EquationalLogic`: https://ualib.org/Base.Varieties.EquationalLogic.html
.. _`Base.Varieties.FreeAlgebras`: https://ualib.org/Base.Varieties.FreeAlgebras.html
.. _`Base.Varieties.Invariants`: https://ualib.org/Base.Varieties.Invariants.html
.. _`Base.Varieties.Preservation`: https://ualib.org/Base.Varieties.Preservation.html
.. _`Base.Varieties.Properties`: https://ualib.org/Base.Varieties.Properties.html
.. _`Demos.HSP`: https://ualib.org/Demos.HSP.html
.. _`Demos.HSP-markdown`: https://ualib.org/Demos.HSP-markdown.html
.. _`Examples.Categories.Functors`: https://ualib.org/Examples.Categories.Functors.html
.. _`Examples.Structures.Basic`: https://ualib.org/Examples.Structures.Basic.html
.. _`Examples.Structures.Signatures`: https://ualib.org/Examples.Structures.Signatures.html
.. _`Exercises.Complexity.FiniteCSP`: https://ualib.org/Exercises.Complexity.FiniteCSP.html
.. _`Preface`: https://ualib.org/Preface.html
.. _Setoid: https://ualib.org/Setoid.html
.. _`Setoid.Algebras`: https://ualib.org/Setoid.Algebras.html
.. _`Setoid.Algebras.Basic`: https://ualib.org/Setoid.Algebras.Basic.html
.. _`Setoid.Algebras.Congruences`: https://ualib.org/Setoid.Algebras.Congruences.html
.. _`Setoid.Algebras.Products`: https://ualib.org/Setoid.Algebras.Products.html
.. _`Setoid.Homomorphisms`: https://ualib.org/Setoid.Homomorphisms.html
.. _`Setoid.Homomorphisms.Basic`: https://ualib.org/Setoid.Homomorphisms.Basic.html
.. _`Setoid.Homomorphisms.Factor`: https://ualib.org/Setoid.Homomorphisms.Factor.html
.. _`Setoid.Homomorphisms.HomomorphicImages`: https://ualib.org/Setoid.Homomorphisms.HomomorphicImages.html
.. _`Setoid.Homomorphisms.Isomorphisms`: https://ualib.org/Setoid.Homomorphisms.Isomorphisms.html
.. _`Setoid.Homomorphisms.Kernels`: https://ualib.org/Setoid.Homomorphisms.Kernels.html
.. _`Setoid.Homomorphisms.Noether`: https://ualib.org/Setoid.Homomorphisms.Noether.html
.. _`Setoid.Homomorphisms.Products`: https://ualib.org/Setoid.Homomorphisms.Products.html
.. _`Setoid.Homomorphisms.Properties`: https://ualib.org/Setoid.Homomorphisms.Properties.html
.. _`Setoid.Overture`: https://ualib.org/Setoid.Overture.html
.. _`Setoid.Overture.Bijective`: https://ualib.org/Setoid.Overture.Bijective.html
.. _`Setoid.Overture.Injective`: https://ualib.org/Setoid.Overture.Injective.html
.. _`Setoid.Overture.Inverses`: https://ualib.org/Setoid.Overture.Inverses.html
.. _`Setoid.Overture.Preliminaries`: https://ualib.org/Setoid.Overture.Preliminaries.html
.. _`Setoid.Overture.Surjective`: https://ualib.org/Setoid.Overture.Surjective.html
.. _`Setoid.Relations`: https://ualib.org/Setoid.Relations.html
.. _`Setoid.Relations.Discrete`: https://ualib.org/Setoid.Relations.Discrete.html
.. _`Setoid.Relations.Quotients`: https://ualib.org/Setoid.Relations.Quotients.html
.. _`Setoid.Subalgebras`: https://ualib.org/Setoid.Subalgebras.html
.. _`Setoid.Subalgebras.Properties`: https://ualib.org/Setoid.Subalgebras.Properties.html
.. _`Setoid.Subalgebras.Subalgebras`: https://ualib.org/Setoid.Subalgebras.Subalgebras.html
.. _`Setoid.Subalgebras.Subuniverses`: https://ualib.org/Setoid.Subalgebras.Subuniverses.html
.. _`Setoid.Terms`: https://ualib.org/Setoid.Terms.html
.. _`Setoid.Terms.Basic`: https://ualib.org/Setoid.Terms.Basic.html
.. _`Setoid.Terms.Operations`: https://ualib.org/Setoid.Terms.Operations.html
.. _`Setoid.Terms.Properties`: https://ualib.org/Setoid.Terms.Properties.html
.. _`Setoid.Varieties`: https://ualib.org/Setoid.Varieties.html
.. _`Setoid.Varieties.Closure`: https://ualib.org/Setoid.Varieties.Closure.html
.. _`Setoid.Varieties.EquationalLogic`: https://ualib.org/Setoid.Varieties.EquationalLogic.html
.. _`Setoid.Varieties.FreeAlgebras`: https://ualib.org/Setoid.Varieties.FreeAlgebras.html
.. _`Setoid.Varieties.HSP`: https://ualib.org/Setoid.Varieties.HSP.html
.. _`Setoid.Varieties.Preservation`: https://ualib.org/Setoid.Varieties.Preservation.html
.. _`Setoid.Varieties.Properties`: https://ualib.org/Setoid.Varieties.Properties.html
.. _`Setoid.Varieties.SoundAndComplete`: https://ualib.org/Setoid.Varieties.SoundAndComplete.html

.. _`Base.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base.lagda
.. _`Base/Adjunction.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Adjunction.lagda
.. _`Base/Adjunction/Closure.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Adjunction/Closure.lagda
.. _`Base/Adjunction/Galois.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Adjunction/Galois.lagda
.. _`Base/Adjunction/Residuation.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Adjunction/Residuation.lagda
.. _`Base/Algebras.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Algebras.lagda
.. _`Base/Algebras/Basic.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Algebras/Basic.lagda
.. _`Base/Algebras/Congruences.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Algebras/Congruences.lagda
.. _`Base/Algebras/Products.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Algebras/Products.lagda
.. _`Base/Categories.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Categories.lagda
.. _`Base/Categories/Functors.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Categories/Functors.lagda
.. _`Base/Complexity.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Complexity.lagda
.. _`Base/Complexity/Basic.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Complexity/Basic.lagda
.. _`Base/Complexity/CSP.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Complexity/CSP.lagda
.. _`Base/Equality.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Equality.lagda
.. _`Base/Equality/Extensionality.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Equality/Extensionality.lagda
.. _`Base/Equality/Truncation.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Equality/Truncation.lagda
.. _`Base/Equality/Welldefined.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Equality/Welldefined.lagda
.. _`Base/Homomorphisms.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Homomorphisms.lagda
.. _`Base/Homomorphisms/Basic.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Homomorphisms/Basic.lagda
.. _`Base/Homomorphisms/Factor.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Homomorphisms/Factor.lagda
.. _`Base/Homomorphisms/HomomorphicImages.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Homomorphisms/HomomorphicImages.lagda
.. _`Base/Homomorphisms/Isomorphisms.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Homomorphisms/Isomorphisms.lagda
.. _`Base/Homomorphisms/Kernels.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Homomorphisms/Kernels.lagda
.. _`Base/Homomorphisms/Noether.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Homomorphisms/Noether.lagda
.. _`Base/Homomorphisms/Products.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Homomorphisms/Products.lagda
.. _`Base/Homomorphisms/Properties.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Homomorphisms/Properties.lagda
.. _`Base/Overture.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Overture.lagda
.. _`Base/Overture/Injective.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Overture/Injective.lagda
.. _`Base/Overture/Inverses.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Overture/Inverses.lagda
.. _`Base/Overture/Preliminaries.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Overture/Preliminaries.lagda
.. _`Base/Overture/Surjective.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Overture/Surjective.lagda
.. _`Base/Overture/Transformers.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Overture/Transformers.lagda
.. _`Base/Relations.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Relations.lagda
.. _`Base/Relations/Continuous.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Relations/Continuous.lagda
.. _`Base/Relations/Discrete.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Relations/Discrete.lagda
.. _`Base/Relations/Properties.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Relations/Properties.lagda
.. _`Base/Relations/Quotients.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Relations/Quotients.lagda
.. _`Base/Structures.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures.lagda
.. _`Base/Structures/Basic.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Basic.lagda
.. _`Base/Structures/Congruences.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Congruences.lagda
.. _`Base/Structures/EquationalLogic.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/EquationalLogic.lagda
.. _`Base/Structures/Graphs.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Graphs.lagda
.. _`Base/Structures/Graphs0.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Graphs0.lagda
.. _`Base/Structures/Homs.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Homs.lagda
.. _`Base/Structures/Isos.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Isos.lagda
.. _`Base/Structures/Products.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Products.lagda
.. _`Base/Structures/Sigma.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Sigma.lagda
.. _`Base/Structures/Sigma/Basic.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Sigma/Basic.lagda
.. _`Base/Structures/Sigma/Congruences.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Sigma/Congruences.lagda
.. _`Base/Structures/Sigma/Homs.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Sigma/Homs.lagda
.. _`Base/Structures/Sigma/Isos.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Sigma/Isos.lagda
.. _`Base/Structures/Sigma/Products.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Sigma/Products.lagda
.. _`Base/Structures/Substructures.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Substructures.lagda
.. _`Base/Structures/Terms.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Structures/Terms.lagda
.. _`Base/Subalgebras.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Subalgebras.lagda
.. _`Base/Subalgebras/Properties.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Subalgebras/Properties.lagda
.. _`Base/Subalgebras/Subalgebras.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Subalgebras/Subalgebras.lagda
.. _`Base/Subalgebras/Subuniverses.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Subalgebras/Subuniverses.lagda
.. _`Base/Terms.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Terms.lagda
.. _`Base/Terms/Basic.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Terms/Basic.lagda
.. _`Base/Terms/Operations.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Terms/Operations.lagda
.. _`Base/Terms/Properties.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Terms/Properties.lagda
.. _`Base/Varieties.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Varieties.lagda
.. _`Base/Varieties/Closure.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Varieties/Closure.lagda
.. _`Base/Varieties/EquationalLogic.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Varieties/EquationalLogic.lagda
.. _`Base/Varieties/FreeAlgebras.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Varieties/FreeAlgebras.lagda
.. _`Base/Varieties/Invariants.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Varieties/Invariants.lagda
.. _`Base/Varieties/Preservation.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Varieties/Preservation.lagda
.. _`Base/Varieties/Properties.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Base/Varieties/Properties.lagda
.. _`Demos/HSP.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Demos/HSP.lagda
.. _`Demos/HSP-markdown.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Demos/HSP/markdown.lagda
.. _`Examples/Categories/Functors.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Examples/Categories/Functors.lagda
.. _`Examples/Structures/Basic.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Examples/Structures/Basic.lagda
.. _`Examples/Structures/Signatures.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Examples/Structures/Signatures.lagda
.. _`Exercises/Complexity/FiniteCSP.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Exercises/Complexity/FiniteCSP.lagda
.. _`Preface.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Preface.lagda
.. _`Setoid.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid.lagda
.. _`Setoid/Algebras.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Algebras.lagda
.. _`Setoid/Algebras/Basic.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Algebras/Basic.lagda
.. _`Setoid/Algebras/Congruences.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Algebras/Congruences.lagda
.. _`Setoid/Algebras/Products.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Algebras/Products.lagda
.. _`Setoid/Homomorphisms.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Homomorphisms.lagda
.. _`Setoid/Homomorphisms/Basic.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Homomorphisms/Basic.lagda
.. _`Setoid/Homomorphisms/Factor.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Homomorphisms/Factor.lagda
.. _`Setoid/Homomorphisms/HomomorphicImages.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Homomorphisms/HomomorphicImages.lagda
.. _`Setoid/Homomorphisms/Isomorphisms.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Homomorphisms/Isomorphisms.lagda
.. _`Setoid/Homomorphisms/Kernels.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Homomorphisms/Kernels.lagda
.. _`Setoid/Homomorphisms/Noether.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Homomorphisms/Noether.lagda
.. _`Setoid/Homomorphisms/Products.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Homomorphisms/Products.lagda
.. _`Setoid/Homomorphisms/Properties.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Homomorphisms/Properties.lagda
.. _`Setoid/Overture.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Overture.lagda
.. _`Setoid/Overture/Bijective.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Overture/Bijective.lagda
.. _`Setoid/Overture/Injective.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Overture/Injective.lagda
.. _`Setoid/Overture/Inverses.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Overture/Inverses.lagda
.. _`Setoid/Overture/Preliminaries.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Overture/Preliminaries.lagda
.. _`Setoid/Overture/Surjective.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Overture/Surjective.lagda
.. _`Setoid/Relations.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Relations.lagda
.. _`Setoid/Relations/Discrete.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Relations/Discrete.lagda
.. _`Setoid/Relations/Quotients.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Relations/Quotients.lagda
.. _`Setoid/Subalgebras.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Subalgebras.lagda
.. _`Setoid/Subalgebras/Properties.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Subalgebras/Properties.lagda
.. _`Setoid/Subalgebras/Subalgebras.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Subalgebras/Subalgebras.lagda
.. _`Setoid/Subalgebras/Subuniverses.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Subalgebras/Subuniverses.lagda
.. _`Setoid/Terms.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Terms.lagda
.. _`Setoid/Terms/Basic.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Terms/Basic.lagda
.. _`Setoid/Terms/Operations.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Terms/Operations.lagda
.. _`Setoid/Terms/Properties.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Terms/Properties.lagda
.. _`Setoid/Varieties.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Varieties.lagda
.. _`Setoid/Varieties/Closure.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Varieties/Closure.lagda
.. _`Setoid/Varieties/EquationalLogic.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Varieties/EquationalLogic.lagda
.. _`Setoid/Varieties/FreeAlgebras.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Varieties/FreeAlgebras.lagda
.. _`Setoid/Varieties/HSP.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Varieties/HSP.lagda
.. _`Setoid/Varieties/Preservation.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Varieties/Preservation.lagda
.. _`Setoid/Varieties/Properties.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Varieties/Properties.lagda
.. _`Setoid/Varieties/SoundAndComplete.lagda`: https://github.com/ualib/agda-algebras/blob/master/src/Setoid/Varieties/SoundAndComplete.lagda