Theorems · Definition · category theory

CategoryTheory.Bicategory.Pseudofunctor.ofLaxFunctorToLocallyGroupoid

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

If B is a (2,1)-category, then every lax functor F from a bicategory to B defines a CategoryTheory.LaxFunctor.PseudoCore structure on F that can be used to promote F to a pseudofunctor using CategoryTheory.Pseudofunctor.mkOfLax.

Defined in

Mathlib.CategoryTheory.Bicategory.LocallyGroupoid

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.BicategoryCategoryTheory.BicategoryCategoryTheory.Bicategory.IsLocallyGroupoid