<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<GOAL>∀ {X Y Z : CategoryTheory.Bicone J} (f : X ⟶ Y) (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f g = CategoryTheory.BiconeHom.casesOn (motive := fun a a_1 x => X = a → Y = a_1 → HEq f x → (X ⟶ Z)) f (fun h => Eq.ndrec (motive := fun {X} => (f : X ⟶ Y) → Y = CategoryTheory.Bicone.left → HEq f CategoryTheory.BiconeHom.left_id → (X ⟶ Z)) (fun f h => Eq.ndrec (motive := fun {Y} => (Y ⟶ Z) → (f : CategoryTheory.Bicone.left ⟶ Y) → HEq f CategoryTheory.BiconeHom.left_id → (CategoryTheory.Bicone.left ⟶ Z)) (fun g f h => g) ⋯ g f) ⋯ f) (fun h => Eq.ndrec (motive := fun {X} => (f : X ⟶ Y) → Y = CategoryTheory.Bicone.right → HEq f CategoryTheory.BiconeHom.right_id → (X ⟶ Z)) (fun f h => Eq.ndrec (motive := fun {Y} => (Y ⟶ Z) → (f : CategoryTheory.Bicone.right ⟶ Y) → HEq f CategoryTheory.BiconeHom.right_id → (CategoryTheory.Bicone.right ⟶ Z)) (fun g f h => g) ⋯ g f) ⋯ f) (fun j h => Eq.ndrec (motive := fun {X} => (f : X ⟶ Y) → Y = CategoryTheory.Bicone.diagram j → HEq f (CategoryTheory.BiconeHom.left j) → (X ⟶ Z)) (fun f h => Eq.ndrec (motive := fun {Y} => (Y ⟶ Z) → (f : CategoryTheory.Bicone.left ⟶ Y) → HEq f (CategoryTheory.BiconeHom.left 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 → HEq g t → (CategoryTheory.Bicone.left ⟶ Z)) g (fun h => CategoryTheory.Bicone.noConfusion h) (fun h => CategoryTheory.Bicone.noConfusion h) (fun j_1 h => CategoryTheory.Bicone.noConfusion h) (fun j_1 h => CategoryTheory.Bicone.noConfusion h) (fun {j_1 k} f h => CategoryTheory.Bicone.noConfusion h fun val_eq => Eq.ndrec (motive := fun {j_2} => (f : j_2 ⟶ k) → Z = CategoryTheory.Bicone.diagram k → HEq g (CategoryTheory.BiconeHom.diagram f) → (CategoryTheory.Bicone.left ⟶ Z)) (fun f h => Eq.ndrec (motive := fun {Z} => (g : CategoryTheory.Bicone.diagram j ⟶ Z) → HEq g (CategoryTheory.BiconeHom.diagram f) → (CategoryTheory.Bicone.left ⟶ Z)) (fun g h => CategoryTheory.BiconeHom.left k) ⋯ g) val_eq f) ⋯ ⋯ ⋯) ⋯ g f) ⋯ f) (fun j h => Eq.ndrec (motive := fun {X} => (f : X ⟶ Y) → Y = CategoryTheory.Bicone.diagram j → HEq f (CategoryTheory.BiconeHom.right j) → (X ⟶ Z)) (fun f h => Eq.ndrec (motive := fun {Y} => (Y ⟶ Z) → (f : CategoryTheory.Bicone.right ⟶ Y) → HEq f (CategoryTheory.BiconeHom.right 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 → HEq g t → (CategoryTheory.Bicone.right ⟶ Z)) g (fun h => CategoryTheory.Bicone.noConfusion h) (fun h => CategoryTheory.Bicone.noConfusion h) (fun j_1 h => CategoryTheory.Bicone.noConfusion h) (fun j_1 h => CategoryTheory.Bicone.noConfusion h) (fun {j_1 k} f h => CategoryTheory.Bicone.noConfusion h fun val_eq => Eq.ndrec (motive := fun {j_2} => (f : j_2 ⟶ k) → Z = CategoryTheory.Bicone.diagram k → HEq g (CategoryTheory.BiconeHom.diagram f) → (CategoryTheory.Bicone.right ⟶ Z)) (fun f h => Eq.ndrec (motive := fun {Z} => (g : CategoryTheory.Bicone.diagram j ⟶ Z) → HEq g (CategoryTheory.BiconeHom.diagram f) → (CategoryTheory.Bicone.right ⟶ Z)) (fun g h => CategoryTheory.BiconeHom.right k) ⋯ g) val_eq f) ⋯ ⋯ ⋯) ⋯ g f) ⋯ f) (fun {j k} f_1 h => Eq.ndrec (motive := fun {X} => (f : X ⟶ Y) → Y = CategoryTheory.Bicone.diagram k → HEq f (CategoryTheory.BiconeHom.diagram f_1) → (X ⟶ Z)) (fun f h => Eq.ndrec (motive := fun {Y} => (Y ⟶ Z) → (f : CategoryTheory.Bicone.diagram j ⟶ Y) → HEq f (CategoryTheory.BiconeHom.diagram f_1) → (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 → HEq g x → (CategoryTheory.Bicone.diagram j ⟶ Z)) g (fun h => CategoryTheory.Bicone.noConfusion h) (fun h => CategoryTheory.Bicone.noConfusion h) (fun j_1 h => CategoryTheory.Bicone.noConfusion h) (fun j_1 h => CategoryTheory.Bicone.noConfusion h) (fun {j_1 k_1} g_1 h => CategoryTheory.Bicone.noConfusion h fun val_eq => Eq.ndrec (motive := fun {j_2} => (g_2 : j_2 ⟶ k_1) → Z = CategoryTheory.Bicone.diagram k_1 → HEq g (CategoryTheory.BiconeHom.diagram g_2) → (CategoryTheory.Bicone.diagram j ⟶ Z)) (fun g_2 h => Eq.ndrec (motive := fun {Z} => (g : CategoryTheory.Bicone.diagram k ⟶ Z) → HEq g (CategoryTheory.BiconeHom.diagram g_2) → (CategoryTheory.Bicone.diagram j ⟶ Z)) (fun g h => CategoryTheory.BiconeHom.diagram (CategoryTheory.CategoryStruct.comp f_1 g_2)) ⋯ g) val_eq g_1) ⋯ ⋯ ⋯) ⋯ g f) ⋯ f) ⋯ ⋯ ⋯