Theorems · Theorem · order theory

PartOrd.forget_map

Deprecated since 2026-02-16Use CategoryTheory.ConcreteCategory.forget_map_eq_ofHom instead.

∀ {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)

Alias of CategoryTheory.ConcreteCategory.forget_map_eq_ofHom.

Defined in

Mathlib.Order.Category.PartOrd

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryoutParamCategoryTheory.ConcreteCategory