Theorems · Definition · category theory

CategoryTheory.Pseudofunctor.ObjectProperty.mapComp

{B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat} →
      (P : F.ObjectProperty) →
        [inst_1 : P.IsClosedUnderMapObj] →
          {X Y Z : B} →
            (f : X ⟶ Y) → (g : Y ⟶ Z) → P.map (CategoryTheory.CategoryStruct.comp f g) ≅ (P.map f).comp (P.map g)

Auxiliary definition for fullsubcategory.

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.BicategoryCategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderMapObj