Theorems · Definition · category theory

CategoryTheory.Discrete.natIsoFunctor

{C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {I : Type u₁} →
      {F : CategoryTheory.Functor (CategoryTheory.Discrete I) C} →
        F ≅ CategoryTheory.Discrete.functor (F.obj ∘ CategoryTheory.Discrete.mk)

Every functor F from a discrete category is naturally isomorphic (actually, equal) to Discrete.functor (F.obj).

Defined in

Mathlib.CategoryTheory.Discrete.Basic

Cited by

11 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category