Theorems · Definition · category theory

CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory

{B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat} →
      (P : F.ObjectProperty) → [P.IsClosedUnderMapObj] → CategoryTheory.Pseudofunctor B CategoryTheory.Cat

Given a property of objects P for a pseudofunctor from B to Cat, this is the induced pseudofunctor which sends X : B to the full subcategory of F.obj X consisting of objects satisfying P.

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty

Cited by

7 results in Mathlib

Foundations

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

Assumes

CategoryTheory.BicategoryCategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderMapObj