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
An extensional function is a functor between setoids (thin groupoids).
There are multiple inequivalent notions of extensional function in type theory.
An extensional function is a function $f:A \to B$ between setoids $A$ and $B$ such that for all terms $a:A$ and $b:A$, $p:(a \equiv_A b) \to (f(a) \equiv_B f(b))$.
An extensional function is a function $f:A \to B$ between types $A$ and $B$ such that for all terms $a:A$ and $b:A$, $p:(a =_A b) \to (f(a) =_B f(b))$.
If there exists an interval type, then every function is an extensional function.
Created on May 3, 2022 at 19:39:38. See the history of this page for a list of all contributions to it.