∀ {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite))
  {X Y Z : ℕᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.StructuredArrow.homMk (F.map (CategoryTheory.CategoryStruct.comp f g)) ⋯ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.StructuredArrow.homMk (F.map f) ⋯)
      (CategoryTheory.StructuredArrow.homMk (F.map g) ⋯)