Theorems · Theorem · category theory

CategoryTheory.ConcreteCategory.forget_map_eq_ofHom

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.forget C).map f = TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom f)

Defined in

Mathlib.CategoryTheory.ConcreteCategory.Forget

Cited by

13 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryoutParamCategoryTheory.ConcreteCategory