Theorems · Definition · category theory

CategoryTheory.asIso

{C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.IsIso f] → X ≅ Y

Reinterpret a morphism f : X ⟶ Y with an IsIso f instance as X ≅ Y.

Defined in

Mathlib.CategoryTheory.Iso

Cited by

177 results in Mathlib

Foundations

Depth 10 from the axioms, rests on 53 definitions · uses Classical.choice

Assumes

CategoryTheory.CategoryCategoryTheory.IsIso