Theorems · Theorem · category theory

CategoryTheory.ConcreteCategory.hom_ofHom

∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {FC : outParam (C → C → Type u_1)} {CC : outParam (C → Type w)}
  {inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))} [self : CategoryTheory.ConcreteCategory C FC]
  {X Y : C} (f : FC X Y), CategoryTheory.ConcreteCategory.hom (CategoryTheory.ConcreteCategory.ofHom f) = f

Defined in

Mathlib.CategoryTheory.ConcreteCategory.Basic

Cited by

205 results in Mathlib

Foundations

Depth 5 from the axioms, rests on 13 definitions · uses no axioms

Assumes

CategoryTheory.ConcreteCategory