Theorems · Inductive type · category theory

CategoryTheory.Iso

{C : Type u} → [CategoryTheory.Category.{v, u} C] → C → C → Type v

An isomorphism (a.k.a. an invertible morphism) between two objects of a category. The inverse morphism is bundled. See also CategoryTheory.Core for the category with the same objects and isomorphisms playing the role of morphisms.

Defined in

Mathlib.CategoryTheory.Iso

Cited by

3,963 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

CategoryTheory.Category