Isomorphisms

This file defines isomorphisms between objects of a category.

Main definitions

• structure iso : a bundled isomorphism between two objects of a category;
• class is_iso : an unbundled version of iso; note that is_iso f is usually not a Prop, because it holds the inverse morphism;
• as_iso : convert from is_iso to iso;
• of_iso : convert from iso to is_iso;
• standard operations on isomorphisms (composition, inverse etc)

Notations

• X ≅ Y : same as iso X Y;
• α ≪≫ β : composition of two isomorphisms; it is called iso.trans

Tags

category, category theory, isomorphism