Best Practice to Form a Category (Specifically d->FC)

Stream: mathlib4

[Mason McBride]

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Functor.Basic
open CategoryTheory

namespace d_to_FC
variable {C D: Type*} [Category C] [Category D]
variable (F : C ⥤ D) (d : D)

@[ext]
structure obj where (c : C) (δ : d ⟶ F.obj c)

@[ext]
structure hom (c_δ c'_δ' : obj F d) where
  α : c_δ.c ⟶ c'_δ'.c
  comm : c_δ.δ ≫ F.map α = c'_δ'.δ

def id (c_δ : obj F d)
: hom F d c_δ c_δ where
  α := 𝟙 c_δ.c
  comm := by rw [F.map_id, Category.comp_id]

def comp {c_δ c'_δ' c''_δ'' : obj F d} (f : hom F d c_δ c'_δ') (g : hom F d c'_δ' c''_δ'')
: hom F d c_δ c''_δ'' where
  α := f.α ≫ g.α
  comm := by rw [F.map_comp, ←Category.assoc, f.comm, g.comm]

instance : CategoryStruct (obj F d) where
  Hom c_δ c'_δ' := hom F d c_δ c'_δ'
  id c_δ := id F d c_δ
  comp f g := comp F d f g

instance : Category (obj F d) where
  id_comp := by {
    intros X Y f
    sorry -- I'm getting stuck here
  }
  comp_id := sorry
  assoc := sorry
end d_to_FC

This is a general question because I want to define categories that I can use inside of my theorems. This category I'm defining for example, the coreflections of an object d across a functor F are precisely the terminal objects of this category. So I want to have the actual datatype so i can type IsTerminal, but I'm not sure about best practices.
1, do I have to define a CategoryStruct then define a Category and prove id_comp etc, in it? If so, why is proving id_comp so hard and why does f think it's a quiver hom and not a hom from my category?
2, the object d and the functor F are fixed, but if I use brackets everything breaks again why is this?

Thank you, if you enjoy questions like this feel free to answer this is merely something I'm doing on my own

[Robert Maxton]

All the fancy notation in Lean is associated with specific typeclasses; when you type f:  X ⟶ Y, that's just syntactic sugar for Quiver.Hom X Y.

[Robert Maxton]

Doing it the way you're doing it will make you write down a bunch of lemmas showing that the names hom, id, comp have the meanings you've assigned them (which are all basically by rfl but are kind of annoying to write), so that you can substitute them in (as unfold will probably not do the thing you want here); you might also get away with making them @[reducible]

[Robert Maxton]

also, for the record, this specific category already exists as docs#CategoryTheory.Comma if you want to use an existing structure

[Markus Himmel]

Robert Maxton said:

also, for the record, this specific category already exists as docs#CategoryTheory.Comma if you want to use an existing structure

See also docs#CategoryTheory.StructuredArrow for the specialization to your specific case.

[Robert Maxton]

If you instead define your homs as Subtypes inline in the Category instance itself, then aesop_cat can handle the rest:

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Functor.Basic
open CategoryTheory

namespace d_to_FC
variable {C D: Type*} [Category C] [Category D]
variable (F : C ⥤ D) (d : D)

@[ext]
structure obj where (c : C) (δ : d ⟶ F.obj c)

instance : Category (obj F d) where
  Hom c_δ c'_δ' := {h : c_δ.c ⟶ c'_δ'.c // c_δ.δ ≫ F.map h = c'_δ'.δ}
  id c_δ := ⟨𝟙 c_δ.c, by simp⟩
  comp f g := ⟨f.val ≫ g.val, by rw [Functor.map_comp, ←Category.assoc, f.2, g.2]⟩

end d_to_FC

[Robert Maxton]

(Category is defined so that all its proofs are autoParams that attempt to discharge themselves with by aesop_cat; you only have to actually provide the proofs if aesop_cat fails.)

[Robert Maxton]

Mason McBride said:

2, the object d and the functor F are fixed, but if I use brackets everything breaks again why is this?

Also, I'm not sure what you mean by "brackets" here. If you mean square brackets, that only works for typeclass instances; if you mean curly braces, that makes them implicit, which means Lean expects that you won't provide them and it'll have to infer them from other parameters, which is probably not what you're going for here.