∀ {X Y Z : Type u_1} (f : X ⟶ Y) (g : Y ⟶ Z),
  (fun x => { down := CategoryTheory.CategoryStruct.comp f g x.down }) =
    CategoryTheory.CategoryStruct.comp (fun x => { down := f x.down }) fun x => { down := g x.down }