Documentation

Mathlib.CategoryTheory.Bicategory.Functor

Oplax functors and pseudofunctors #

An oplax functor F between bicategories B and C consists of

A pseudofunctor is an oplax functor whose mapId and mapComp are isomorphisms. We provide several constructors for pseudofunctors:

The additional constructors are useful when constructing a pseudofunctor where the construction of the oplax functor associated with it is already done. For example, the composition of pseudofunctors can be defined by using the composition of oplax functors as follows:

def comp (F : Pseudofunctor B C) (G : Pseudofunctor C D) : Pseudofunctor B D :=
  mkOfOplax ((F : OplaxFunctor B C).comp G)
  { mapIdIso := λ a => (G.mapFunctor _ _).mapIso (F.mapId a) ≪≫ G.mapId (F.obj a),
    mapCompIso := λ f g =>
      (G.mapFunctor _ _).mapIso (F.mapComp f g) ≪≫ G.mapComp (F.map f) (F.map g) }

although the composition of pseudofunctors in this file is defined by using the default constructor because obviously wasn't smart enough in mathlib3 and the porter of this file was too lazy to investigate this issue further in mathlib4. Similarly, the composition is also defined by using mkOfOplax' after giving appropriate instances for IsIso. The former constructor mkOfOplax requires isomorphisms as data type Iso, and so it is useful if you don't want to forget the definitions of the inverses. On the other hand, the latter constructor mkOfOplax' is useful if you want to use propositional type class IsIso.

Main definitions #

Future work #

There are two types of functors between bicategories, called lax and oplax functors, depending on the directions of mapId and mapComp. We may need both in mathlib in the future, but for now we only define oplax functors.

source
structure CategoryTheory.PrelaxFunctor (B : Type u₁) [Quiver B] [(a b : B) → Quiver (a ⟶ b)] (C : Type u₂) [Quiver C] [(a b : C) → Quiver (a ⟶ b)] extends Prefunctor :
Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)
  • obj : B → C
  • map : {X Y : B} → (X ⟶ Y) → ((↑s).obj X ⟶ (↑s).obj Y)
  • map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → ((↑s).map f ⟶ (↑s).map g)

    The action of a prelax functor on 2-morphisms.

A prelax functor between bicategories consists of functions between objects, 1-morphisms, and 2-morphisms. This structure will be extended to define OplaxFunctor.

Instances For
    source
    instance CategoryTheory.PrelaxFunctor.hasCoeToPrefunctor {B : Type u₁} [Quiver B] [(a b : B) → Quiver (a ⟶ b)] {C : Type u₂} [Quiver C] [(a b : C) → Quiver (a ⟶ b)] :
    Coe (CategoryTheory.PrelaxFunctor B C) (B ⥤q C)
    source
    @[simp]
    theorem CategoryTheory.PrelaxFunctor.id_toPrefunctor_map (B : Type u₁) [Quiver B] [(a b : B) → Quiver (a ⟶ b)] :
    ∀ {X Y : B} (a : X ⟶ Y), (↑(CategoryTheory.PrelaxFunctor.id B)).map a = (𝟭q B).map a
    source
    @[simp]
    theorem CategoryTheory.PrelaxFunctor.id_map₂ (B : Type u₁) [Quiver B] [(a b : B) → Quiver (a ⟶ b)] :
    ∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g), CategoryTheory.PrelaxFunctor.map₂ (CategoryTheory.PrelaxFunctor.id B) η = η
    source
    @[simp]
    theorem CategoryTheory.PrelaxFunctor.id_toPrefunctor_obj (B : Type u₁) [Quiver B] [(a b : B) → Quiver (a ⟶ b)] :
    ∀ (a : B), (↑(CategoryTheory.PrelaxFunctor.id B)).obj a = (𝟭q B).obj a
    source
    def CategoryTheory.PrelaxFunctor.id (B : Type u₁) [Quiver B] [(a b : B) → Quiver (a ⟶ b)] :
    CategoryTheory.PrelaxFunctor B B

    The identity prelax functor.

    Instances For
      source
      instance CategoryTheory.PrelaxFunctor.instInhabitedPrelaxFunctor {B : Type u₁} [Quiver B] [(a b : B) → Quiver (a ⟶ b)] :
      Inhabited (CategoryTheory.PrelaxFunctor B B)
      source
      @[simp]
      theorem CategoryTheory.PrelaxFunctor.comp_toPrefunctor_map {B : Type u₁} [Quiver B] [(a b : B) → Quiver (a ⟶ b)] {C : Type u₂} [Quiver C] [(a b : C) → Quiver (a ⟶ b)] {D : Type u₃} [Quiver D] [(a b : D) → Quiver (a ⟶ b)] (F : CategoryTheory.PrelaxFunctor B C) (G : CategoryTheory.PrelaxFunctor C D) :
      ∀ {X Y : B} (a : X ⟶ Y), (↑(CategoryTheory.PrelaxFunctor.comp F G)).map a = (↑F ⋙q ↑G).map a
      source
      @[simp]
      theorem CategoryTheory.PrelaxFunctor.comp_toPrefunctor_obj {B : Type u₁} [Quiver B] [(a b : B) → Quiver (a ⟶ b)] {C : Type u₂} [Quiver C] [(a b : C) → Quiver (a ⟶ b)] {D : Type u₃} [Quiver D] [(a b : D) → Quiver (a ⟶ b)] (F : CategoryTheory.PrelaxFunctor B C) (G : CategoryTheory.PrelaxFunctor C D) :
      ∀ (a : B), (↑(CategoryTheory.PrelaxFunctor.comp F G)).obj a = (↑F ⋙q ↑G).obj a
      source
      @[simp]
      theorem CategoryTheory.PrelaxFunctor.comp_map₂ {B : Type u₁} [Quiver B] [(a b : B) → Quiver (a ⟶ b)] {C : Type u₂} [Quiver C] [(a b : C) → Quiver (a ⟶ b)] {D : Type u₃} [Quiver D] [(a b : D) → Quiver (a ⟶ b)] (F : CategoryTheory.PrelaxFunctor B C) (G : CategoryTheory.PrelaxFunctor C D) :
      ∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g), CategoryTheory.PrelaxFunctor.map₂ (CategoryTheory.PrelaxFunctor.comp F G) η = CategoryTheory.PrelaxFunctor.map₂ G (CategoryTheory.PrelaxFunctor.map₂ F η)
      source
      def CategoryTheory.PrelaxFunctor.comp {B : Type u₁} [Quiver B] [(a b : B) → Quiver (a ⟶ b)] {C : Type u₂} [Quiver C] [(a b : C) → Quiver (a ⟶ b)] {D : Type u₃} [Quiver D] [(a b : D) → Quiver (a ⟶ b)] (F : CategoryTheory.PrelaxFunctor B C) (G : CategoryTheory.PrelaxFunctor C D) :
      CategoryTheory.PrelaxFunctor B D

      Composition of prelax functors.

      Instances For
        source
        structure CategoryTheory.OplaxFunctor (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] extends CategoryTheory.PrelaxFunctor :
        Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)

        An oplax functor F between bicategories B and C consists of a function between objects F.obj, a function between 1-morphisms F.map, and a function between 2-morphisms F.map₂.

        Unlike functors between categories, F.map do not need to strictly commute with the composition, and do not need to strictly preserve the identity. Instead, there are specified 2-morphisms F.map (𝟙 a) ⟶ 𝟙 (F.obj a) and F.map (f ≫ g) ⟶ F.map f ≫ F.map g.

        F.map₂ strictly commute with compositions and preserve the identity. They also preserve the associator, the left unitor, and the right unitor modulo some adjustments of domains and codomains of 2-morphisms.

        Instances For
          source
          @[simp]
          theorem CategoryTheory.OplaxFunctor.map₂_associator_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) {Z : (↑self.toPrelaxFunctor).obj a ⟶ (↑self.toPrelaxFunctor).obj d} (h : CategoryTheory.CategoryStruct.comp ((↑self.toPrelaxFunctor).map f) (CategoryTheory.CategoryStruct.comp ((↑self.toPrelaxFunctor).map g) ((↑self.toPrelaxFunctor).map h)) ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.PrelaxFunctor.map₂ self.toPrelaxFunctor (CategoryTheory.Bicategory.associator f g h).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.OplaxFunctor.mapComp self f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((↑self.toPrelaxFunctor).map f) (CategoryTheory.OplaxFunctor.mapComp self g h)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.OplaxFunctor.mapComp self (CategoryTheory.CategoryStruct.comp f g) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxFunctor.mapComp self f g) ((↑self.toPrelaxFunctor).map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator ((↑self.toPrelaxFunctor).map f) ((↑self.toPrelaxFunctor).map g) ((↑self.toPrelaxFunctor).map h)).hom h))
          source
          @[simp]
          theorem CategoryTheory.OplaxFunctor.mapComp_naturality_left_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} {c : B} {f : a ⟶ b} {f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) {Z : (↑self.toPrelaxFunctor).obj a ⟶ (↑self.toPrelaxFunctor).obj c} (h : CategoryTheory.CategoryStruct.comp ((↑self.toPrelaxFunctor).map f') ((↑self.toPrelaxFunctor).map g) ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.PrelaxFunctor.map₂ self.toPrelaxFunctor (CategoryTheory.Bicategory.whiskerRight η g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.OplaxFunctor.mapComp self f' g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.OplaxFunctor.mapComp self f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.PrelaxFunctor.map₂ self.toPrelaxFunctor η) ((↑self.toPrelaxFunctor).map g)) h)
          source
          @[simp]
          theorem CategoryTheory.OplaxFunctor.mapComp_naturality_right_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} {c : B} (f : a ⟶ b) {g : b ⟶ c} {g' : b ⟶ c} (η : g ⟶ g') {Z : (↑self.toPrelaxFunctor).obj a ⟶ (↑self.toPrelaxFunctor).obj c} (h : CategoryTheory.CategoryStruct.comp ((↑self.toPrelaxFunctor).map f) ((↑self.toPrelaxFunctor).map g') ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.PrelaxFunctor.map₂ self.toPrelaxFunctor (CategoryTheory.Bicategory.whiskerLeft f η)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.OplaxFunctor.mapComp self f g') h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.OplaxFunctor.mapComp self f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((↑self.toPrelaxFunctor).map f) (CategoryTheory.PrelaxFunctor.map₂ self.toPrelaxFunctor η)) h)
          source
          theorem CategoryTheory.OplaxFunctor.map₂_rightUnitor_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} (f : a ⟶ b) {Z : (↑self.toPrelaxFunctor).obj a ⟶ (↑self.toPrelaxFunctor).obj b} (h : (↑self.toPrelaxFunctor).map f ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.PrelaxFunctor.map₂ self.toPrelaxFunctor (CategoryTheory.Bicategory.rightUnitor f).hom) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.OplaxFunctor.mapComp self f (CategoryTheory.CategoryStruct.id b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((↑self.toPrelaxFunctor).map f) (CategoryTheory.OplaxFunctor.mapId self b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor ((↑self.toPrelaxFunctor).map f)).hom h))
          source
          theorem CategoryTheory.OplaxFunctor.map₂_leftUnitor_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} (f : a ⟶ b) {Z : (↑self.toPrelaxFunctor).obj a ⟶ (↑self.toPrelaxFunctor).obj b} (h : (↑self.toPrelaxFunctor).map f ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.PrelaxFunctor.map₂ self.toPrelaxFunctor (CategoryTheory.Bicategory.leftUnitor f).hom) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.OplaxFunctor.mapComp self (CategoryTheory.CategoryStruct.id a) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.OplaxFunctor.mapId self a) ((↑self.toPrelaxFunctor).map f)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor ((↑self.toPrelaxFunctor).map f)).hom h))
          source
          theorem CategoryTheory.OplaxFunctor.map₂_comp_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} {h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) {Z : (↑self.toPrelaxFunctor).obj a ⟶ (↑self.toPrelaxFunctor).obj b} (h : (↑self.toPrelaxFunctor).map h ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.PrelaxFunctor.map₂ self.toPrelaxFunctor (CategoryTheory.CategoryStruct.comp η θ)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.PrelaxFunctor.map₂ self.toPrelaxFunctor η) (CategoryTheory.CategoryStruct.comp (CategoryTheory.PrelaxFunctor.map₂ self.toPrelaxFunctor θ) h)
          source
          instance CategoryTheory.OplaxFunctor.hasCoeToPrelax {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] :
          Coe (CategoryTheory.OplaxFunctor B C) (CategoryTheory.PrelaxFunctor B C)
          source
          @[simp]
          theorem CategoryTheory.OplaxFunctor.mapFunctor_obj {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (a : B) (b : B) (f : a ⟶ b) :
          (CategoryTheory.OplaxFunctor.mapFunctor F a b).obj f = (↑F.toPrelaxFunctor).map f
          source
          @[simp]
          theorem CategoryTheory.OplaxFunctor.mapFunctor_map {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (a : B) (b : B) :
          ∀ {X Y : a ⟶ b} (η : X ⟶ Y), (CategoryTheory.OplaxFunctor.mapFunctor F a b).map η = CategoryTheory.PrelaxFunctor.map₂ F.toPrelaxFunctor η
          source
          def CategoryTheory.OplaxFunctor.mapFunctor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (a : B) (b : B) :
          CategoryTheory.Functor (a ⟶ b) ((↑F.toPrelaxFunctor).obj a ⟶ (↑F.toPrelaxFunctor).obj b)

          Function between 1-morphisms as a functor.

          Instances For
            source
            @[simp]
            theorem CategoryTheory.OplaxFunctor.id_mapId (B : Type u₁) [CategoryTheory.Bicategory B] (a : B) :
            CategoryTheory.OplaxFunctor.mapId (CategoryTheory.OplaxFunctor.id B) a = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id a)
            source
            @[simp]
            theorem CategoryTheory.OplaxFunctor.id_toPrelaxFunctor_toPrefunctor (B : Type u₁) [CategoryTheory.Bicategory B] :
            ↑(CategoryTheory.OplaxFunctor.id B).toPrelaxFunctor = ↑(CategoryTheory.PrelaxFunctor.id B)
            source
            @[simp]
            theorem CategoryTheory.OplaxFunctor.id_toPrelaxFunctor_map₂ (B : Type u₁) [CategoryTheory.Bicategory B] :
            ∀ {a b : B} {f g : a ⟶ b} (a_1 : f ⟶ g), CategoryTheory.PrelaxFunctor.map₂ (CategoryTheory.OplaxFunctor.id B).toPrelaxFunctor a_1 = CategoryTheory.PrelaxFunctor.map₂ (CategoryTheory.PrelaxFunctor.id B) a_1
            source
            @[simp]
            theorem CategoryTheory.OplaxFunctor.id_mapComp (B : Type u₁) [CategoryTheory.Bicategory B] :
            ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.OplaxFunctor.mapComp (CategoryTheory.OplaxFunctor.id B) f g = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)
            source
            def CategoryTheory.OplaxFunctor.id (B : Type u₁) [CategoryTheory.Bicategory B] :
            CategoryTheory.OplaxFunctor B B

            The identity oplax functor.

            Instances For
              source
              instance CategoryTheory.OplaxFunctor.instInhabitedOplaxFunctor {B : Type u₁} [CategoryTheory.Bicategory B] :
              Inhabited (CategoryTheory.OplaxFunctor B B)
              source
              def CategoryTheory.OplaxFunctor.comp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {D : Type u₃} [CategoryTheory.Bicategory D] (F : CategoryTheory.OplaxFunctor B C) (G : CategoryTheory.OplaxFunctor C D) :
              CategoryTheory.OplaxFunctor B D

              Composition of oplax functors.

              Instances For
                source
                structure CategoryTheory.OplaxFunctor.PseudoCore {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) :
                Type (max (max u₁ v₁) w₂)

                A structure on an oplax functor that promotes an oplax functor to a pseudofunctor. See Pseudofunctor.mkOfOplax.

                Instances For
                  source
                  structure CategoryTheory.Pseudofunctor (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] extends CategoryTheory.PrelaxFunctor :
                  Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)

                  A pseudofunctor F between bicategories B and C consists of a function between objects F.obj, a function between 1-morphisms F.map, and a function between 2-morphisms F.map₂.

                  Unlike functors between categories, F.map do not need to strictly commute with the compositions, and do not need to strictly preserve the identity. Instead, there are specified 2-isomorphisms F.map (𝟙 a) ≅ 𝟙 (F.obj a) and F.map (f ≫ g) ≅ F.map f ≫ F.map g.

                  F.map₂ strictly commute with compositions and preserve the identity. They also preserve the associator, the left unitor, and the right unitor modulo some adjustments of domains and codomains of 2-morphisms.

                  Instances For
                    source
                    theorem CategoryTheory.Pseudofunctor.map₂_right_unitor_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} (f : a ⟶ b) {Z : (↑self.toPrelaxFunctor).obj a ⟶ (↑self.toPrelaxFunctor).obj b} (h : (↑self.toPrelaxFunctor).map f ⟶ Z) :
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.PrelaxFunctor.map₂ self.toPrelaxFunctor (CategoryTheory.Bicategory.rightUnitor f).hom) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.mapComp self f (CategoryTheory.CategoryStruct.id b)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((↑self.toPrelaxFunctor).map f) (CategoryTheory.Pseudofunctor.mapId self b).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor ((↑self.toPrelaxFunctor).map f)).hom h))
                    source
                    theorem CategoryTheory.Pseudofunctor.map₂_comp_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} {h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) {Z : (↑self.toPrelaxFunctor).obj a ⟶ (↑self.toPrelaxFunctor).obj b} (h : (↑self.toPrelaxFunctor).map h ⟶ Z) :
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.PrelaxFunctor.map₂ self.toPrelaxFunctor (CategoryTheory.CategoryStruct.comp η θ)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.PrelaxFunctor.map₂ self.toPrelaxFunctor η) (CategoryTheory.CategoryStruct.comp (CategoryTheory.PrelaxFunctor.map₂ self.toPrelaxFunctor θ) h)
                    source
                    theorem CategoryTheory.Pseudofunctor.map₂_whisker_right_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} {c : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) {Z : (↑self.toPrelaxFunctor).obj a ⟶ (↑self.toPrelaxFunctor).obj c} (h : (↑self.toPrelaxFunctor).map (CategoryTheory.CategoryStruct.comp g h) ⟶ Z) :
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.PrelaxFunctor.map₂ self.toPrelaxFunctor (CategoryTheory.Bicategory.whiskerRight η h)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.mapComp self f h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.PrelaxFunctor.map₂ self.toPrelaxFunctor η) ((↑self.toPrelaxFunctor).map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.mapComp self g h).inv h))
                    source
                    theorem CategoryTheory.Pseudofunctor.map₂_left_unitor_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} (f : a ⟶ b) {Z : (↑self.toPrelaxFunctor).obj a ⟶ (↑self.toPrelaxFunctor).obj b} (h : (↑self.toPrelaxFunctor).map f ⟶ Z) :
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.PrelaxFunctor.map₂ self.toPrelaxFunctor (CategoryTheory.Bicategory.leftUnitor f).hom) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.mapComp self (CategoryTheory.CategoryStruct.id a) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Pseudofunctor.mapId self a).hom ((↑self.toPrelaxFunctor).map f)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor ((↑self.toPrelaxFunctor).map f)).hom h))
                    source
                    theorem CategoryTheory.Pseudofunctor.map₂_whisker_left_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} {c : B} (f : a ⟶ b) {g : b ⟶ c} {h : b ⟶ c} (η : g ⟶ h) {Z : (↑self.toPrelaxFunctor).obj a ⟶ (↑self.toPrelaxFunctor).obj c} (h : (↑self.toPrelaxFunctor).map (CategoryTheory.CategoryStruct.comp f h) ⟶ Z) :
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.PrelaxFunctor.map₂ self.toPrelaxFunctor (CategoryTheory.Bicategory.whiskerLeft f η)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.mapComp self f g).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((↑self.toPrelaxFunctor).map f) (CategoryTheory.PrelaxFunctor.map₂ self.toPrelaxFunctor η)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.mapComp self f h).inv h))
                    source
                    theorem CategoryTheory.Pseudofunctor.map₂_associator_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) {Z : (↑self.toPrelaxFunctor).obj a ⟶ (↑self.toPrelaxFunctor).obj d} (h : (↑self.toPrelaxFunctor).map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)) ⟶ Z) :
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.PrelaxFunctor.map₂ self.toPrelaxFunctor (CategoryTheory.Bicategory.associator f g h).hom) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.mapComp self (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Pseudofunctor.mapComp self f g).hom ((↑self.toPrelaxFunctor).map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator ((↑self.toPrelaxFunctor).map f) ((↑self.toPrelaxFunctor).map g) ((↑self.toPrelaxFunctor).map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((↑self.toPrelaxFunctor).map f) (CategoryTheory.Pseudofunctor.mapComp self g h).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.mapComp self f (CategoryTheory.CategoryStruct.comp g h)).inv h))))
                    source
                    instance CategoryTheory.Pseudofunctor.hasCoeToPrelaxFunctor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] :
                    Coe (CategoryTheory.Pseudofunctor B C) (CategoryTheory.PrelaxFunctor B C)
                    source
                    def CategoryTheory.Pseudofunctor.toOplax {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) :
                    CategoryTheory.OplaxFunctor B C

                    The oplax functor associated with a pseudofunctor.

                    Instances For
                      source
                      instance CategoryTheory.Pseudofunctor.hasCoeToOplax {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] :
                      Coe (CategoryTheory.Pseudofunctor B C) (CategoryTheory.OplaxFunctor B C)
                      source
                      @[simp]
                      theorem CategoryTheory.Pseudofunctor.to_oplax_obj {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) :
                      (↑(CategoryTheory.Pseudofunctor.toOplax F).toPrelaxFunctor).obj = F.obj
                      source
                      @[simp]
                      theorem CategoryTheory.Pseudofunctor.to_oplax_mapId {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) (a : B) :
                      CategoryTheory.OplaxFunctor.mapId (CategoryTheory.Pseudofunctor.toOplax F) a = (CategoryTheory.Pseudofunctor.mapId F a).hom
                      source
                      @[simp]
                      theorem CategoryTheory.Pseudofunctor.to_oplax_mapComp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) :
                      CategoryTheory.OplaxFunctor.mapComp (CategoryTheory.Pseudofunctor.toOplax F) f g = (CategoryTheory.Pseudofunctor.mapComp F f g).hom
                      source
                      @[simp]
                      theorem CategoryTheory.Pseudofunctor.mapFunctor_map {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) (a : B) (b : B) :
                      ∀ {X Y : a ⟶ b} (η : X ⟶ Y), (CategoryTheory.Pseudofunctor.mapFunctor F a b).map η = CategoryTheory.PrelaxFunctor.map₂ (CategoryTheory.Pseudofunctor.toOplax F).toPrelaxFunctor η
                      source
                      @[simp]
                      theorem CategoryTheory.Pseudofunctor.mapFunctor_obj {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) (a : B) (b : B) (f : a ⟶ b) :
                      (CategoryTheory.Pseudofunctor.mapFunctor F a b).obj f = (↑(CategoryTheory.Pseudofunctor.toOplax F).toPrelaxFunctor).map f
                      source
                      def CategoryTheory.Pseudofunctor.mapFunctor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) (a : B) (b : B) :
                      CategoryTheory.Functor (a ⟶ b) ((↑F.toPrelaxFunctor).obj a ⟶ (↑F.toPrelaxFunctor).obj b)

                      Function on 1-morphisms as a functor.

                      Instances For
                        source
                        @[simp]
                        theorem CategoryTheory.Pseudofunctor.id_mapId (B : Type u₁) [CategoryTheory.Bicategory B] (a : B) :
                        CategoryTheory.Pseudofunctor.mapId (CategoryTheory.Pseudofunctor.id B) a = CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.id a)
                        source
                        @[simp]
                        theorem CategoryTheory.Pseudofunctor.id_mapComp (B : Type u₁) [CategoryTheory.Bicategory B] :
                        ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.Pseudofunctor.mapComp (CategoryTheory.Pseudofunctor.id B) f g = CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.comp f g)
                        source
                        @[simp]
                        theorem CategoryTheory.Pseudofunctor.id_toPrelaxFunctor_toPrefunctor (B : Type u₁) [CategoryTheory.Bicategory B] :
                        ↑(CategoryTheory.Pseudofunctor.id B).toPrelaxFunctor = ↑(CategoryTheory.PrelaxFunctor.id B)
                        source
                        @[simp]
                        theorem CategoryTheory.Pseudofunctor.id_toPrelaxFunctor_map₂ (B : Type u₁) [CategoryTheory.Bicategory B] :
                        ∀ {a b : B} {f g : a ⟶ b} (a_1 : f ⟶ g), CategoryTheory.PrelaxFunctor.map₂ (CategoryTheory.Pseudofunctor.id B).toPrelaxFunctor a_1 = CategoryTheory.PrelaxFunctor.map₂ (CategoryTheory.PrelaxFunctor.id B) a_1
                        source
                        def CategoryTheory.Pseudofunctor.id (B : Type u₁) [CategoryTheory.Bicategory B] :
                        CategoryTheory.Pseudofunctor B B

                        The identity pseudofunctor.

                        Instances For
                          source
                          instance CategoryTheory.Pseudofunctor.instInhabitedPseudofunctor {B : Type u₁} [CategoryTheory.Bicategory B] :
                          Inhabited (CategoryTheory.Pseudofunctor B B)
                          source
                          @[simp]
                          theorem CategoryTheory.Pseudofunctor.comp_mapComp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {D : Type u₃} [CategoryTheory.Bicategory D] (F : CategoryTheory.Pseudofunctor B C) (G : CategoryTheory.Pseudofunctor C D) :
                          ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.Pseudofunctor.mapComp (CategoryTheory.Pseudofunctor.comp F G) f g = (CategoryTheory.Pseudofunctor.mapFunctor G ((↑F.toPrelaxFunctor).obj a) ((↑F.toPrelaxFunctor).obj c)).mapIso (CategoryTheory.Pseudofunctor.mapComp F f g) ≪≫ CategoryTheory.Pseudofunctor.mapComp G ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g)
                          source
                          @[simp]
                          theorem CategoryTheory.Pseudofunctor.comp_toPrelaxFunctor_toPrefunctor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {D : Type u₃} [CategoryTheory.Bicategory D] (F : CategoryTheory.Pseudofunctor B C) (G : CategoryTheory.Pseudofunctor C D) :
                          ↑(CategoryTheory.Pseudofunctor.comp F G).toPrelaxFunctor = ↑(CategoryTheory.PrelaxFunctor.comp F.toPrelaxFunctor G.toPrelaxFunctor)
                          source
                          @[simp]
                          theorem CategoryTheory.Pseudofunctor.comp_mapId {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {D : Type u₃} [CategoryTheory.Bicategory D] (F : CategoryTheory.Pseudofunctor B C) (G : CategoryTheory.Pseudofunctor C D) (a : B) :
                          CategoryTheory.Pseudofunctor.mapId (CategoryTheory.Pseudofunctor.comp F G) a = (CategoryTheory.Pseudofunctor.mapFunctor G ((↑F.toPrelaxFunctor).obj a) ((↑F.toPrelaxFunctor).obj a)).mapIso (CategoryTheory.Pseudofunctor.mapId F a) ≪≫ CategoryTheory.Pseudofunctor.mapId G ((↑F.toPrelaxFunctor).obj a)
                          source
                          @[simp]
                          theorem CategoryTheory.Pseudofunctor.comp_toPrelaxFunctor_map₂ {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {D : Type u₃} [CategoryTheory.Bicategory D] (F : CategoryTheory.Pseudofunctor B C) (G : CategoryTheory.Pseudofunctor C D) :
                          ∀ {a b : B} {f g : a ⟶ b} (a_1 : f ⟶ g), CategoryTheory.PrelaxFunctor.map₂ (CategoryTheory.Pseudofunctor.comp F G).toPrelaxFunctor a_1 = CategoryTheory.PrelaxFunctor.map₂ (CategoryTheory.PrelaxFunctor.comp F.toPrelaxFunctor G.toPrelaxFunctor) a_1
                          source
                          def CategoryTheory.Pseudofunctor.comp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {D : Type u₃} [CategoryTheory.Bicategory D] (F : CategoryTheory.Pseudofunctor B C) (G : CategoryTheory.Pseudofunctor C D) :
                          CategoryTheory.Pseudofunctor B D

                          Composition of pseudofunctors.

                          Instances For
                            source
                            @[simp]
                            theorem CategoryTheory.Pseudofunctor.mkOfOplax_toPrelaxFunctor_toPrefunctor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (F' : CategoryTheory.OplaxFunctor.PseudoCore F) :
                            ↑(CategoryTheory.Pseudofunctor.mkOfOplax F F').toPrelaxFunctor = ↑F.toPrelaxFunctor
                            source
                            @[simp]
                            theorem CategoryTheory.Pseudofunctor.mkOfOplax_mapId {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (F' : CategoryTheory.OplaxFunctor.PseudoCore F) (a : B) :
                            CategoryTheory.Pseudofunctor.mapId (CategoryTheory.Pseudofunctor.mkOfOplax F F') a = CategoryTheory.OplaxFunctor.PseudoCore.mapIdIso F' a
                            source
                            @[simp]
                            theorem CategoryTheory.Pseudofunctor.mkOfOplax_mapComp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (F' : CategoryTheory.OplaxFunctor.PseudoCore F) :
                            ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.Pseudofunctor.mapComp (CategoryTheory.Pseudofunctor.mkOfOplax F F') f g = CategoryTheory.OplaxFunctor.PseudoCore.mapCompIso F' f g
                            source
                            @[simp]
                            theorem CategoryTheory.Pseudofunctor.mkOfOplax_toPrelaxFunctor_map₂ {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (F' : CategoryTheory.OplaxFunctor.PseudoCore F) :
                            ∀ {a b : B} {f g : a ⟶ b} (a_1 : f ⟶ g), CategoryTheory.PrelaxFunctor.map₂ (CategoryTheory.Pseudofunctor.mkOfOplax F F').toPrelaxFunctor a_1 = CategoryTheory.PrelaxFunctor.map₂ F.toPrelaxFunctor a_1
                            source
                            def CategoryTheory.Pseudofunctor.mkOfOplax {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (F' : CategoryTheory.OplaxFunctor.PseudoCore F) :
                            CategoryTheory.Pseudofunctor B C

                            Construct a pseudofunctor from an oplax functor whose mapId and mapComp are isomorphisms.

                            Instances For
                              source
                              @[simp]
                              theorem CategoryTheory.Pseudofunctor.mkOfOplax'_toPrelaxFunctor_toPrefunctor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) [∀ (a : B), CategoryTheory.IsIso (CategoryTheory.OplaxFunctor.mapId F a)] [∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (CategoryTheory.OplaxFunctor.mapComp F f g)] :
                              ↑(CategoryTheory.Pseudofunctor.mkOfOplax' F).toPrelaxFunctor = ↑F.toPrelaxFunctor
                              source
                              @[simp]
                              theorem CategoryTheory.Pseudofunctor.mkOfOplax'_mapId {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) [∀ (a : B), CategoryTheory.IsIso (CategoryTheory.OplaxFunctor.mapId F a)] [∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (CategoryTheory.OplaxFunctor.mapComp F f g)] (a : B) :
                              CategoryTheory.Pseudofunctor.mapId (CategoryTheory.Pseudofunctor.mkOfOplax' F) a = CategoryTheory.asIso (CategoryTheory.OplaxFunctor.mapId F a)
                              source
                              @[simp]
                              theorem CategoryTheory.Pseudofunctor.mkOfOplax'_mapComp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) [∀ (a : B), CategoryTheory.IsIso (CategoryTheory.OplaxFunctor.mapId F a)] [∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (CategoryTheory.OplaxFunctor.mapComp F f g)] :
                              ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.Pseudofunctor.mapComp (CategoryTheory.Pseudofunctor.mkOfOplax' F) f g = CategoryTheory.asIso (CategoryTheory.OplaxFunctor.mapComp F f g)
                              source
                              @[simp]
                              theorem CategoryTheory.Pseudofunctor.mkOfOplax'_toPrelaxFunctor_map₂ {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) [∀ (a : B), CategoryTheory.IsIso (CategoryTheory.OplaxFunctor.mapId F a)] [∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (CategoryTheory.OplaxFunctor.mapComp F f g)] :
                              ∀ {a b : B} {f g : a ⟶ b} (a_1 : f ⟶ g), CategoryTheory.PrelaxFunctor.map₂ (CategoryTheory.Pseudofunctor.mkOfOplax' F).toPrelaxFunctor a_1 = CategoryTheory.PrelaxFunctor.map₂ F.toPrelaxFunctor a_1
                              source
                              noncomputable def CategoryTheory.Pseudofunctor.mkOfOplax' {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) [∀ (a : B), CategoryTheory.IsIso (CategoryTheory.OplaxFunctor.mapId F a)] [∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (CategoryTheory.OplaxFunctor.mapComp F f g)] :
                              CategoryTheory.Pseudofunctor B C

                              Construct a pseudofunctor from an oplax functor whose mapId and mapComp are isomorphisms.

                              Instances For