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).
Given sets and , a function is a bijection if it comes with an inverse function such that for all elements , and for all elements , if , then
The condition that could also be made more general, by any element such that . This then becomes
This could be simplified down to the statement that if and only if .
This is an adjoint equivalence between two thin univalent groupoids.
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 January 7, 2023 at 05:48:28. See the history of this page for a list of all contributions to it.