Theorems · Theorem

CategoryTheory.Iso.hom_inv_id_apply

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (self : X ≅ Y) {F : C → C → Type uF}
  {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
  [inst_1 : CategoryTheory.ConcreteCategory C F] (x : carrier X),
  (CategoryTheory.ConcreteCategory.hom self.inv) ((CategoryTheory.ConcreteCategory.hom self.hom) x) = x

Defined in

Mathlib.CategoryTheory.Elementwise

Cited by

50 results in Mathlib

Foundations

Depth 7 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.ConcreteCategory