The strict bicategory associated to a Cat-enriched category

If C is a type with a EnrichedCategory Cat C structure, then it has hom-categories, whose objects define 1-dimensional arrows on C and whose morphisms define 2-dimensional arrows between these. The enriched category axioms equip this data with the structure of a strict bicategory.

We define a type alias CatEnriched C for a type C with a EnrichedCategory Cat C structure. We provide this with an instance of a strict bicategory structure constructing Bicategory.Strict (CatEnriched C).

If C is a type with a EnrichedOrdinaryCategory Cat C structure, then it has an Enrichred Cat C structure, so the previous construction would again produce a strict bicategory. However, in this setting C is also given a Category C structure, together with an equivalence between this category and the underlying category of the Enriched Cat C, and in examples the given category structure is the preferred one.

Thus, we define a type alias CatEnrichedOrdinary C for a type C with an EnrichedOrdinaryCategory Cat C structure. We provide this with an instance of a strict bicategory structure extending the category structure provided by the given instance Category C constructing Bicategory.Strict (CatEnrichedOrdinary C).

def CategoryTheory.CatEnriched (C : Type u_2) : Type u_2

A type synonym for C, which should come equipped with a Cat-enriched category structure. This converts it to a strict bicategory where Category (X ⟶ Y) is (X ⟶[Cat] Y).

instance CategoryTheory.CatEnriched.instEnrichedCategoryCat {C : Type u_1} [EnrichedCategory Cat C] : EnrichedCategory Cat (CatEnriched C)

instance CategoryTheory.CatEnriched.instCategoryStruct {C : Type u_1} [EnrichedCategory Cat C] : CategoryStruct.{u_2, u_1} (CatEnriched C)

Any enriched category has an underlying category structure defined by ForgetEnrichment. This is equivalent but not definitionally equal the category structure constructed here, which is more canonically associated to the data of an EnrichedCategory Cat structure.

theorem CategoryTheory.CatEnriched.id_eq {C : Type u_1} [EnrichedCategory Cat C] (X : CatEnriched C) : CategoryStruct.id X = (eId Cat X).obj { down := { as := () } }

theorem CategoryTheory.CatEnriched.comp_eq {C : Type u_1} [EnrichedCategory Cat C] {X Y Z : CatEnriched C} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryStruct.comp f g = (eComp Cat X Y Z).obj (f, g)

instance CategoryTheory.CatEnriched.instCategoryHom {C : Type u_1} [EnrichedCategory Cat C] {X Y : CatEnriched C} : Category.{u_3, u_2} (X ⟶ Y)

def CategoryTheory.CatEnriched.hComp {C : Type u_1} [EnrichedCategory Cat C] {a b c : CatEnriched C} {f f' : a ⟶ b} {g g' : b ⟶ c} (η : f ⟶ f') (θ : g ⟶ g') : CategoryStruct.comp f g ⟶ CategoryStruct.comp f' g'

The horizontal composition on 2-morphisms is defined using the action on arrows of the composition bifunctor from the enriched category structure.

@[simp]

theorem CategoryTheory.CatEnriched.id_hComp_id {C : Type u_1} [EnrichedCategory Cat C] {a b c : CatEnriched C} (f : a ⟶ b) (g : b ⟶ c) : hComp (CategoryStruct.id f) (CategoryStruct.id g) = CategoryStruct.id (CategoryStruct.comp f g)

@[simp]

theorem CategoryTheory.CatEnriched.eqToHom_hComp_eqToHom {C : Type u_1} [EnrichedCategory Cat C] {a b c : CatEnriched C} {f f' : a ⟶ b} (α : f = f') {g g' : b ⟶ c} (β : g = g') : hComp (eqToHom α) (eqToHom β) = eqToHom ⋯

@[simp]

theorem CategoryTheory.CatEnriched.hComp_comp {C : Type u_1} [EnrichedCategory Cat C] {a b c : CatEnriched C} {f₁ f₂ f₃ : a ⟶ b} {g₁ g₂ g₃ : b ⟶ c} (η : f₁ ⟶ f₂) (η' : f₂ ⟶ f₃) (θ : g₁ ⟶ g₂) (θ' : g₂ ⟶ g₃) : CategoryStruct.comp (hComp η θ) (hComp η' θ') = hComp (CategoryStruct.comp η η') (CategoryStruct.comp θ θ')

The interchange law for horizontal and vertical composition of 2-cells in a bicategory.

instance CategoryTheory.CatEnriched.instCategory {C : Type u_1} [EnrichedCategory Cat C] : Category.{u_2, u_1} (CatEnriched C)

The action on objects of the EnrichedCategory Cat coherences proves the category axioms.

instance CategoryTheory.CatEnriched.instEnrichedOrdinaryCategoryCat {C : Type u_1} [EnrichedCategory Cat C] : EnrichedOrdinaryCategory Cat (CatEnriched C)

The category instance on CatEnriched C promotes it to a Cat enriched ordinary category.

theorem CategoryTheory.CatEnriched.id_hComp_heq {C : Type u_1} [EnrichedCategory Cat C] {a b : CatEnriched C} {f f' : a ⟶ b} (η : f ⟶ f') : hComp (CategoryStruct.id (CategoryStruct.id a)) η ≍ η

theorem CategoryTheory.CatEnriched.id_hComp {C : Type u_1} [EnrichedCategory Cat C] {a b : CatEnriched C} {f f' : a ⟶ b} (η : f ⟶ f') : hComp (CategoryStruct.id (CategoryStruct.id a)) η = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp η (eqToHom ⋯))

theorem CategoryTheory.CatEnriched.hComp_id_heq {C : Type u_1} [EnrichedCategory Cat C] {a b : CatEnriched C} {f f' : a ⟶ b} (η : f ⟶ f') : hComp η (CategoryStruct.id (CategoryStruct.id b)) ≍ η

theorem CategoryTheory.CatEnriched.hComp_id {C : Type u_1} [EnrichedCategory Cat C] {a b : CatEnriched C} {f f' : a ⟶ b} (η : f ⟶ f') : hComp η (CategoryStruct.id (CategoryStruct.id b)) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp η (eqToHom ⋯))

theorem CategoryTheory.CatEnriched.hComp_assoc_heq {C : Type u_1} [EnrichedCategory Cat C] {a b c d : CatEnriched C} {f f' : a ⟶ b} {g g' : b ⟶ c} {h h' : c ⟶ d} (η : f ⟶ f') (θ : g ⟶ g') (κ : h ⟶ h') : hComp (hComp η θ) κ ≍ hComp η (hComp θ κ)

theorem CategoryTheory.CatEnriched.hComp_assoc {C : Type u_1} [EnrichedCategory Cat C] {a b c d : CatEnriched C} {f f' : a ⟶ b} {g g' : b ⟶ c} {h h' : c ⟶ d} (η : f ⟶ f') (θ : g ⟶ g') (κ : h ⟶ h') : hComp (hComp η θ) κ = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (hComp η (hComp θ κ)) (eqToHom ⋯))

instance CategoryTheory.CatEnriched.instBicategory {C : Type u_1} [EnrichedCategory Cat C] : Bicategory (CatEnriched C)

instance CategoryTheory.CatEnriched.instStrict {C : Type u_1} [EnrichedCategory Cat C] : Bicategory.Strict (CatEnriched C)

As the associator and left and right unitors are defined as eqToIso of category axioms, the bicategory structure on CatEnriched C is strict.

def CategoryTheory.CatEnrichedOrdinary (C : Type u_1) : Type u_1

A type synonym for C, which should come equipped with a Cat-enriched category structure. This converts it to a strict bicategory where Category (X ⟶ Y) is (X ⟶[Cat] Y).

instance CategoryTheory.CatEnrichedOrdinary.instCategory {C : Type u} [Category.{v, u} C] : Category.{v, u} (CatEnrichedOrdinary C)

instance CategoryTheory.CatEnrichedOrdinary.instEnrichedCategoryCat {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] : EnrichedCategory Cat (CatEnrichedOrdinary C)

instance CategoryTheory.CatEnrichedOrdinary.instEnrichedOrdinaryCategoryCat {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] : EnrichedOrdinaryCategory Cat (CatEnrichedOrdinary C)

def CategoryTheory.CatEnrichedOrdinary.toBase {C : Type u} (a : CatEnrichedOrdinary C) : CatEnriched C

The forgetful map from the type alias associated to EnrichedOrdinaryCategory Cat C and the type alias associated to EnrichedCategory Cat C is the identity on underlying types.

def CategoryTheory.CatEnrichedOrdinary.homEquiv {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {a b : CatEnrichedOrdinary C} : (a ⟶ b) ≃ (a.toBase ⟶ b.toBase)

The hom-types in a Cat-enriched ordinary category are equivalent to the types underlying the hom-categories.

theorem CategoryTheory.CatEnrichedOrdinary.homEquiv_id {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {a : CatEnrichedOrdinary C} : homEquiv (CategoryStruct.id a) = CategoryStruct.id a.toBase

theorem CategoryTheory.CatEnrichedOrdinary.homEquiv_comp {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {a b c : CatEnrichedOrdinary C} (f : a ⟶ b) (g : b ⟶ c) : homEquiv (CategoryStruct.comp f g) = CategoryStruct.comp (homEquiv f) (homEquiv g)

structure CategoryTheory.CatEnrichedOrdinary.Hom {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {X Y : CatEnrichedOrdinary C} (f g : X ⟶ Y) : Type v'

The 2-cells between a parallel pair of 1-cells f g in CatEnrichedOrdinary C are defined to be the morphisms in the hom-categories provided by the EnrichedCategory Cat C structure between the corresponding objects.

• mk' :: (
• base' : homEquiv f ⟶ homEquiv g

  A 2-cell from f to g is a 2-cell from homEquiv f to homEquiv g.

• )

instance CategoryTheory.CatEnrichedOrdinary.instQuiverHom {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {X Y : CatEnrichedOrdinary C} : Quiver (X ⟶ Y)

def CategoryTheory.CatEnrichedOrdinary.Hom.base {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {X Y : CatEnrichedOrdinary C} {f g : X ⟶ Y} (α : f ⟶ g) : homEquiv f ⟶ homEquiv g

A 2-cell in CatEnrichedOrdinary C has a corresponding "base" 2-cell in CatEnriched C.

def CategoryTheory.CatEnrichedOrdinary.Hom.mk {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {X Y : CatEnrichedOrdinary C} {f g : X ⟶ Y} (α : homEquiv f ⟶ homEquiv g) : f ⟶ g

A 2-cell in CatEnriched C can be "made" into a 2-cell in CatEnrichedOrdinary C.

@[simp]

theorem CategoryTheory.CatEnrichedOrdinary.mk_base {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {X Y : CatEnrichedOrdinary C} {f g : X ⟶ Y} (α : f ⟶ g) : Hom.mk (Hom.base α) = α

@[simp]

theorem CategoryTheory.CatEnrichedOrdinary.base_mk {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {X Y : CatEnrichedOrdinary C} {f g : X ⟶ Y} (α : homEquiv f ⟶ homEquiv g) : Hom.base (Hom.mk α) = α

instance CategoryTheory.CatEnrichedOrdinary.instCategoryStructHom {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {X Y : CatEnrichedOrdinary C} : CategoryStruct.{v', v} (X ⟶ Y)

theorem CategoryTheory.CatEnrichedOrdinary.Hom.id_eq {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {X Y : CatEnrichedOrdinary C} (f : X ⟶ Y) : CategoryStruct.id f = mk (CategoryStruct.id (homEquiv f))

@[simp]

theorem CategoryTheory.CatEnrichedOrdinary.Hom.base_id {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {X Y : CatEnrichedOrdinary C} (f : X ⟶ Y) : base (CategoryStruct.id f) = CategoryStruct.id (homEquiv f)

theorem CategoryTheory.CatEnrichedOrdinary.Hom.comp_eq {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {X Y : CatEnrichedOrdinary C} {f g h : X ⟶ Y} (α : f ⟶ g) (β : g ⟶ h) : CategoryStruct.comp α β = mk (CategoryStruct.comp (base α) (base β))

@[simp]

theorem CategoryTheory.CatEnrichedOrdinary.Hom.base_comp {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {X Y : CatEnrichedOrdinary C} {f g h : X ⟶ Y} (α : f ⟶ g) (β : g ⟶ h) : base (CategoryStruct.comp α β) = CategoryStruct.comp (base α) (base β)

theorem CategoryTheory.CatEnrichedOrdinary.Hom.mk_comp {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {X Y : CatEnrichedOrdinary C} {f g h : X ⟶ Y} (α : homEquiv f ⟶ homEquiv g) (β : homEquiv g ⟶ homEquiv h) : mk (CategoryStruct.comp α β) = CategoryStruct.comp (mk α) (mk β)

theorem CategoryTheory.CatEnrichedOrdinary.Hom.ext {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {X Y : CatEnrichedOrdinary C} {f g : X ⟶ Y} (α β : f ⟶ g) (H : base α = base β) : α = β

theorem CategoryTheory.CatEnrichedOrdinary.Hom.ext_iff {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {X Y : CatEnrichedOrdinary C} {f g : X ⟶ Y} {α β : f ⟶ g} : α = β ↔ base α = base β

instance CategoryTheory.CatEnrichedOrdinary.instCategoryHom {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {X Y : CatEnrichedOrdinary C} : Category.{v', v} (X ⟶ Y)

A Cat-enriched ordinary category comes with hom-categories X ⟶[Cat] Y whose underlying type of objects is equivalent to the type X ⟶ Y defined by the category structure on C. The following definition transfers the category structure to the latter type of objects.

@[simp]

theorem CategoryTheory.CatEnrichedOrdinary.Hom.base_eqToHom {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {X Y : CatEnrichedOrdinary C} {f g : X ⟶ Y} (α : f = g) : base (eqToHom α) = eqToHom ⋯

def CategoryTheory.CatEnrichedOrdinary.hComp {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {a b c : CatEnrichedOrdinary C} {f f' : a ⟶ b} {g g' : b ⟶ c} (η : f ⟶ f') (θ : g ⟶ g') : CategoryStruct.comp f g ⟶ CategoryStruct.comp f' g'

The horizontal composition on 2-morphisms is defined using the action on arrows of the composition bifunctor from the enriched category structure.

@[simp]

theorem CategoryTheory.CatEnrichedOrdinary.id_hComp_id {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {a b c : CatEnrichedOrdinary C} (f : a ⟶ b) (g : b ⟶ c) : hComp (CategoryStruct.id f) (CategoryStruct.id g) = CategoryStruct.id (CategoryStruct.comp f g)

@[simp]

theorem CategoryTheory.CatEnrichedOrdinary.eqToHom_hComp_eqToHom {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {a b c : CatEnrichedOrdinary C} {f f' : a ⟶ b} (α : f = f') {g g' : b ⟶ c} (β : g = g') : hComp (eqToHom α) (eqToHom β) = eqToHom ⋯

@[simp]

theorem CategoryTheory.CatEnrichedOrdinary.hComp_comp {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {a b c : CatEnrichedOrdinary C} {f₁ f₂ f₃ : a ⟶ b} {g₁ g₂ g₃ : b ⟶ c} (η : f₁ ⟶ f₂) (η' : f₂ ⟶ f₃) (θ : g₁ ⟶ g₂) (θ' : g₂ ⟶ g₃) : CategoryStruct.comp (hComp η θ) (hComp η' θ') = hComp (CategoryStruct.comp η η') (CategoryStruct.comp θ θ')

The interchange law for horizontal and vertical composition of 2-cells in a bicategory.

theorem CategoryTheory.CatEnrichedOrdinary.id_hComp {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {a b : CatEnrichedOrdinary C} {f f' : a ⟶ b} (η : f ⟶ f') : hComp (CategoryStruct.id (CategoryStruct.id a)) η = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp η (eqToHom ⋯))

theorem CategoryTheory.CatEnrichedOrdinary.id_hComp_heq {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {a b : CatEnrichedOrdinary C} {f f' : a ⟶ b} (η : f ⟶ f') : hComp (CategoryStruct.id (CategoryStruct.id a)) η ≍ η

theorem CategoryTheory.CatEnrichedOrdinary.hComp_id {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {a b : CatEnrichedOrdinary C} {f f' : a ⟶ b} (η : f ⟶ f') : hComp η (CategoryStruct.id (CategoryStruct.id b)) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp η (eqToHom ⋯))

theorem CategoryTheory.CatEnrichedOrdinary.hComp_id_heq {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {a b : CatEnrichedOrdinary C} {f f' : a ⟶ b} (η : f ⟶ f') : hComp η (CategoryStruct.id (CategoryStruct.id b)) ≍ η

theorem CategoryTheory.CatEnrichedOrdinary.id_eq_eqToHom {C : Type u_1} [Category.{u_2, u_1} C] (X : C) : CategoryStruct.id X = eqToHom ⋯

theorem CategoryTheory.CatEnrichedOrdinary.hComp_assoc {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {a b c d : CatEnrichedOrdinary C} {f f' : a ⟶ b} {g g' : b ⟶ c} {h h' : c ⟶ d} (η : f ⟶ f') (θ : g ⟶ g') (κ : h ⟶ h') : hComp (hComp η θ) κ = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (hComp η (hComp θ κ)) (eqToHom ⋯))

theorem CategoryTheory.CatEnrichedOrdinary.hComp_assoc_heq {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] {a b c d : CatEnrichedOrdinary C} {f f' : a ⟶ b} {g g' : b ⟶ c} {h h' : c ⟶ d} (η : f ⟶ f') (θ : g ⟶ g') (κ : h ⟶ h') : hComp (hComp η θ) κ ≍ hComp η (hComp θ κ)

instance CategoryTheory.CatEnrichedOrdinary.instBicategory {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] : Bicategory (CatEnrichedOrdinary C)

instance CategoryTheory.CatEnrichedOrdinary.instStrict {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory Cat C] : Bicategory.Strict (CatEnrichedOrdinary C)

As the associator and left and right unitors are defined as eqToIso of category axioms, the bicategory structure on CatEnrichedOrdinary C is strict.