∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {D : Type u_6} {E : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_5, u_6} D] [inst_2 : CategoryTheory.Category.{u_3, u_4} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) {X Y : CategoryTheory.WithTerminal C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.WithTerminal.map (F.comp G)).map f)
      ((fun X =>
            match X with
            | CategoryTheory.WithTerminal.of a =>
              CategoryTheory.Iso.refl
                ((CategoryTheory.WithTerminal.map (F.comp G)).obj (CategoryTheory.WithTerminal.of a))
            | CategoryTheory.WithTerminal.star =>
              CategoryTheory.Iso.refl
                ((CategoryTheory.WithTerminal.map (F.comp G)).obj CategoryTheory.WithTerminal.star))
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun X =>
            match X with
            | CategoryTheory.WithTerminal.of a =>
              CategoryTheory.Iso.refl
                ((CategoryTheory.WithTerminal.map (F.comp G)).obj (CategoryTheory.WithTerminal.of a))
            | CategoryTheory.WithTerminal.star =>
              CategoryTheory.Iso.refl
                ((CategoryTheory.WithTerminal.map (F.comp G)).obj CategoryTheory.WithTerminal.star))
          X).hom
      (((CategoryTheory.WithTerminal.map F).comp (CategoryTheory.WithTerminal.map G)).map f)