∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] (x : C),
  CategoryTheory.CategoryStruct.comp
      ({
            obj := fun x =>
              match x with
              | Opposite.op x =>
                match x with
                | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x)
                | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star,
            map := fun {x y} x_1 =>
              match x_1 with
              | Opposite.op f =>
                match x, y, f, x_1 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),
            map_id := ⋯, map_comp := ⋯ }.map
        ((CategoryTheory.NatIso.ofComponents
                (fun x =>
                  match x with
                  | Opposite.op x =>
                    match x with
                    | CategoryTheory.WithInitial.of x =>
                      CategoryTheory.Iso.refl
                        ((CategoryTheory.Functor.id (CategoryTheory.WithInitial C)ᵒᵖ).obj
                          (Opposite.op (CategoryTheory.WithInitial.of x)))
                    | CategoryTheory.WithInitial.star =>
                      CategoryTheory.Iso.refl
                        ((CategoryTheory.Functor.id (CategoryTheory.WithInitial C)ᵒᵖ).obj
                          (Opposite.op CategoryTheory.WithInitial.star)))
                ⋯).hom.app
          (Opposite.op (CategoryTheory.WithInitial.of x))))
      ((CategoryTheory.NatIso.ofComponents
              (fun x =>
                match x with
                | CategoryTheory.WithTerminal.of x =>
                  CategoryTheory.Iso.refl
                    (({
                              obj := fun x =>
                                match x with
                                | CategoryTheory.WithTerminal.of x =>
                                  Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x))
                                | CategoryTheory.WithTerminal.star => Opposite.op CategoryTheory.WithInitial.star,
                              map := fun {x y} f =>
                                match x, y, f with
                                | CategoryTheory.WithTerminal.of (Opposite.op x),
                                  CategoryTheory.WithTerminal.of (Opposite.op y), f => CategoryTheory.WithInitial.down f
                                | CategoryTheory.WithTerminal.of (Opposite.op unop), CategoryTheory.WithTerminal.star,
                                  x =>
                                  Opposite.op
                                    (CategoryTheory.WithInitial.starInitial.to
                                      (Opposite.unop
                                        (match CategoryTheory.WithTerminal.of (Opposite.op unop) with
                                        | CategoryTheory.WithTerminal.of x =>
                                          Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x))
                                        | CategoryTheory.WithTerminal.star =>
                                          Opposite.op CategoryTheory.WithInitial.star)))
                                | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x =>
                                  CategoryTheory.CategoryStruct.id
                                    (match CategoryTheory.WithTerminal.star with
                                    | CategoryTheory.WithTerminal.of x =>
                                      Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x))
                                    | CategoryTheory.WithTerminal.star => Opposite.op CategoryTheory.WithInitial.star),
                              map_id := ⋯, map_comp := ⋯ }.comp
                          {
                            obj := fun x =>
                              match x with
                              | Opposite.op x =>
                                match x with
                                | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x)
                                | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star,
                            map := fun {x y} x_1 =>
                              match x_1 with
                              | Opposite.op f =>
                                match x, y, f, x_1 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),
                            map_id := ⋯, map_comp := ⋯ }).obj
                      (CategoryTheory.WithTerminal.of x))
                | CategoryTheory.WithTerminal.star =>
                  CategoryTheory.Iso.refl
                    (({
                              obj := fun x =>
                                match x with
                                | CategoryTheory.WithTerminal.of x =>
                                  Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x))
                                | CategoryTheory.WithTerminal.star => Opposite.op CategoryTheory.WithInitial.star,
                              map := fun {x y} f =>
                                match x, y, f with
                                | CategoryTheory.WithTerminal.of (Opposite.op x),
                                  CategoryTheory.WithTerminal.of (Opposite.op y), f => CategoryTheory.WithInitial.down f
                                | CategoryTheory.WithTerminal.of (Opposite.op unop), CategoryTheory.WithTerminal.star,
                                  x =>
                                  Opposite.op
                                    (CategoryTheory.WithInitial.starInitial.to
                                      (Opposite.unop
                                        (match CategoryTheory.WithTerminal.of (Opposite.op unop) with
                                        | CategoryTheory.WithTerminal.of x =>
                                          Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x))
                                        | CategoryTheory.WithTerminal.star =>
                                          Opposite.op CategoryTheory.WithInitial.star)))
                                | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x =>
                                  CategoryTheory.CategoryStruct.id
                                    (match CategoryTheory.WithTerminal.star with
                                    | CategoryTheory.WithTerminal.of x =>
                                      Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x))
                                    | CategoryTheory.WithTerminal.star => Opposite.op CategoryTheory.WithInitial.star),
                              map_id := ⋯, map_comp := ⋯ }.comp
                          {
                            obj := fun x =>
                              match x with
                              | Opposite.op x =>
                                match x with
                                | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x)
                                | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star,
                            map := fun {x y} x_1 =>
                              match x_1 with
                              | Opposite.op f =>
                                match x, y, f, x_1 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),
                            map_id := ⋯, map_comp := ⋯ }).obj
                      CategoryTheory.WithTerminal.star))
              ⋯).hom.app
        ({
              obj := fun x =>
                match x with
                | Opposite.op x =>
                  match x with
                  | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x)
                  | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star,
              map := fun {x y} x_1 =>
                match x_1 with
                | Opposite.op f =>
                  match x, y, f, x_1 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),
              map_id := ⋯, map_comp := ⋯ }.obj
          (Opposite.op (CategoryTheory.WithInitial.of x)))) =
    CategoryTheory.CategoryStruct.id
      ({
            obj := fun x =>
              match x with
              | Opposite.op x =>
                match x with
                | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x)
                | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star,
            map := fun {x y} x_1 =>
              match x_1 with
              | Opposite.op f =>
                match x, y, f, x_1 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),
            map_id := ⋯, map_comp := ⋯ }.obj
        (Opposite.op (CategoryTheory.WithInitial.of x)))