Theorems · Definition · category theory

CategoryTheory.Bicategory.Pseudofunctor.ofOplaxFunctorToLocallyGroupoid

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

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

Defined in

Mathlib.CategoryTheory.Bicategory.LocallyGroupoid

Cited by

2 results in Mathlib

Foundations

Depth 12 from the axioms · uses Classical.choice

Assumes

CategoryTheory.BicategoryCategoryTheory.BicategoryCategoryTheory.Bicategory.IsLocallyGroupoid