Documentation

Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete

Pseudofunctors from locally discrete bicategories #

This file provides various ways of constructing pseudofunctors from locally discrete bicategories.

Firstly, we define the constructors pseudofunctorOfIsLocallyDiscrete and oplaxFunctorOfIsLocallyDiscrete for defining pseudofunctors and oplax functors from a locally discrete bicategories. In this situation, we do not need to care about the field map₂, because all the 2-morphisms in B are identities.

We also define a specialized constructor LocallyDiscrete.mkPseudofunctor when the source bicategory is of the form B := LocallyDiscrete B₀ for a category B₀.

We also prove that a functor F : I ⥤ B with B a strict bicategory can be promoted to a pseudofunctor (or oplax functor) (Functor.toPseudofunctor) with domain LocallyDiscrete I.

source
def CategoryTheory.pseudofunctorOfIsLocallyDiscrete {B : Type u_1} {C : Type u_2} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.IsLocallyDiscrete B] [CategoryTheory.Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) :
CategoryTheory.Pseudofunctor B C

Constructor for pseudofunctors from a locally discrete bicategory. In that case, we do not need to provide the map₂ field of pseudofunctors.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.pseudofunctorOfIsLocallyDiscrete_obj {B : Type u_1} {C : Type u_2} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.IsLocallyDiscrete B] [CategoryTheory.Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (a✝ : B) :
    (CategoryTheory.pseudofunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).obj a✝ = obj a✝
    source
    @[simp]
    theorem CategoryTheory.pseudofunctorOfIsLocallyDiscrete_mapId {B : Type u_1} {C : Type u_2} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.IsLocallyDiscrete B] [CategoryTheory.Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (b : B) :
    (CategoryTheory.pseudofunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).mapId b = mapId b
    source
    @[simp]
    theorem CategoryTheory.pseudofunctorOfIsLocallyDiscrete_map {B : Type u_1} {C : Type u_2} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.IsLocallyDiscrete B] [CategoryTheory.Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) {X✝ Y✝ : B} (a✝ : X✝ ⟶ Y✝) :
    (CategoryTheory.pseudofunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).map a✝ = map a✝
    source
    @[simp]
    theorem CategoryTheory.pseudofunctorOfIsLocallyDiscrete_mapComp {B : Type u_1} {C : Type u_2} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.IsLocallyDiscrete B] [CategoryTheory.Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) :
    (CategoryTheory.pseudofunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).mapComp f g = mapComp f g
    source
    def CategoryTheory.oplaxFunctorOfIsLocallyDiscrete {B : Type u_1} {C : Type u_2} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.IsLocallyDiscrete B] [CategoryTheory.Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ⟶ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ⟶ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h))) = CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g) (map h)) (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom) := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀) (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁)) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) :
    CategoryTheory.OplaxFunctor B C

    Constructor for oplax functors from a locally discrete bicategory. In that case, we do not need to provide the map₂ field of oplax functors.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.oplaxFunctorOfIsLocallyDiscrete_mapComp {B : Type u_1} {C : Type u_2} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.IsLocallyDiscrete B] [CategoryTheory.Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ⟶ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ⟶ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h))) = CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g) (map h)) (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom) := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀) (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁)) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) :
      (CategoryTheory.oplaxFunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).mapComp f g = mapComp f g
      source
      @[simp]
      theorem CategoryTheory.oplaxFunctorOfIsLocallyDiscrete_obj {B : Type u_1} {C : Type u_2} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.IsLocallyDiscrete B] [CategoryTheory.Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ⟶ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ⟶ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h))) = CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g) (map h)) (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom) := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀) (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁)) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (a✝ : B) :
      (CategoryTheory.oplaxFunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).obj a✝ = obj a✝
      source
      @[simp]
      theorem CategoryTheory.oplaxFunctorOfIsLocallyDiscrete_mapId {B : Type u_1} {C : Type u_2} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.IsLocallyDiscrete B] [CategoryTheory.Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ⟶ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ⟶ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h))) = CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g) (map h)) (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom) := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀) (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁)) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (b : B) :
      (CategoryTheory.oplaxFunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).mapId b = mapId b
      source
      @[simp]
      theorem CategoryTheory.oplaxFunctorOfIsLocallyDiscrete_map {B : Type u_1} {C : Type u_2} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.IsLocallyDiscrete B] [CategoryTheory.Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ⟶ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ⟶ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h))) = CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g) (map h)) (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom) := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀) (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁)) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) {X✝ Y✝ : B} (a✝ : X✝ ⟶ Y✝) :
      (CategoryTheory.oplaxFunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).map a✝ = map a✝
      source
      def CategoryTheory.Functor.toPseudoFunctor {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) :
      CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete I) B

      If B is a strict bicategory and I is a (1-)category, any functor (of 1-categories) I ⥤ B can be promoted to a pseudofunctor from LocallyDiscrete I to B.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Functor.toPseudoFunctor_map {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) {X✝ Y✝ : CategoryTheory.LocallyDiscrete I} (x✝ : X✝ ⟶ Y✝) :
        F.toPseudoFunctor.map x✝ = F.map x✝.as
        source
        @[simp]
        theorem CategoryTheory.Functor.toPseudoFunctor_obj {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) (x✝ : CategoryTheory.LocallyDiscrete I) :
        F.toPseudoFunctor.obj x✝ = F.obj x✝.as
        source
        @[simp]
        theorem CategoryTheory.Functor.toPseudoFunctor_mapComp {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete I} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) :
        F.toPseudoFunctor.mapComp f g = CategoryTheory.eqToIso ⋯
        source
        @[simp]
        theorem CategoryTheory.Functor.toPseudoFunctor_mapId {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) (x✝ : CategoryTheory.LocallyDiscrete I) :
        F.toPseudoFunctor.mapId x✝ = CategoryTheory.eqToIso ⋯
        source
        def CategoryTheory.Functor.toOplaxFunctor {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) :
        CategoryTheory.OplaxFunctor (CategoryTheory.LocallyDiscrete I) B

        If B is a strict bicategory and I is a (1-)category, any functor (of 1-categories) I ⥤ B can be promoted to an oplax functor from LocallyDiscrete I to B.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Functor.toOplaxFunctor_obj {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) (x✝ : CategoryTheory.LocallyDiscrete I) :
          F.toOplaxFunctor.obj x✝ = F.obj x✝.as
          source
          @[simp]
          theorem CategoryTheory.Functor.toOplaxFunctor_map {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) {X✝ Y✝ : CategoryTheory.LocallyDiscrete I} (x✝ : X✝ ⟶ Y✝) :
          F.toOplaxFunctor.map x✝ = F.map x✝.as
          source
          @[simp]
          theorem CategoryTheory.Functor.toOplaxFunctor_mapId {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) (x✝ : CategoryTheory.LocallyDiscrete I) :
          F.toOplaxFunctor.mapId x✝ = CategoryTheory.eqToHom ⋯
          source
          @[simp]
          theorem CategoryTheory.Functor.toOplaxFunctor_mapComp {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete I} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) :
          F.toOplaxFunctor.mapComp f g = CategoryTheory.eqToHom ⋯
          source
          def CategoryTheory.LocallyDiscrete.mkPseudofunctor {B₀ : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} B₀] [CategoryTheory.Bicategory C] (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B₀) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) :
          CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete B₀) C

          Constructor for pseudofunctors from a locally discrete bicategory. In that case, we do not need to provide the map₂ field of pseudofunctors.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.LocallyDiscrete.mkPseudofunctor_mapComp {B₀ : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} B₀] [CategoryTheory.Bicategory C] (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B₀) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete B₀} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) :
            (CategoryTheory.LocallyDiscrete.mkPseudofunctor obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).mapComp x✝ x✝¹ = mapComp x✝.as x✝¹.as
            source
            @[simp]
            theorem CategoryTheory.LocallyDiscrete.mkPseudofunctor_map {B₀ : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} B₀] [CategoryTheory.Bicategory C] (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B₀) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) {X✝ Y✝ : CategoryTheory.LocallyDiscrete B₀} (f : X✝ ⟶ Y✝) :
            (CategoryTheory.LocallyDiscrete.mkPseudofunctor obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).map f = map f.as
            source
            @[simp]
            theorem CategoryTheory.LocallyDiscrete.mkPseudofunctor_obj {B₀ : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} B₀] [CategoryTheory.Bicategory C] (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B₀) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (b : CategoryTheory.LocallyDiscrete B₀) :
            (CategoryTheory.LocallyDiscrete.mkPseudofunctor obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).obj b = obj b.as
            source
            @[simp]
            theorem CategoryTheory.LocallyDiscrete.mkPseudofunctor_mapId {B₀ : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} B₀] [CategoryTheory.Bicategory C] (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B₀) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by aesop_cat) (x✝ : CategoryTheory.LocallyDiscrete B₀) :
            (CategoryTheory.LocallyDiscrete.mkPseudofunctor obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).mapId x✝ = mapId x✝.as