CategoryTheory.Category.mk

Stream: mathlib4

[Dean Young]

I've decided that Mathlib's categories, functors, natural transformations, and bicategories have advanced features I really respect, so I'm constructing bijections with their ordinary counterparts so I can learn to use them. It's more important to me that I be able to translate into Mathlib's categories, functors, natural transformations, bicategories than vice versa, since I'm content with the extensionality results of Mathlib's category library. I was hoping someone who knows the library could help me fill in these two .mk's, since there were some complexities in the inference that are giving me difficulties.

#check CategoryTheory.Category
#check CategoryTheory.Category.mk

-- A basic category structure
structure category.{u₀,v₀} where
  Obj : Type u₀
  Hom : Obj → Obj → Type v₀
  Idn : (X:Obj) → Hom X X
  Cmp : (X:Obj) → (Y:Obj) → (Z:Obj) → (_:Hom X Y) → (_:Hom Y Z) → Hom X Z
  Id₁ : (X:Obj) → (Y:Obj) → (f:Hom X Y) →
    Cmp X Y Y f (Idn Y) = f
  Id₂ : (X:Obj) → (Y:Obj) → (f:Hom X Y) →
    Cmp X X Y (Idn X) f = f
  Ass : (W:Obj) → (X:Obj) → (Y:Obj) → (Z:Obj) → (f:Hom W X) → (g:Hom X Y) → (h:Hom Y Z) →
    (Cmp W X Z) f (Cmp X Y Z g h) = Cmp W Y Z (Cmp W X Y f g) h

def dict₁ (C : category) : CategoryTheory.Category := sorry
-- It could be something involving CategoryTheory.Category.mk ...

The situation was similar with functors and natural transformations:

#check CategoryTheory.Functor
#check CategoryTheory.Functor.mk

I wanted to be able to go back and forth with it with only the information of this:

-- an ordinary functor structure
structure functor (C : category) (D : category) where
   Obj : ∀(_ : C.Obj),D.Obj
   Hom : ∀(X : C.Obj),∀(Y : C.Obj),∀(_ : C.Hom X Y),D.Hom (Obj X) (Obj Y)
   Idn : ∀(X : C.Obj),Hom X X (C.Idn X) = D.Idn (Obj X)
   Cmp : ∀(X : C.Obj),∀(Y : C.Obj),∀(Z : C.Obj),∀(f : C.Hom X Y),∀(g : C.Hom Y Z),
   D.Cmp (Obj X) (Obj Y) (Obj Z) (Hom X Y f) (Hom Y Z g) = Hom X Z (C.Cmp X Y Z f g)

def dict₂ (C : category) (D : category) (F : functor C D) : CategoryTheory.Functor (dict₁ C) (dict₁ D) := sorry
-- It could be CategoryTheory.Functor.mk ... (and it should involve two applications of dict₁)

The .mk's are a little complex for the object and hom components with some nice features clearly built in. Can anyone give me some advice on how to work these .mk's?

[Scott Morrison]

What you've written doesn't make sense. CategoryTheory.Functor is not a type: you need to parametrize is by two CategoryTheory.Categorys.

[Dean Young]

Ok, I made some edits.

[Dean Young]

I got the first part.

-- A category C consists of:
structure category.{u₀,v₀} where
  Obj : Type u₀
  Hom : Obj → Obj → Type v₀
  Idn : (X:Obj) → Hom X X
  Cmp : (X:Obj) → (Y:Obj) → (Z:Obj) → (_:Hom X Y) → (_:Hom Y Z) → Hom X Z
  Id₁ : (X:Obj) → (Y:Obj) → (f:Hom X Y) →
    Cmp X Y Y f (Idn Y) = f
  Id₂ : (X:Obj) → (Y:Obj) → (f:Hom X Y) →
    Cmp X X Y (Idn X) f = f
  Ass : (W:Obj) → (X:Obj) → (Y:Obj) → (Z:Obj) → (f:Hom W X) → (g:Hom X Y) → (h:Hom Y Z) →
    (Cmp W X Z) f (Cmp X Y Z g h) = Cmp W Y Z (Cmp W X Y f g) h



-- Notation for the identity map which infers the category:
def identity_map (C : category) (X : C.Obj) := C.Idn X
notation "𝟙_(" C ")" => identity_map C



-- Notation for composition which infers the category and objects:
def composition (C : category) {X : C.Obj} {Y : C.Obj} {Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) : C.Hom X Z := C.Cmp X Y Z f g
notation g "∘_(" C ")" f => composition C f g

theorem Id₁ (C : category) {X : C.Obj} { Y : C.Obj} (f : C.Hom X Y) :
  (f ∘_(C) (𝟙_(C) X)) = f := C.Id₂ X Y f

theorem Id₂ (C : category) {X Y : C.Obj} (f : C.Hom X Y) :
  (𝟙_(C) Y ∘_(C) f) = f := C.Id₁ X Y f

theorem Ass (C : category) {W X Y Z : C.Obj} (f : C.Hom W X) (g : C.Hom X Y) (h : C.Hom Y Z) :
  ((h ∘_(C) g) ∘_(C) f) = (h ∘_(C) (g ∘_(C) f)) := (C.Ass W X Y Z f g h)

#check CategoryTheory.Category.mk

def toCategory (C : category) : Category C.Obj := {Hom := C.Hom, id := C.Idn, comp := composition C, id_comp := Id₁ C, comp_id := (Id₂ C), assoc := Ass C}
#check toCategory

The functors seem a bit harder since Functor seems to take in object components and infer the category structure on its on.

[Eric Wieser]

Does changing your toCategory to an instance rather than a def help?

[Dean Young]

Yeah thanks.

I decided to just completely switch over to Mathlib's set.