Theorems · Definition · category theory

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

Convert a bundled function to a morphism of C.

Defined in

Mathlib.CategoryTheory.ConcreteCategory.Basic

Cited by

18 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.ConcreteCategory