Theorems · Definition · category theory

CategoryTheory.OplaxFunctor.PseudoCore.mapIdIso

{B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F : CategoryTheory.OplaxFunctor B C} →
          F.PseudoCore →
            (a : B) → F.map (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id (F.obj a)

The isomorphism giving rise to the oplax unity constraint

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Cited by

3 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.BicategoryCategoryTheory.Bicategory