Iso.idr

The Category of Isomorphisms

Isomorphisms form a category where the objects are types, just like $\mathcal{S}et$ \defref{def:set-cat} but the morphisms are not function but isomorphisms \defref{def:iso}. The identity is given by the identity isomorphism, and the composition by transitivity of isomorphisms. In a sense, the category $\mathcal{S}et$ is a sub-category of $\mathcal{I}so$ where only the “to” map is kept and everything else is thrown away.

Proposition

Isomorphisms form a category $\mathcal{I}so$.

IsoCat : Category Type
IsoCat = NewCat
  { objects = Type
  , morphisms = (≅)
  , identity = (\x => Iso.identity _)
  , composition = transIso
  , identity_right = (\x => fromIsoEq _ _ (isoIdRight x))
  , identity_left = (\x => fromIsoEq _ _ (isoIdLeft x))
  , compose_assoc = (\x, y, z => fromIsoEq _ _ (transIsoAssoc x y z))
  }