∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] (x x_1 : (CategoryTheory.WithInitial C)ᵒᵖ)
  (f : Opposite.unop x_1 ⟶ Opposite.unop x)
  (g : Opposite.unop (Opposite.op CategoryTheory.WithInitial.star) ⟶ Opposite.unop x_1),
  (match CategoryTheory.CategoryStruct.comp (Opposite.op f) (Opposite.op g) with
    | Opposite.op f_1 =>
      match x, Opposite.op CategoryTheory.WithInitial.star, f_1,
        CategoryTheory.CategoryStruct.comp (Opposite.op f) (Opposite.op g) with
      | Opposite.op (CategoryTheory.WithInitial.of x), Opposite.op (CategoryTheory.WithInitial.of y), f, x_2 =>
        (CategoryTheory.WithTerminal.down f).op
      | Opposite.op (CategoryTheory.WithInitial.of a), Opposite.op CategoryTheory.WithInitial.star, x, x_2 =>
        CategoryTheory.WithTerminal.starTerminal.from
          (match Opposite.op (CategoryTheory.WithInitial.of a) with
          | Opposite.op x =>
            match x with
            | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x)
            | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star)
      | Opposite.op CategoryTheory.WithInitial.star, Opposite.op CategoryTheory.WithInitial.star, x, x_2 =>
        CategoryTheory.CategoryStruct.id
          (match Opposite.op CategoryTheory.WithInitial.star with
          | Opposite.op x =>
            match x with
            | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x)
            | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star)) =
    CategoryTheory.CategoryStruct.comp
      (match Opposite.op f with
      | Opposite.op f_1 =>
        match x, x_1, f_1, Opposite.op f with
        | Opposite.op (CategoryTheory.WithInitial.of x), Opposite.op (CategoryTheory.WithInitial.of y), f, x_2 =>
          (CategoryTheory.WithTerminal.down f).op
        | Opposite.op (CategoryTheory.WithInitial.of a), Opposite.op CategoryTheory.WithInitial.star, x, x_2 =>
          CategoryTheory.WithTerminal.starTerminal.from
            (match Opposite.op (CategoryTheory.WithInitial.of a) with
            | Opposite.op x =>
              match x with
              | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x)
              | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star)
        | Opposite.op CategoryTheory.WithInitial.star, Opposite.op CategoryTheory.WithInitial.star, x, x_2 =>
          CategoryTheory.CategoryStruct.id
            (match Opposite.op CategoryTheory.WithInitial.star with
            | Opposite.op x =>
              match x with
              | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x)
              | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star))
      (match Opposite.op g with
      | Opposite.op f =>
        match x_1, Opposite.op CategoryTheory.WithInitial.star, f, Opposite.op g with
        | Opposite.op (CategoryTheory.WithInitial.of x), Opposite.op (CategoryTheory.WithInitial.of y), f, x_2 =>
          (CategoryTheory.WithTerminal.down f).op
        | Opposite.op (CategoryTheory.WithInitial.of a), Opposite.op CategoryTheory.WithInitial.star, x, x_2 =>
          CategoryTheory.WithTerminal.starTerminal.from
            (match Opposite.op (CategoryTheory.WithInitial.of a) with
            | Opposite.op x =>
              match x with
              | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x)
              | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star)
        | Opposite.op CategoryTheory.WithInitial.star, Opposite.op CategoryTheory.WithInitial.star, x, x_2 =>
          CategoryTheory.CategoryStruct.id
            (match Opposite.op CategoryTheory.WithInitial.star with
            | Opposite.op x =>
              match x with
              | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x)
              | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star))