Theorems · Inductive type · category theory

CategoryTheory.IsIso

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

The IsIso typeclass expresses that a morphism is invertible. Given a morphism f with IsIso f, one can view f as an isomorphism via asIso f and get the inverse using inv f.

Defined in

Mathlib.CategoryTheory.Iso

Cited by

1,156 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category