CT: Isomorphism

Summary

If two things are isomorphic, then for many intents and purposes they are the same.

Category Theory

In category theory, an isomorphism is a morphism which can be inverted. $f$

$$\forall c. \forall f : a \rightarrow b\quad g : b \rightarrow a. g \circ f = id$$

$$\forall c. \forall f : a \rightarrow b\quad g : b \rightarrow a. f \circ g = id$$

where $id$ is the identity morphism.

A pair of objects is isomorphic if an isomorphism exists between them. This practically means that objects which are isomorphic to each other are the same.

Isomorphism is the generalisation of the concept of bijection from the category Set to other categories.

In software, A pair of types with the same cardinality will always be isomorphic

Backlinks

• CT: Morphism
  • isomorphism
• A pair of types with the same cardinality will always be isomorphic
  • This is known as a bijection. Bijectivity is a more specific version of isomorphism, specific to Set - the category of all sets.
• Bijection
  • In the category of sets, Set, a bijection is a morphism which is both injective and surjective. In it's generalised form, this is isomorphism.
• A type is the same as another type if they share a normal form
  • In Pie, any two Types which share the same normal form are the same type. They are effectively isomorphic. Therefore
• An Isomorphism can be encoded with two functions
  • By providing a $\\text{to}$ and a $\\text{from}$ function it's possible to encode any isomorphism in a programming language. These functions should still follow the laws of left and right identity.
• Lenses can be seen as a bijection with some residual
  • A Lens a b is a bijection between $a$ and $(b, r)$, where $r$ is $a - b$. This represents a Lens as an isomorphism. Given $(b, r)$ one could construct $a$.