-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.biconeCategoryStruct_comp : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] {X Y Z : CategoryTheory.Bicone J}
  (f : CategoryTheory.BiconeHom J X Y) (g : CategoryTheory.BiconeHom J Y Z),
  CategoryTheory.CategoryStruct.comp f g =
    CategoryTheory.BiconeHom.casesOn (motive := fun a a_1 x => X = a → Y = a_1 → f ≍ x → CategoryTheory.BiconeHom J X Z)
      f
      (fun h =>
        Eq.ndrec (motive := fun {X} =>
          (f : CategoryTheory.BiconeHom J X Y) →
            Y = CategoryTheory.Bicone.left → f ≍ CategoryTheory.BiconeHom.left_id → CategoryTheory.BiconeHom J X Z)
          (fun f h =>
            Eq.ndrec (motive := fun {Y} =>
              CategoryTheory.BiconeHom J Y Z →
                (f : CategoryTheory.BiconeHom J CategoryTheory.Bicone.left Y) →
                  f ≍ CategoryTheory.BiconeHom.left_id → CategoryTheory.BiconeHom J CategoryTheory.Bicone.left Z)
              (fun g f h => g) ⋯ g f)
          ⋯ f)
      (fun h =>
        Eq.ndrec (motive := fun {X} =>
          (f : CategoryTheory.BiconeHom J X Y) →
            Y = CategoryTheory.Bicone.right → f ≍ CategoryTheory.BiconeHom.right_id → CategoryTheory.BiconeHom J X Z)
          (fun f h =>
            Eq.ndrec (motive := fun {Y} =>
              CategoryTheory.BiconeHom J Y Z →
                (f : CategoryTheory.BiconeHom J CategoryTheory.Bicone.right Y) →
                  f ≍ CategoryTheory.BiconeHom.right_id → CategoryTheory.BiconeHom J CategoryTheory.Bicone.right Z)
              (fun g f h => g) ⋯ g f)
          ⋯ f)
      (fun j h =>
        Eq.ndrec (motive := fun {X} =>
          (f : CategoryTheory.BiconeHom J X Y) →
            Y = CategoryTheory.Bicone.diagram j → f ≍ CategoryTheory.BiconeHom.left j → CategoryTheory.BiconeHom J X Z)
          (fun f h =>
            Eq.ndrec (motive := fun {Y} =>
              CategoryTheory.BiconeHom J Y Z →
                (f : CategoryTheory.BiconeHom J CategoryTheory.Bicone.left Y) →
                  f ≍ CategoryTheory.BiconeHom.left j → CategoryTheory.BiconeHom J CategoryTheory.Bicone.left Z)
              (fun g f h =>
                CategoryTheory.BiconeHom.casesOn (motive := fun a a_1 t =>
                  CategoryTheory.Bicone.diagram j = a →
                    Z = a_1 → g ≍ t → CategoryTheory.BiconeHom J CategoryTheory.Bicone.left Z)
                  g (fun h => False.elim ⋯) (fun h => False.elim ⋯) (fun j_1 h => False.elim ⋯)
                  (fun j_1 h => False.elim ⋯)
                  (fun {j_1 k} f h =>
                    CategoryTheory.Bicone.diagram.noConfusion h fun val_eq =>
                      Eq.ndrec (motive := fun {j_2} =>
                        (f : j_2 ⟶ k) →
                          Z = CategoryTheory.Bicone.diagram k →
                            g ≍ CategoryTheory.BiconeHom.diagram f →
                              CategoryTheory.BiconeHom J CategoryTheory.Bicone.left Z)
                        (fun f h =>
                          Eq.ndrec (motive := fun {Z} =>
                            (g : CategoryTheory.BiconeHom J (CategoryTheory.Bicone.diagram j) Z) →
                              g ≍ CategoryTheory.BiconeHom.diagram f →
                                CategoryTheory.BiconeHom J CategoryTheory.Bicone.left Z)
                            (fun g h => CategoryTheory.BiconeHom.left k) ⋯ g)
                        ⋯ f)
                  ⋯ ⋯ ⋯)
              ⋯ g f)
          ⋯ f)
      (fun j h =>
        Eq.ndrec (motive := fun {X} =>
          (f : CategoryTheory.BiconeHom J X Y) →
            Y = CategoryTheory.Bicone.diagram j → f ≍ CategoryTheory.BiconeHom.right j → CategoryTheory.BiconeHom J X Z)
          (fun f h =>
            Eq.ndrec (motive := fun {Y} =>
              CategoryTheory.BiconeHom J Y Z →
                (f : CategoryTheory.BiconeHom J CategoryTheory.Bicone.right Y) →
                  f ≍ CategoryTheory.BiconeHom.right j → CategoryTheory.BiconeHom J CategoryTheory.Bicone.right Z)
              (fun g f h =>
                CategoryTheory.BiconeHom.casesOn (motive := fun a a_1 t =>
                  CategoryTheory.Bicone.diagram j = a →
                    Z = a_1 → g ≍ t → CategoryTheory.BiconeHom J CategoryTheory.Bicone.right Z)
                  g (fun h => False.elim ⋯) (fun h => False.elim ⋯) (fun j_1 h => False.elim ⋯)
                  (fun j_1 h => False.elim ⋯)
                  (fun {j_1 k} f h =>
                    CategoryTheory.Bicone.diagram.noConfusion h fun val_eq =>
                      Eq.ndrec (motive := fun {j_2} =>
                        (f : j_2 ⟶ k) →
                          Z = CategoryTheory.Bicone.diagram k →
                            g ≍ CategoryTheory.BiconeHom.diagram f →
                              CategoryTheory.BiconeHom J CategoryTheory.Bicone.right Z)
                        (fun f h =>
                          Eq.ndrec (motive := fun {Z} =>
                            (g : CategoryTheory.BiconeHom J (CategoryTheory.Bicone.diagram j) Z) →
                              g ≍ CategoryTheory.BiconeHom.diagram f →
                                CategoryTheory.BiconeHom J CategoryTheory.Bicone.right Z)
                            (fun g h => CategoryTheory.BiconeHom.right k) ⋯ g)
                        ⋯ f)
                  ⋯ ⋯ ⋯)
              ⋯ g f)
          ⋯ f)
      (fun {j k} f_1 h =>
        Eq.ndrec (motive := fun {X} =>
          (f : CategoryTheory.BiconeHom J X Y) →
            Y = CategoryTheory.Bicone.diagram k →
              f ≍ CategoryTheory.BiconeHom.diagram f_1 → CategoryTheory.BiconeHom J X Z)
          (fun f h =>
            Eq.ndrec (motive := fun {Y} =>
              CategoryTheory.BiconeHom J Y Z →
                (f : CategoryTheory.BiconeHom J (CategoryTheory.Bicone.diagram j) Y) →
                  f ≍ CategoryTheory.BiconeHom.diagram f_1 →
                    CategoryTheory.BiconeHom J (CategoryTheory.Bicone.diagram j) Z)
              (fun g f h =>
                CategoryTheory.BiconeHom.casesOn (motive := fun a a_1 x =>
                  CategoryTheory.Bicone.diagram k = a →
                    Z = a_1 → g ≍ x → CategoryTheory.BiconeHom J (CategoryTheory.Bicone.diagram j) Z)
                  g (fun h => False.elim ⋯) (fun h => False.elim ⋯) (fun j_1 h => False.elim ⋯)
                  (fun j_1 h => False.elim ⋯)
                  (fun {j_1 k_1} g_1 h =>
                    CategoryTheory.Bicone.diagram.noConfusion h fun val_eq =>
                      Eq.ndrec (motive := fun {j_2} =>
                        (g_2 : j_2 ⟶ k_1) →
                          Z = CategoryTheory.Bicone.diagram k_1 →
                            g ≍ CategoryTheory.BiconeHom.diagram g_2 →
                              CategoryTheory.BiconeHom J (CategoryTheory.Bicone.diagram j) Z)
                        (fun g_2 h =>
                          Eq.ndrec (motive := fun {Z} =>
                            (g : CategoryTheory.BiconeHom J (CategoryTheory.Bicone.diagram k) Z) →
                              g ≍ CategoryTheory.BiconeHom.diagram g_2 →
                                CategoryTheory.BiconeHom J (CategoryTheory.Bicone.diagram j) Z)
                            (fun g h => CategoryTheory.BiconeHom.diagram (CategoryTheory.CategoryStruct.comp f_1 g_2)) ⋯
                            g)
                        ⋯ g_1)
                  ⋯ ⋯ ⋯)
              ⋯ g f)
          ⋯ f)
      ⋯ ⋯ ⋯