functor category

Stream: new members

[mdnestor]

Hi, I am trying to implement functor category and running into some trouble. My code is below:

structure Category where
  obj: Type
  hom (x y: obj) : Type
  id (a: obj): hom a a
  comp (f: hom a b) (g: hom b c): hom a c
  id_left (f: hom a b): comp (id a) f = f
  id_right (f: hom a b): comp f (id b) = f
  assoc: comp f (comp g h) = comp (comp f g) h

structure functor (C D: Category) where
  func0: C.obj → D.obj
  func1: C.hom x y → D.hom (func0 x) (func0 y)
  id_preserving: func1 (C.id x) = D.id (func0 x)
  comp_preserving: func1 (C.comp f g) = D.comp (func1 f) (func1 g)

structure NatTrans {C D: Category} (F G: functor C D) where
  component (x: C.obj): D.hom (F.func0 x) (G.func0 x)
  ok (f: C.hom x y): D.comp (F.func1 f) (component y) = D.comp (component x) (G.func1 f)

def NatTrans.id {C D: Category} (F: functor C D): NatTrans F F := {
  component := fun x => D.id (F.func0 x)
  ok := by
    intro x y f
    rw [D.id_right (F.func1 f), D.id_left (F.func1 f)]
}

def NatTrans.comp {C D: Category} {F G H: functor C D} (η: NatTrans F G) (μ: NatTrans G H): NatTrans F H := {
  component := fun x => D.comp (η.component x) (μ.component x)
  ok := by
    intros
    rw [D.assoc, η.ok, ←D.assoc, μ.ok, D.assoc]
}

def functorCategory (C D: Category): Category := {
  obj := functor C D
  hom := NatTrans
  id := NatTrans.id
  comp := NatTrans.comp
  id_left := by
    intro F G η
    simp [NatTrans.comp, NatTrans.id]
    -- ⊢ { component := fun x => D.comp (D.id (F.func0 x)) (η.component x), ok := ⋯ } = η
    sorry
  id_right := by
    intro F G η
    simp [NatTrans.comp, NatTrans.id]
    -- ⊢ { component := fun x => D.comp (D.id (F.func0 x)) (η.component x), ok := ⋯ } = η
    sorry
  assoc := by
    intros
    simp [NatTrans.comp]
    ext
    rw [D.assoc]
}

I have two sorrys when I need to prove the left and right identity composition laws. My goal has the form ⊢ { component := fun x => D.comp (D.id (F.func0 x)) (η.component x), ok := ⋯ } = η.

I think I need to prove two NatTrans structures are equal, so I should be able to use constructor and then prove they are equal field-by-field. For the first field, I show the component functions are equal, and then by proof irrelevance I should also have that the two ok fields are equal. But something about this approach seems wrong.

[Markus Himmel]

If you tag your NatTrans structure using @[ext], then you can use the ext tactic to show that two NatTrans are equal if they are equal field-by-field:

structure Category where
  obj: Type
  hom (x y: obj) : Type
  id (a: obj): hom a a
  comp (f: hom a b) (g: hom b c): hom a c
  id_left (f: hom a b): comp (id a) f = f
  id_right (f: hom a b): comp f (id b) = f
  assoc: comp f (comp g h) = comp (comp f g) h

structure functor (C D: Category) where
  func0: C.obj → D.obj
  func1: C.hom x y → D.hom (func0 x) (func0 y)
  id_preserving: func1 (C.id x) = D.id (func0 x)
  comp_preserving: func1 (C.comp f g) = D.comp (func1 f) (func1 g)

@[ext]
structure NatTrans {C D: Category} (F G: functor C D) where
  component (x: C.obj): D.hom (F.func0 x) (G.func0 x)
  ok (f: C.hom x y): D.comp (F.func1 f) (component y) = D.comp (component x) (G.func1 f)

def NatTrans.id {C D: Category} (F: functor C D): NatTrans F F := {
  component := fun x => D.id (F.func0 x)
  ok := by
    intro x y f
    rw [D.id_right (F.func1 f), D.id_left (F.func1 f)]
}

def NatTrans.comp {C D: Category} {F G H: functor C D} (η: NatTrans F G) (μ: NatTrans G H): NatTrans F H := {
  component := fun x => D.comp (η.component x) (μ.component x)
  ok := by
    intros
    rw [D.assoc, η.ok, ←D.assoc, μ.ok, D.assoc]
}

def functorCategory (C D: Category): Category := {
  obj := functor C D
  hom := NatTrans
  id := NatTrans.id
  comp := NatTrans.comp
  id_left := by
    intro F G η
    simp [NatTrans.comp, NatTrans.id]
    ext
    simp [functor.id_preserving, Category.id_left]
  id_right := by
    intro F G η
    simp [NatTrans.comp, NatTrans.id]
    -- ⊢ { component := fun x => D.comp (D.id (F.func0 x)) (η.component x), ok := ⋯ } = η
    sorry
  assoc := by
    intros
    simp [NatTrans.comp]
    ext
    rw [D.assoc]
}