Theorems · Definition · category theory

CategoryTheory.Discrete.functor

{C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {I : Type u₁} → (I → C) → CategoryTheory.Functor (CategoryTheory.Discrete I) C

Any function I → C gives a functor Discrete I ⥤ C.

Defined in

Mathlib.CategoryTheory.Discrete.Basic

Cited by

633 results in Mathlib

Foundations

Depth 12 from the axioms, rests on 69 definitions · uses propext

Assumes

CategoryTheory.Category