Defining 2-category in lean?

Stream: Is there code for X?

[Coriver Chen]

Hi how to define 2-category in lean? I found that it even quite hard to define the data

[Coriver Chen]

I checked Quiver's definition and try something like

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Products.Basic


open CategoryTheory

universe w v u

class TwoQuiver (V : Type u) where
  Hom : V → V → Sort v
  Trans : Sort v → Sort v → Sort w

[Coriver Chen]

Is the type signature OK for https://ncatlab.org/nlab/show/2-category ?

[Coriver Chen]

I tried

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Products.Basic


open CategoryTheory

universe w v u₁ u₂ u₃

variable (V : Type v) [CategoryTheory.Category.{w} V]

class TwoCategory (C: Type u₁) where
  Hom : C →  C →  V
  h_comp{X Y Z: C}: Hom X Y × Hom Y Z → Hom X Z

too code in playground but it says "type expected, got (Hom X Z : V)"

[Coriver Chen]

I understand that Hom X Z is a value with type V, but it should also be treat as a type too?

[Scott Morrison]

docs#CategoryTheory.Bicategory

[Coriver Chen]

I am continuing the construction of the definition of 2-category in lean, using the idea similar to Bicategory.
Now I get the following code:

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Products.Basic
import Mathlib.CategoryTheory.Products.Associator
import Mathlib.CategoryTheory.Functor.Basic
import Mathlib.CategoryTheory.Functor.Currying

open CategoryTheory
open CategoryTheory.prod
universe w v u u₁ u₂ u₃  v₁ v₂ v₃
variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] {E : Type u₃} [Category.{v₃} E]

-- copy from Mathlib.CategoryTheory.Functor.Currying
-- where it does not curry the second, werid
def curryObj₂ (F : C × D ⥤ E) : D ⥤ C ⥤ E
    where
  obj Y :=
    { obj := fun X => F.obj (X, Y)
      map := fun g => F.map (g, 𝟙 Y)
      map_id := fun X => by simp only [F.map_id]; rw [←prod_id]; exact F.map_id ⟨X,Y⟩
      map_comp := fun f g => by simp [←F.map_comp]}
  map g :=
    { app := fun X => F.map (𝟙 X, g)
      naturality := fun {Y} {Y'} g => by simp [←F.map_comp] }
  map_id := fun X => by ext Y; exact F.map_id _
  map_comp := fun f g => by ext Y; dsimp; simp [←F.map_comp]

class TwoCategory (C : Type u) extends Quiver.{v + 1} C : Type (max (max u (v + 1)) (w + 1)) where
  homCategory(X Y : C) : Category.{w} (X ⟶ Y)
  h_comp{X Y Z : C} : (X ⟶ Y) × (Y ⟶ Z) ⥤ (X ⟶ Z)

  -- cannot use symbol 𝟙
  id(X : C) : X ⟶ X
  id_eq₁(X Y : C) : (curryObj h_comp).obj (id X) = 𝟭 (X ⟶ Y)
  id_eq₂(X Y : C) : (curryObj₂ h_comp).obj (id Y) = 𝟭 (X ⟶ Y)

  assoc(X Y Z W : C) : (@h_comp X Y Z).prod (𝟭 (Z ⟶ W)) ⋙ (@h_comp X Z W) = ((𝟭 (X ⟶ Y)).prod (@h_comp Y Z W)) ⋙ (@h_comp X Y W)

[Coriver Chen]

But in the definition of assoc the kernel reprots the error

type mismatch
  Functor.prod (𝟭 (X ⟶ Y)) h_comp ⋙ h_comp
has type
  (X ⟶ Y) × (Y ⟶ Z) × (Z ⟶ W) ⥤ (X ⟶ W) : Type (max w v)
but is expected to have type
  ((X ⟶ Y) × (Y ⟶ Z)) × (Z ⟶ W) ⥤ (X ⟶ W) : Type (max w v)

Is it any way to fix this? It seems that the equivalance (C × D) × E ≌ C × D × E has to be considered. I saw CategoryTheory.prod.associativity. But I have no idea how to use it. Thank you very much!

[Scott Morrison]

Can't you just use the existing Bicategory? Setting up this definition is not the easiest learning exercise for a beginner.

[Coriver Chen]

Yeah I can do that too. Now I see that "any strict 2-category is a bicategory in which the unitors and associator are identities. " in ncatlab. Using the existing bicategory and adding two more constraints to it should be enough, I will try to do it this way.

[Dean Young]

@Coriver Chen it's worth noting that a strict twocategory can be made to have seven entries just like a category, if you bundle them up right:

-- definition of a (strict) twocategory
structure twocategory.{w} where
  Obj : Type w
  Hom : Obj →
        Obj →
        category
  Idn : (C : Obj) →
        Cat.Hom *_Cat (Hom C C)
  Cmp : (C : Obj) →
        (D : Obj) →
        (E : Obj) →
        Cat.Hom ((Hom C D) ×_Cat (Hom D E)) (Hom C E)
  Id₁ : (C : Obj) →
        (D : Obj) →
        ((Cmp C D D) ∘_(Cat) ((𝟙_(Cat) (Hom C D)) ×_Fun (Idn D)) ∘_(Cat) (PrdId₁ (Hom C D)).Fst) = (𝟙_(Cat) (Hom C D))
  Id₂ : (C : Obj) →
        (D : Obj) →
        ((Cmp C C D) ∘_(Cat) ((Idn C) ×_Fun (𝟙_(Cat) (Hom C D))) ∘_(Cat) (PrdId₂Fst (Hom C D))) = (𝟙_(Cat) (Hom C D))
  Ass : (B : Obj) →
        (C : Obj) →
        (D : Obj) →
        (E : Obj) →
        ((Cmp B C E) ∘_(Cat) ((𝟙_(Cat) (Hom B C)) ×_Fun (Cmp C D E))) = (Cmp B D E) ∘_(Cat) ((Cmp B C D) ×_Fun (𝟙_(Cat) (Hom D E))) ∘_(Cat) (PrdAss (Hom B C) (Hom C D) (Hom D E)).Fst

This is more cumbersome than using a bicategory though.

[Coriver Chen]

@Dean Young Thank you for the alternative definition. I will try this too. The definition of it seems to be possible in three ways: via data like obj, 1-morphism and 2-morphism; or as an enriched category; or from the definition of bicategory.