<VAR>J : Type v₁<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>F : CategoryTheory.Functor J C<VAR>c₁ c₂ : CategoryTheory.Limits.Cone F<GOAL>∀ {X Y : CategoryTheory.Bicone J} (f : X ⟶ Y), (CategoryTheory.biconeMk J c₁ c₂).map f = CategoryTheory.BiconeHom.casesOn (motive := fun a a_1 x => X = a → Y = a_1 → HEq f x → ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶ (fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y)) f (fun h => Eq.ndrec (motive := fun {X} => (f : X ⟶ Y) → Y = CategoryTheory.Bicone.left → HEq f CategoryTheory.BiconeHom.left_id → ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶ (fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y)) (fun f h => Eq.ndrec (motive := fun {Y} => (f : CategoryTheory.Bicone.left ⟶ Y) → HEq f CategoryTheory.BiconeHom.left_id → ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) CategoryTheory.Bicone.left ⟶ (fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y)) (fun f h => CategoryTheory.CategoryStruct.id ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) CategoryTheory.Bicone.left)) ⋯ f) ⋯ f) (fun h => Eq.ndrec (motive := fun {X} => (f : X ⟶ Y) → Y = CategoryTheory.Bicone.right → HEq f CategoryTheory.BiconeHom.right_id → ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶ (fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y)) (fun f h => Eq.ndrec (motive := fun {Y} => (f : CategoryTheory.Bicone.right ⟶ Y) → HEq f CategoryTheory.BiconeHom.right_id → ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) CategoryTheory.Bicone.right ⟶ (fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y)) (fun f h => CategoryTheory.CategoryStruct.id ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) CategoryTheory.Bicone.right)) ⋯ f) ⋯ f) (fun j h => Eq.ndrec (motive := fun {X} => (f : X ⟶ Y) → Y = CategoryTheory.Bicone.diagram j → HEq f (CategoryTheory.BiconeHom.left j) → ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶ (fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y)) (fun f h => Eq.ndrec (motive := fun {Y} => (f : CategoryTheory.Bicone.left ⟶ Y) → HEq f (CategoryTheory.BiconeHom.left j) → ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) CategoryTheory.Bicone.left ⟶ (fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y)) (fun f h => c₁.π.app j) ⋯ f) ⋯ f) (fun j h => Eq.ndrec (motive := fun {X} => (f : X ⟶ Y) → Y = CategoryTheory.Bicone.diagram j → HEq f (CategoryTheory.BiconeHom.right j) → ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶ (fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y)) (fun f h => Eq.ndrec (motive := fun {Y} => (f : CategoryTheory.Bicone.right ⟶ Y) → HEq f (CategoryTheory.BiconeHom.right j) → ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) CategoryTheory.Bicone.right ⟶ (fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y)) (fun f h => c₂.π.app j) ⋯ 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) → ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶ (fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y)) (fun f h => Eq.ndrec (motive := fun {Y} => (f : CategoryTheory.Bicone.diagram j ⟶ Y) → HEq f (CategoryTheory.BiconeHom.diagram f_1) → ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (CategoryTheory.Bicone.diagram j) ⟶ (fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y)) (fun f h => F.map f_1) ⋯ f) ⋯ f) ⋯ ⋯ ⋯