-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Bicones (goal)
Goal:
J : Type v₁
inst : SmallCategory J
C : Type u₁
inst_1 : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
X Y Z : Bicone J
f : X ⟶ Y
g : Y ⟶ Z
left_id :
  ∀ (g : Bicone.left ⟶ Z),
    Eq (α :=
      Quiver.Hom.{v₁, u₁} (V := C)
        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
      (@BiconeHom.casesOn _ _
          (fun (a a_1 : Bicone J) (x : BiconeHom J a a_1) ↦
            (h : Bicone.left = a) →
              (h : Z = a_1) →
                (h : HEq (α := Bicone.left ⟶ Z) (BiconeHom.left_id ≫ g) x) →
                  Quiver.Hom.{v₁, u₁} (V := C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j :
                      C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
          Bicone.left _ (BiconeHom.left_id ≫ g)
          (fun (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.left Bicone.left) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f : X ⟶ Z) →
                (h : Z = Bicone.left) →
                  (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
              (fun (f : Bicone.left ⟶ Z) (h : Z = Bicone.left) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f : Bicone.left ⟶ Y) →
                    (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f : Quiver.Hom (V := Bicone J) Bicone.left Bicone.left)
                      (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) ↦
                    𝟙 (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j))
                  ⋯ f)
              ⋯ (BiconeHom.left_id ≫ g))
          (fun (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.left Bicone.right) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f : X ⟶ Z) →
                (h : Z = Bicone.right) →
                  (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
              (fun (f : Bicone.right ⟶ Z) (h : Z = Bicone.right) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f : Bicone.right ⟶ Y) →
                    (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f : Quiver.Hom (V := Bicone J) Bicone.right Bicone.right)
                      (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) ↦
                    𝟙
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                        F.obj j))
                  ⋯ f)
              ⋯ (BiconeHom.left_id ≫ g))
          (fun (j : J) (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.left Bicone.left) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f : X ⟶ Z) →
                (h : Z = Bicone.diagram j) →
                  (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
              (fun (f : Bicone.left ⟶ Z) (h : Z = Bicone.diagram j) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f : Bicone.left ⟶ Y) →
                    (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f : Bicone.left ⟶ Bicone.diagram j)
                      (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) ↦
                    c₁.π.app j)
                  ⋯ f)
              ⋯ (BiconeHom.left_id ≫ g))
          (fun (j : J) (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.left Bicone.right) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f : X ⟶ Z) →
                (h : Z = Bicone.diagram j) →
                  (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
              (fun (f : Bicone.right ⟶ Z) (h : Z = Bicone.diagram j) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f : Bicone.right ⟶ Y) →
                    (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f : Bicone.right ⟶ Bicone.diagram j)
                      (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) ↦
                    c₂.π.app j)
                  ⋯ f)
              ⋯ (BiconeHom.left_id ≫ g))
          (fun {j k : J} (f : j ⟶ k) (h : Bicone.left = Bicone.diagram j) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f_1 : X ⟶ Z) →
                (h : Z = Bicone.diagram k) →
                  (h : f_1 ≍ BiconeHom.diagram f) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
              (fun (f_1 : Bicone.diagram j ⟶ Z) (h : Z = Bicone.diagram k) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f_2 : Bicone.diagram j ⟶ Y) →
                    (h : f_2 ≍ BiconeHom.diagram f) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) (Bicone.diagram j) c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f_2 : Bicone.diagram j ⟶ Bicone.diagram k) (h : f_2 ≍ BiconeHom.diagram f) ↦ F.map f) ⋯ f_1)
              ⋯ (BiconeHom.left_id ≫ g))
          ⋯ ⋯ ⋯ :
        Quiver.Hom.{v₁, u₁} (V := C)
          (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
          (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
      (CategoryStruct.comp (Y :=
          Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j)
          (BiconeHom.casesOn (motive := fun (a a_1 : Bicone J) (x : BiconeHom J a a_1) ↦
            (h : Bicone.left = a) →
              (h : Bicone.left = a_1) →
                (h : HEq (α := Quiver.Hom (V := Bicone J) Bicone.left Bicone.left) BiconeHom.left_id x) →
                  Quiver.Hom.{v₁, u₁} (V := C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j :
                      C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j :
                      C))
            BiconeHom.left_id
            (fun (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.left Bicone.left) ↦
              Eq.ndrec (motive := fun {X : Bicone J} ↦
                (f : X ⟶ Bicone.left) →
                  (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.left Bicone.left) →
                    (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C))
                (fun (f : Quiver.Hom (V := Bicone J) Bicone.left Bicone.left)
                    (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.left Bicone.left) ↦
                  Eq.ndrec (motive := fun {Y : Bicone J} ↦
                    (f : Bicone.left ⟶ Y) →
                      (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) →
                        Quiver.Hom.{v₁, u₁} (V := C)
                          (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦
                              F.obj j :
                            C)
                          (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                    (fun (f : Quiver.Hom (V := Bicone J) Bicone.left Bicone.left)
                        (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) ↦
                      𝟙
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦
                          F.obj j))
                    ⋯ f)
                ⋯ BiconeHom.left_id)
            (fun (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.left Bicone.right) ↦
              Eq.ndrec (motive := fun {X : Bicone J} ↦
                (f : X ⟶ Bicone.left) →
                  (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.left Bicone.right) →
                    (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C))
                (fun (f : Quiver.Hom (V := Bicone J) Bicone.right Bicone.left)
                    (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.left Bicone.right) ↦
                  Eq.ndrec (motive := fun {Y : Bicone J} ↦
                    (f : Bicone.right ⟶ Y) →
                      (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) →
                        Quiver.Hom.{v₁, u₁} (V := C)
                          (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                              F.obj j :
                            C)
                          (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                    (fun (f : Quiver.Hom (V := Bicone J) Bicone.right Bicone.right)
                        (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) ↦
                      𝟙
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                          F.obj j))
                    ⋯ f)
                ⋯ BiconeHom.left_id)
            (fun (j : J) (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.left Bicone.left) ↦
              Eq.ndrec (motive := fun {X : Bicone J} ↦
                (f : X ⟶ Bicone.left) →
                  (h : Bicone.left = Bicone.diagram j) →
                    (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C))
                (fun (f : Quiver.Hom (V := Bicone J) Bicone.left Bicone.left) (h : Bicone.left = Bicone.diagram j) ↦
                  Eq.ndrec (motive := fun {Y : Bicone J} ↦
                    (f : Bicone.left ⟶ Y) →
                      (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) →
                        Quiver.Hom.{v₁, u₁} (V := C)
                          (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦
                              F.obj j :
                            C)
                          (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                    (fun (f : Bicone.left ⟶ Bicone.diagram j)
                        (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) ↦
                      c₁.π.app j)
                    ⋯ f)
                ⋯ BiconeHom.left_id)
            (fun (j : J) (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.left Bicone.right) ↦
              Eq.ndrec (motive := fun {X : Bicone J} ↦
                (f : X ⟶ Bicone.left) →
                  (h : Bicone.left = Bicone.diagram j) →
                    (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C))
                (fun (f : Quiver.Hom (V := Bicone J) Bicone.right Bicone.left) (h : Bicone.left = Bicone.diagram j) ↦
                  Eq.ndrec (motive := fun {Y : Bicone J} ↦
                    (f : Bicone.right ⟶ Y) →
                      (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) →
                        Quiver.Hom.{v₁, u₁} (V := C)
                          (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                              F.obj j :
                            C)
                          (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                    (fun (f : Bicone.right ⟶ Bicone.diagram j)
                        (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) ↦
                      c₂.π.app j)
                    ⋯ f)
                ⋯ BiconeHom.left_id)
            (fun {j k : J} (f : j ⟶ k) (h : Bicone.left = Bicone.diagram j) ↦
              Eq.ndrec (motive := fun {X : Bicone J} ↦
                (f_1 : X ⟶ Bicone.left) →
                  (h : Bicone.left = Bicone.diagram k) →
                    (h : f_1 ≍ BiconeHom.diagram f) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C))
                (fun (f_1 : Bicone.diagram j ⟶ Bicone.left) (h : Bicone.left = Bicone.diagram k) ↦
                  Eq.ndrec (motive := fun {Y : Bicone J} ↦
                    (f_2 : Bicone.diagram j ⟶ Y) →
                      (h : f_2 ≍ BiconeHom.diagram f) →
                        Quiver.Hom.{v₁, u₁} (V := C)
                          (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) (Bicone.diagram j) c₁.pt c₂.pt
                              fun (j : J) ↦ F.obj j :
                            C)
                          (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                    (fun (f_2 : Bicone.diagram j ⟶ Bicone.diagram k) (h : f_2 ≍ BiconeHom.diagram f) ↦ F.map f) ⋯ f_1)
                ⋯ BiconeHom.left_id)
            ⋯ ⋯ ⋯)
          (BiconeHom.casesOn (motive := fun (a a_1 : Bicone J) (x : BiconeHom J a a_1) ↦
            (h : Bicone.left = a) →
              (h : Z = a_1) →
                (h : g ≍ x) →
                  Quiver.Hom.{v₁, u₁} (V := C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j :
                      C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
            g
            (fun (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.left Bicone.left) ↦
              Eq.ndrec (motive := fun {X : Bicone J} ↦
                (f : X ⟶ Z) →
                  (h : Z = Bicone.left) →
                    (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                (fun (f : Bicone.left ⟶ Z) (h : Z = Bicone.left) ↦
                  Eq.ndrec (motive := fun {Y : Bicone J} ↦
                    (f : Bicone.left ⟶ Y) →
                      (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) →
                        Quiver.Hom.{v₁, u₁} (V := C)
                          (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦
                              F.obj j :
                            C)
                          (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                    (fun (f : Quiver.Hom (V := Bicone J) Bicone.left Bicone.left)
                        (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) ↦
                      𝟙
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦
                          F.obj j))
                    ⋯ f)
                ⋯ g)
            (fun (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.left Bicone.right) ↦
              Eq.ndrec (motive := fun {X : Bicone J} ↦
                (f : X ⟶ Z) →
                  (h : Z = Bicone.right) →
                    (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                (fun (f : Bicone.right ⟶ Z) (h : Z = Bicone.right) ↦
                  Eq.ndrec (motive := fun {Y : Bicone J} ↦
                    (f : Bicone.right ⟶ Y) →
                      (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) →
                        Quiver.Hom.{v₁, u₁} (V := C)
                          (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                              F.obj j :
                            C)
                          (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                    (fun (f : Quiver.Hom (V := Bicone J) Bicone.right Bicone.right)
                        (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) ↦
                      𝟙
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                          F.obj j))
                    ⋯ f)
                ⋯ g)
            (fun (j : J) (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.left Bicone.left) ↦
              Eq.ndrec (motive := fun {X : Bicone J} ↦
                (f : X ⟶ Z) →
                  (h : Z = Bicone.diagram j) →
                    (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                (fun (f : Bicone.left ⟶ Z) (h : Z = Bicone.diagram j) ↦
                  Eq.ndrec (motive := fun {Y : Bicone J} ↦
                    (f : Bicone.left ⟶ Y) →
                      (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) →
                        Quiver.Hom.{v₁, u₁} (V := C)
                          (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦
                              F.obj j :
                            C)
                          (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                    (fun (f : Bicone.left ⟶ Bicone.diagram j)
                        (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) ↦
                      c₁.π.app j)
                    ⋯ f)
                ⋯ g)
            (fun (j : J) (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.left Bicone.right) ↦
              Eq.ndrec (motive := fun {X : Bicone J} ↦
                (f : X ⟶ Z) →
                  (h : Z = Bicone.diagram j) →
                    (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                (fun (f : Bicone.right ⟶ Z) (h : Z = Bicone.diagram j) ↦
                  Eq.ndrec (motive := fun {Y : Bicone J} ↦
                    (f : Bicone.right ⟶ Y) →
                      (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) →
                        Quiver.Hom.{v₁, u₁} (V := C)
                          (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                              F.obj j :
                            C)
                          (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                    (fun (f : Bicone.right ⟶ Bicone.diagram j)
                        (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) ↦
                      c₂.π.app j)
                    ⋯ f)
                ⋯ g)
            (fun {j k : J} (f : j ⟶ k) (h : Bicone.left = Bicone.diagram j) ↦
              Eq.ndrec (motive := fun {X : Bicone J} ↦
                (f_1 : X ⟶ Z) →
                  (h : Z = Bicone.diagram k) →
                    (h : f_1 ≍ BiconeHom.diagram f) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                (fun (f_1 : Bicone.diagram j ⟶ Z) (h : Z = Bicone.diagram k) ↦
                  Eq.ndrec (motive := fun {Y : Bicone J} ↦
                    (f_2 : Bicone.diagram j ⟶ Y) →
                      (h : f_2 ≍ BiconeHom.diagram f) →
                        Quiver.Hom.{v₁, u₁} (V := C)
                          (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) (Bicone.diagram j) c₁.pt c₂.pt
                              fun (j : J) ↦ F.obj j :
                            C)
                          (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                    (fun (f_2 : Bicone.diagram j ⟶ Bicone.diagram k) (h : f_2 ≍ BiconeHom.diagram f) ↦ F.map f) ⋯ f_1)
                ⋯ g)
            ⋯ ⋯ ⋯) :
        Quiver.Hom.{v₁, u₁} (V := C)
          (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
          (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
⊢ Eq (α :=
    Quiver.Hom.{v₁, u₁} (V := C)
      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
    (BiconeHom.casesOn (motive := fun (a a_1 : Bicone J) (x : BiconeHom J a a_1) ↦
        (h : X = a) →
          (h : Z = a_1) →
            (h : f ≫ g ≍ x) →
              Quiver.Hom.{v₁, u₁} (V := C)
                (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
        (f ≫ g)
        (fun (h : X = Bicone.left) ↦
          Eq.ndrec (motive := fun {X : Bicone J} ↦
            (f : X ⟶ Z) →
              (h : Z = Bicone.left) →
                (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) →
                  Quiver.Hom.{v₁, u₁} (V := C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
            (fun (f : Bicone.left ⟶ Z) (h : Z = Bicone.left) ↦
              Eq.ndrec (motive := fun {Y : Bicone J} ↦
                (f : Bicone.left ⟶ Y) →
                  (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j :
                        C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                (fun (f : Quiver.Hom (V := Bicone J) Bicone.left Bicone.left)
                    (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) ↦
                  𝟙 (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j))
                ⋯ f)
            ⋯ (f ≫ g))
        (fun (h : X = Bicone.right) ↦
          Eq.ndrec (motive := fun {X : Bicone J} ↦
            (f : X ⟶ Z) →
              (h : Z = Bicone.right) →
                (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) →
                  Quiver.Hom.{v₁, u₁} (V := C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
            (fun (f : Bicone.right ⟶ Z) (h : Z = Bicone.right) ↦
              Eq.ndrec (motive := fun {Y : Bicone J} ↦
                (f : Bicone.right ⟶ Y) →
                  (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                          F.obj j :
                        C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                (fun (f : Quiver.Hom (V := Bicone J) Bicone.right Bicone.right)
                    (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) ↦
                  𝟙 (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦ F.obj j))
                ⋯ f)
            ⋯ (f ≫ g))
        (fun (j : J) (h : X = Bicone.left) ↦
          Eq.ndrec (motive := fun {X : Bicone J} ↦
            (f : X ⟶ Z) →
              (h : Z = Bicone.diagram j) →
                (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) →
                  Quiver.Hom.{v₁, u₁} (V := C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
            (fun (f : Bicone.left ⟶ Z) (h : Z = Bicone.diagram j) ↦
              Eq.ndrec (motive := fun {Y : Bicone J} ↦
                (f : Bicone.left ⟶ Y) →
                  (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j :
                        C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                (fun (f : Bicone.left ⟶ Bicone.diagram j)
                    (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) ↦
                  c₁.π.app j)
                ⋯ f)
            ⋯ (f ≫ g))
        (fun (j : J) (h : X = Bicone.right) ↦
          Eq.ndrec (motive := fun {X : Bicone J} ↦
            (f : X ⟶ Z) →
              (h : Z = Bicone.diagram j) →
                (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) →
                  Quiver.Hom.{v₁, u₁} (V := C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
            (fun (f : Bicone.right ⟶ Z) (h : Z = Bicone.diagram j) ↦
              Eq.ndrec (motive := fun {Y : Bicone J} ↦
                (f : Bicone.right ⟶ Y) →
                  (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                          F.obj j :
                        C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                (fun (f : Bicone.right ⟶ Bicone.diagram j)
                    (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) ↦
                  c₂.π.app j)
                ⋯ f)
            ⋯ (f ≫ g))
        (fun {j k : J} (f_1 : j ⟶ k) (h : X = Bicone.diagram j) ↦
          Eq.ndrec (motive := fun {X : Bicone J} ↦
            (f : X ⟶ Z) →
              (h : Z = Bicone.diagram k) →
                (h : f ≍ BiconeHom.diagram f_1) →
                  Quiver.Hom.{v₁, u₁} (V := C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
            (fun (f : Bicone.diagram j ⟶ Z) (h : Z = Bicone.diagram k) ↦
              Eq.ndrec (motive := fun {Y : Bicone J} ↦
                (f : Bicone.diagram j ⟶ Y) →
                  (h : f ≍ BiconeHom.diagram f_1) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) (Bicone.diagram j) c₁.pt c₂.pt fun (j : J) ↦
                          F.obj j :
                        C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                (fun (f : Bicone.diagram j ⟶ Bicone.diagram k) (h : f ≍ BiconeHom.diagram f_1) ↦ F.map f_1) ⋯ f)
            ⋯ (f ≫ g))
        ⋯ ⋯ ⋯ :
      Quiver.Hom.{v₁, u₁} (V := C)
        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
    (CategoryStruct.comp (Y := Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j)
        (BiconeHom.casesOn (motive := fun (a a_1 : Bicone J) (x : BiconeHom J a a_1) ↦
          (h : X = a) →
            (h : Y = a_1) →
              (h : f ≍ x) →
                Quiver.Hom.{v₁, u₁} (V := C)
                  (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                  (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
          f
          (fun (h : X = Bicone.left) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f : X ⟶ Y) →
                (h : Y = Bicone.left) →
                  (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
              (fun (f : Bicone.left ⟶ Y) (h : Y = Bicone.left) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f : Bicone.left ⟶ Y) →
                    (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f : Quiver.Hom (V := Bicone J) Bicone.left Bicone.left)
                      (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) ↦
                    𝟙 (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j))
                  ⋯ f)
              ⋯ f)
          (fun (h : X = Bicone.right) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f : X ⟶ Y) →
                (h : Y = Bicone.right) →
                  (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
              (fun (f : Bicone.right ⟶ Y) (h : Y = Bicone.right) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f : Bicone.right ⟶ Y) →
                    (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f : Quiver.Hom (V := Bicone J) Bicone.right Bicone.right)
                      (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) ↦
                    𝟙
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                        F.obj j))
                  ⋯ f)
              ⋯ f)
          (fun (j : J) (h : X = Bicone.left) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f : X ⟶ Y) →
                (h : Y = Bicone.diagram j) →
                  (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
              (fun (f : Bicone.left ⟶ Y) (h : Y = Bicone.diagram j) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f : Bicone.left ⟶ Y) →
                    (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f : Bicone.left ⟶ Bicone.diagram j)
                      (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) ↦
                    c₁.π.app j)
                  ⋯ f)
              ⋯ f)
          (fun (j : J) (h : X = Bicone.right) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f : X ⟶ Y) →
                (h : Y = Bicone.diagram j) →
                  (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
              (fun (f : Bicone.right ⟶ Y) (h : Y = Bicone.diagram j) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f : Bicone.right ⟶ Y) →
                    (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f : Bicone.right ⟶ Bicone.diagram j)
                      (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) ↦
                    c₂.π.app j)
                  ⋯ f)
              ⋯ f)
          (fun {j k : J} (f_1 : j ⟶ k) (h : X = Bicone.diagram j) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f : X ⟶ Y) →
                (h : Y = Bicone.diagram k) →
                  (h : f ≍ BiconeHom.diagram f_1) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
              (fun (f : Bicone.diagram j ⟶ Y) (h : Y = Bicone.diagram k) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f : Bicone.diagram j ⟶ Y) →
                    (h : f ≍ BiconeHom.diagram f_1) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) (Bicone.diagram j) c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f : Bicone.diagram j ⟶ Bicone.diagram k) (h : f ≍ BiconeHom.diagram f_1) ↦ F.map f_1) ⋯ f)
              ⋯ f)
          ⋯ ⋯ ⋯)
        (BiconeHom.casesOn (motive := fun (a a_1 : Bicone J) (x : BiconeHom J a a_1) ↦
          (h : Y = a) →
            (h : Z = a_1) →
              (h : g ≍ x) →
                Quiver.Hom.{v₁, u₁} (V := C)
                  (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                  (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
          g
          (fun (h : Y = Bicone.left) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f : X ⟶ Z) →
                (h : Z = Bicone.left) →
                  (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
              (fun (f : Bicone.left ⟶ Z) (h : Z = Bicone.left) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f : Bicone.left ⟶ Y) →
                    (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f : Quiver.Hom (V := Bicone J) Bicone.left Bicone.left)
                      (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) ↦
                    𝟙 (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j))
                  ⋯ f)
              ⋯ g)
          (fun (h : Y = Bicone.right) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f : X ⟶ Z) →
                (h : Z = Bicone.right) →
                  (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
              (fun (f : Bicone.right ⟶ Z) (h : Z = Bicone.right) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f : Bicone.right ⟶ Y) →
                    (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f : Quiver.Hom (V := Bicone J) Bicone.right Bicone.right)
                      (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) ↦
                    𝟙
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                        F.obj j))
                  ⋯ f)
              ⋯ g)
          (fun (j : J) (h : Y = Bicone.left) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f : X ⟶ Z) →
                (h : Z = Bicone.diagram j) →
                  (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
              (fun (f : Bicone.left ⟶ Z) (h : Z = Bicone.diagram j) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f : Bicone.left ⟶ Y) →
                    (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f : Bicone.left ⟶ Bicone.diagram j)
                      (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) ↦
                    c₁.π.app j)
                  ⋯ f)
              ⋯ g)
          (fun (j : J) (h : Y = Bicone.right) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f : X ⟶ Z) →
                (h : Z = Bicone.diagram j) →
                  (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
              (fun (f : Bicone.right ⟶ Z) (h : Z = Bicone.diagram j) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f : Bicone.right ⟶ Y) →
                    (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f : Bicone.right ⟶ Bicone.diagram j)
                      (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) ↦
                    c₂.π.app j)
                  ⋯ f)
              ⋯ g)
          (fun {j k : J} (f : j ⟶ k) (h : Y = Bicone.diagram j) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f_1 : X ⟶ Z) →
                (h : Z = Bicone.diagram k) →
                  (h : f_1 ≍ BiconeHom.diagram f) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
              (fun (f_1 : Bicone.diagram j ⟶ Z) (h : Z = Bicone.diagram k) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f_2 : Bicone.diagram j ⟶ Y) →
                    (h : f_2 ≍ BiconeHom.diagram f) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) (Bicone.diagram j) c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f_2 : Bicone.diagram j ⟶ Bicone.diagram k) (h : f_2 ≍ BiconeHom.diagram f) ↦ F.map f) ⋯ f_1)
              ⋯ g)
          ⋯ ⋯ ⋯) :
      Quiver.Hom.{v₁, u₁} (V := C)
        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
have right_id : ∀ (g : Bicone.right ⟶ Z),
  Eq (α :=
    Quiver.Hom.{v₁, u₁} (V := C)
      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
    (@BiconeHom.casesOn _ _
        (fun (a a_1 : Bicone J) (x : BiconeHom J a a_1) ↦
          (h : Bicone.right = a) →
            (h : Z = a_1) →
              (h : HEq (α := Bicone.right ⟶ Z) (BiconeHom.right_id ≫ g) x) →
                Quiver.Hom.{v₁, u₁} (V := C)
                  (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                  (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
        Bicone.right _ (BiconeHom.right_id ≫ g)
        (fun (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.right Bicone.left) ↦
          Eq.ndrec (motive := fun {X : Bicone J} ↦
            (f : X ⟶ Z) →
              (h : Z = Bicone.left) →
                (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) →
                  Quiver.Hom.{v₁, u₁} (V := C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
            (fun (f : Bicone.left ⟶ Z) (h : Z = Bicone.left) ↦
              Eq.ndrec (motive := fun {Y : Bicone J} ↦
                (f : Bicone.left ⟶ Y) →
                  (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j :
                        C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                (fun (f : Quiver.Hom (V := Bicone J) Bicone.left Bicone.left)
                    (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) ↦
                  𝟙 (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j))
                sorry f)
            sorry (BiconeHom.right_id ≫ g))
        (fun (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.right Bicone.right) ↦
          Eq.ndrec (motive := fun {X : Bicone J} ↦
            (f : X ⟶ Z) →
              (h : Z = Bicone.right) →
                (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) →
                  Quiver.Hom.{v₁, u₁} (V := C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
            (fun (f : Bicone.right ⟶ Z) (h : Z = Bicone.right) ↦
              Eq.ndrec (motive := fun {Y : Bicone J} ↦
                (f : Bicone.right ⟶ Y) →
                  (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                          F.obj j :
                        C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                (fun (f : Quiver.Hom (V := Bicone J) Bicone.right Bicone.right)
                    (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) ↦
                  𝟙 (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦ F.obj j))
                sorry f)
            sorry (BiconeHom.right_id ≫ g))
        (fun (j : J) (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.right Bicone.left) ↦
          Eq.ndrec (motive := fun {X : Bicone J} ↦
            (f : X ⟶ Z) →
              (h : Z = Bicone.diagram j) →
                (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) →
                  Quiver.Hom.{v₁, u₁} (V := C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
            (fun (f : Bicone.left ⟶ Z) (h : Z = Bicone.diagram j) ↦
              Eq.ndrec (motive := fun {Y : Bicone J} ↦
                (f : Bicone.left ⟶ Y) →
                  (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j :
                        C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                (fun (f : Bicone.left ⟶ Bicone.diagram j)
                    (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) ↦
                  c₁.π.app j)
                sorry f)
            sorry (BiconeHom.right_id ≫ g))
        (fun (j : J) (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.right Bicone.right) ↦
          Eq.ndrec (motive := fun {X : Bicone J} ↦
            (f : X ⟶ Z) →
              (h : Z = Bicone.diagram j) →
                (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) →
                  Quiver.Hom.{v₁, u₁} (V := C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
            (fun (f : Bicone.right ⟶ Z) (h : Z = Bicone.diagram j) ↦
              Eq.ndrec (motive := fun {Y : Bicone J} ↦
                (f : Bicone.right ⟶ Y) →
                  (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                          F.obj j :
                        C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                (fun (f : Bicone.right ⟶ Bicone.diagram j)
                    (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) ↦
                  c₂.π.app j)
                sorry f)
            sorry (BiconeHom.right_id ≫ g))
        (fun {j k : J} (f : j ⟶ k) (h : Bicone.right = Bicone.diagram j) ↦
          Eq.ndrec (motive := fun {X : Bicone J} ↦
            (f_1 : X ⟶ Z) →
              (h : Z = Bicone.diagram k) →
                (h : f_1 ≍ BiconeHom.diagram f) →
                  Quiver.Hom.{v₁, u₁} (V := C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                    (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
            (fun (f_1 : Bicone.diagram j ⟶ Z) (h : Z = Bicone.diagram k) ↦
              Eq.ndrec (motive := fun {Y : Bicone J} ↦
                (f_2 : Bicone.diagram j ⟶ Y) →
                  (h : f_2 ≍ BiconeHom.diagram f) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) (Bicone.diagram j) c₁.pt c₂.pt fun (j : J) ↦
                          F.obj j :
                        C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                (fun (f_2 : Bicone.diagram j ⟶ Bicone.diagram k) (h : f_2 ≍ BiconeHom.diagram f) ↦ F.map f) sorry f_1)
            sorry (BiconeHom.right_id ≫ g))
        sorry sorry sorry :
      Quiver.Hom.{v₁, u₁} (V := C)
        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
    (CategoryStruct.comp (Y :=
        Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦ F.obj j)
        (BiconeHom.casesOn (motive := fun (a a_1 : Bicone J) (x : BiconeHom J a a_1) ↦
          (h : Bicone.right = a) →
            (h : Bicone.right = a_1) →
              (h : HEq (α := Quiver.Hom (V := Bicone J) Bicone.right Bicone.right) BiconeHom.right_id x) →
                Quiver.Hom.{v₁, u₁} (V := C)
                  (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                  (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦ F.obj j :
                    C))
          BiconeHom.right_id
          (fun (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.right Bicone.left) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f : X ⟶ Bicone.right) →
                (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.right Bicone.left) →
                  (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                          F.obj j :
                        C))
              (fun (f : Quiver.Hom (V := Bicone J) Bicone.left Bicone.right)
                  (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.right Bicone.left) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f : Bicone.left ⟶ Y) →
                    (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f : Quiver.Hom (V := Bicone J) Bicone.left Bicone.left)
                      (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) ↦
                    𝟙 (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j))
                  sorry f)
              sorry BiconeHom.right_id)
          (fun (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.right Bicone.right) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f : X ⟶ Bicone.right) →
                (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.right Bicone.right) →
                  (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                          F.obj j :
                        C))
              (fun (f : Quiver.Hom (V := Bicone J) Bicone.right Bicone.right)
                  (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.right Bicone.right) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f : Bicone.right ⟶ Y) →
                    (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f : Quiver.Hom (V := Bicone J) Bicone.right Bicone.right)
                      (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) ↦
                    𝟙
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                        F.obj j))
                  sorry f)
              sorry BiconeHom.right_id)
          (fun (j : J) (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.right Bicone.left) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f : X ⟶ Bicone.right) →
                (h : Bicone.right = Bicone.diagram j) →
                  (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                          F.obj j :
                        C))
              (fun (f : Quiver.Hom (V := Bicone J) Bicone.left Bicone.right) (h : Bicone.right = Bicone.diagram j) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f : Bicone.left ⟶ Y) →
                    (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f : Bicone.left ⟶ Bicone.diagram j)
                      (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) ↦
                    c₁.π.app j)
                  sorry f)
              sorry BiconeHom.right_id)
          (fun (j : J) (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.right Bicone.right) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f : X ⟶ Bicone.right) →
                (h : Bicone.right = Bicone.diagram j) →
                  (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                          F.obj j :
                        C))
              (fun (f : Quiver.Hom (V := Bicone J) Bicone.right Bicone.right) (h : Bicone.right = Bicone.diagram j) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f : Bicone.right ⟶ Y) →
                    (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f : Bicone.right ⟶ Bicone.diagram j)
                      (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) ↦
                    c₂.π.app j)
                  sorry f)
              sorry BiconeHom.right_id)
          (fun {j k : J} (f : j ⟶ k) (h : Bicone.right = Bicone.diagram j) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f_1 : X ⟶ Bicone.right) →
                (h : Bicone.right = Bicone.diagram k) →
                  (h : f_1 ≍ BiconeHom.diagram f) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                          F.obj j :
                        C))
              (fun (f_1 : Bicone.diagram j ⟶ Bicone.right) (h : Bicone.right = Bicone.diagram k) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f_2 : Bicone.diagram j ⟶ Y) →
                    (h : f_2 ≍ BiconeHom.diagram f) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) (Bicone.diagram j) c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f_2 : Bicone.diagram j ⟶ Bicone.diagram k) (h : f_2 ≍ BiconeHom.diagram f) ↦ F.map f) sorry f_1)
              sorry BiconeHom.right_id)
          sorry sorry sorry)
        (BiconeHom.casesOn (motive := fun (a a_1 : Bicone J) (x : BiconeHom J a a_1) ↦
          (h : Bicone.right = a) →
            (h : Z = a_1) →
              (h : g ≍ x) →
                Quiver.Hom.{v₁, u₁} (V := C)
                  (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                  (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
          g
          (fun (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.right Bicone.left) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f : X ⟶ Z) →
                (h : Z = Bicone.left) →
                  (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
              (fun (f : Bicone.left ⟶ Z) (h : Z = Bicone.left) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f : Bicone.left ⟶ Y) →
                    (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f : Quiver.Hom (V := Bicone J) Bicone.left Bicone.left)
                      (h : HEq f (β := BiconeHom J Bicone.left Bicone.left) BiconeHom.left_id) ↦
                    𝟙 (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦ F.obj j))
                  sorry f)
              sorry g)
          (fun (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.right Bicone.right) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f : X ⟶ Z) →
                (h : Z = Bicone.right) →
                  (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
              (fun (f : Bicone.right ⟶ Z) (h : Z = Bicone.right) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f : Bicone.right ⟶ Y) →
                    (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f : Quiver.Hom (V := Bicone J) Bicone.right Bicone.right)
                      (h : HEq f (β := BiconeHom J Bicone.right Bicone.right) BiconeHom.right_id) ↦
                    𝟙
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                        F.obj j))
                  sorry f)
              sorry g)
          (fun (j : J) (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.right Bicone.left) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f : X ⟶ Z) →
                (h : Z = Bicone.diagram j) →
                  (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
              (fun (f : Bicone.left ⟶ Z) (h : Z = Bicone.diagram j) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f : Bicone.left ⟶ Y) →
                    (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.left c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f : Bicone.left ⟶ Bicone.diagram j)
                      (h : HEq f (β := BiconeHom J Bicone.left (Bicone.diagram j)) (BiconeHom.left j)) ↦
                    c₁.π.app j)
                  sorry f)
              sorry g)
          (fun (j : J) (h : Eq.{v₁ + 1} (α := Bicone J) Bicone.right Bicone.right) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f : X ⟶ Z) →
                (h : Z = Bicone.diagram j) →
                  (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
              (fun (f : Bicone.right ⟶ Z) (h : Z = Bicone.diagram j) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f : Bicone.right ⟶ Y) →
                    (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f : Bicone.right ⟶ Bicone.diagram j)
                      (h : HEq f (β := BiconeHom J Bicone.right (Bicone.diagram j)) (BiconeHom.right j)) ↦
                    c₂.π.app j)
                  sorry f)
              sorry g)
          (fun {j k : J} (f : j ⟶ k) (h : Bicone.right = Bicone.diagram j) ↦
            Eq.ndrec (motive := fun {X : Bicone J} ↦
              (f_1 : X ⟶ Z) →
                (h : Z = Bicone.diagram k) →
                  (h : f_1 ≍ BiconeHom.diagram f) →
                    Quiver.Hom.{v₁, u₁} (V := C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) X c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
                      (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
              (fun (f_1 : Bicone.diagram j ⟶ Z) (h : Z = Bicone.diagram k) ↦
                Eq.ndrec (motive := fun {Y : Bicone J} ↦
                  (f_2 : Bicone.diagram j ⟶ Y) →
                    (h : f_2 ≍ BiconeHom.diagram f) →
                      Quiver.Hom.{v₁, u₁} (V := C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) (Bicone.diagram j) c₁.pt c₂.pt fun (j : J) ↦
                            F.obj j :
                          C)
                        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Y c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
                  (fun (f_2 : Bicone.diagram j ⟶ Bicone.diagram k) (h : f_2 ≍ BiconeHom.diagram f) ↦ F.map f) sorry f_1)
              sorry g)
          sorry sorry sorry) :
      Quiver.Hom.{v₁, u₁} (V := C)
        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Bicone.right c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C)
        (Bicone.casesOn (motive := fun (x : Bicone J) ↦ C) Z c₁.pt c₂.pt fun (j : J) ↦ F.obj j : C))
Tactic: rcases f with (_ | _ | _ | _ | _)
Cleared hypotheses: X, Y, f, g