Theorems · Definition · category theory

CategoryTheory.Bicategory.Pith.pseudofunctorToPith

{B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {B' : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory B'] →
        [CategoryTheory.Bicategory.IsLocallyGroupoid B'] →
          CategoryTheory.Pseudofunctor B' B → CategoryTheory.Pseudofunctor B' (CategoryTheory.Bicategory.Pith B)

Any pseudofunctor from a (2,1)-category to a bicategory factors through the pith of the target bicategory.

Defined in

Mathlib.CategoryTheory.Bicategory.LocallyGroupoid

Cited by

10 results in Mathlib

Foundations

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

Assumes

CategoryTheory.BicategoryCategoryTheory.BicategoryCategoryTheory.Bicategory.IsLocallyGroupoid