Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
A setoid is a collection of things (which could be a set, a type, or a preset depending on the chosen foundations) equipped with an equivalence relation or a pseudo-equivalence relation. Setoids are commonly used in “impoverished” foundations of mathematics that lack a primitive notion of quotient; see for instance Bishop set.
Last revised on September 20, 2021 at 06:44:07. See the history of this page for a list of all contributions to it.