Theorems · Definition · category theory

CategoryTheory.ConcreteCategory.hom

{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} → (X ⟶ Y) → FC X Y

Convert a morphism of C to a bundled function.

Defined in

Mathlib.CategoryTheory.ConcreteCategory.Basic

Cited by

4,022 results in Mathlib

Foundations

Depth 4 from the axioms, rests on 11 definitions · uses no axioms

Assumes

CategoryTheory.ConcreteCategory