Theorems · Definition · category theory

CategoryTheory.Core.inclusionCompFunctorToCoreIso

{G : Type u₂} →
  [inst : CategoryTheory.Groupoid G] →
    (CategoryTheory.Core.inclusion G).comp (CategoryTheory.Core.functorToCore (CategoryTheory.Functor.id G)) ≅
      CategoryTheory.Functor.id (CategoryTheory.Core G)

The functor functorToCore (𝟭 G) is a section of inclusion G.

Defined in

Mathlib.CategoryTheory.Core

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Groupoid