A **bijection** is an isomorphism in Set.

Since Set is a balanced category, bijections can also be characterized as functions which are both injective (monic) and surjective (epic).

In older literature, a bijection may be called a **one-to-one correspondence**, or (as a compromise) **bijective correspondence**.

**computational trinitarianism** =

**propositions as types** +**programs as proofs** +**relation type theory/category theory**

Last revised on October 16, 2022 at 03:09:27. See the history of this page for a list of all contributions to it.