Bicones

Given a category J, a walking Bicone J is a category whose objects are the objects of J and two extra vertices Bicone.left and Bicone.right. The morphisms are the morphisms of J and left ⟶ j, right ⟶ j for each j : J such that (· ⟶ j) and (· ⟶ k) commutes with each f : j ⟶ k.

Given a diagram F : J ⥤ C and two Cone Fs, we can join them into a diagram Bicone J ⥤ C via biconeMk.

This is used in CategoryTheory.Functor.Flat.

inductive CategoryTheory.Bicone (J : Type u₁) : Type u₁

Given a category J, construct a walking Bicone J by adjoining two elements.

• left: {J : Type u₁} → CategoryTheory.Bicone J
• right: {J : Type u₁} → CategoryTheory.Bicone J
• diagram: {J : Type u₁} → J → CategoryTheory.Bicone J

instance CategoryTheory.instDecidableEqBicone : {J : Type u_1} → [inst : DecidableEq J] → DecidableEq (CategoryTheory.Bicone J)

Equations

• CategoryTheory.instDecidableEqBicone = CategoryTheory.decEqBicone✝

instance CategoryTheory.instInhabitedBicone (J : Type u₁) : Inhabited (CategoryTheory.Bicone J)

Equations

• CategoryTheory.instInhabitedBicone J = { default := CategoryTheory.Bicone.left }

instance CategoryTheory.finBicone (J : Type u₁) [Fintype J] : Fintype (CategoryTheory.Bicone J)

Equations

• One or more equations did not get rendered due to their size.

inductive CategoryTheory.BiconeHom (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] : CategoryTheory.Bicone J → CategoryTheory.Bicone J → Type (max u₁ v₁)

The homs for a walking Bicone J.

• left_id: {J : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} J] → CategoryTheory.BiconeHom J CategoryTheory.Bicone.left CategoryTheory.Bicone.left
• right_id: {J : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} J] → CategoryTheory.BiconeHom J CategoryTheory.Bicone.right CategoryTheory.Bicone.right
• left: {J : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} J] → (j : J) → CategoryTheory.BiconeHom J CategoryTheory.Bicone.left (CategoryTheory.Bicone.diagram j)
• right: {J : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} J] → (j : J) → CategoryTheory.BiconeHom J CategoryTheory.Bicone.right (CategoryTheory.Bicone.diagram j)
• diagram: {J : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} J] → {j k : J} → (j ⟶ k) → CategoryTheory.BiconeHom J (CategoryTheory.Bicone.diagram j) (CategoryTheory.Bicone.diagram k)

instance CategoryTheory.instInhabitedBiconeHomLeft (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] : Inhabited (CategoryTheory.BiconeHom J CategoryTheory.Bicone.left CategoryTheory.Bicone.left)

Equations

• CategoryTheory.instInhabitedBiconeHomLeft J = { default := CategoryTheory.BiconeHom.left_id }

instance CategoryTheory.BiconeHom.decidableEq (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {j : CategoryTheory.Bicone J} {k : CategoryTheory.Bicone J} : DecidableEq (CategoryTheory.BiconeHom J j k)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

theorem CategoryTheory.biconeCategoryStruct_Hom (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] : ∀ (a a_1 : CategoryTheory.Bicone J), (a ⟶ a_1) = CategoryTheory.BiconeHom J a a_1

@[simp]

theorem CategoryTheory.biconeCategoryStruct_id (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] (j : CategoryTheory.Bicone J) : CategoryTheory.CategoryStruct.id j = CategoryTheory.Bicone.casesOn j CategoryTheory.BiconeHom.left_id CategoryTheory.BiconeHom.right_id fun (k : J) => CategoryTheory.BiconeHom.diagram (CategoryTheory.CategoryStruct.id k)

instance CategoryTheory.biconeCategoryStruct (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] : CategoryTheory.CategoryStruct.{max u₁ v₁, u₁} (CategoryTheory.Bicone J)

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.biconeCategory (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] : CategoryTheory.Category.{max u₁ v₁, u₁} (CategoryTheory.Bicone J)

Equations

• CategoryTheory.biconeCategory J = CategoryTheory.Category.mk

@[simp]

theorem CategoryTheory.biconeMk_map (J : Type v₁) [CategoryTheory.SmallCategory J] {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor J C} (c₁ : CategoryTheory.Limits.Cone F) (c₂ : CategoryTheory.Limits.Cone F) : ∀ {X Y : CategoryTheory.Bicone J} (f : X ⟶ Y), (CategoryTheory.biconeMk J c₁ c₂).toPrefunctor.map f = CategoryTheory.BiconeHom.casesOn (motive := fun (a a_1 : CategoryTheory.Bicone J) (x : CategoryTheory.BiconeHom J a a_1) => X = a → Y = a_1 → HEq f x → ((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j) X ⟶ (fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j) Y)) f (fun (h : X = CategoryTheory.Bicone.left) => Eq.ndrec (motive := fun {X : CategoryTheory.Bicone J} => (f : X ⟶ Y) → Y = CategoryTheory.Bicone.left → HEq f CategoryTheory.BiconeHom.left_id → ((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j) X ⟶ (fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j) Y)) (fun (f : CategoryTheory.Bicone.left ⟶ Y) (h : Y = CategoryTheory.Bicone.left) => Eq.ndrec (motive := fun {Y : CategoryTheory.Bicone J} => (f : CategoryTheory.Bicone.left ⟶ Y) → HEq f CategoryTheory.BiconeHom.left_id → ((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j) CategoryTheory.Bicone.left ⟶ (fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j) Y)) (fun (f : CategoryTheory.Bicone.left ⟶ CategoryTheory.Bicone.left) (h : HEq f CategoryTheory.BiconeHom.left_id) => CategoryTheory.CategoryStruct.id ((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j) CategoryTheory.Bicone.left)) (_ : CategoryTheory.Bicone.left = Y) f) (_ : CategoryTheory.Bicone.left = X) f) (fun (h : X = CategoryTheory.Bicone.right) => Eq.ndrec (motive := fun {X : CategoryTheory.Bicone J} => (f : X ⟶ Y) → Y = CategoryTheory.Bicone.right → HEq f CategoryTheory.BiconeHom.right_id → ((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j) X ⟶ (fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j) Y)) (fun (f : CategoryTheory.Bicone.right ⟶ Y) (h : Y = CategoryTheory.Bicone.right) => Eq.ndrec (motive := fun {Y : CategoryTheory.Bicone J} => (f : CategoryTheory.Bicone.right ⟶ Y) → HEq f CategoryTheory.BiconeHom.right_id → ((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j) CategoryTheory.Bicone.right ⟶ (fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j) Y)) (fun (f : CategoryTheory.Bicone.right ⟶ CategoryTheory.Bicone.right) (h : HEq f CategoryTheory.BiconeHom.right_id) => CategoryTheory.CategoryStruct.id ((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j) CategoryTheory.Bicone.right)) (_ : CategoryTheory.Bicone.right = Y) f) (_ : CategoryTheory.Bicone.right = X) f) (fun (j : J) (h : X = CategoryTheory.Bicone.left) => Eq.ndrec (motive := fun {X : CategoryTheory.Bicone J} => (f : X ⟶ Y) → Y = CategoryTheory.Bicone.diagram j → HEq f (CategoryTheory.BiconeHom.left j) → ((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j) X ⟶ (fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j) Y)) (fun (f : CategoryTheory.Bicone.left ⟶ Y) (h : Y = CategoryTheory.Bicone.diagram j) => Eq.ndrec (motive := fun {Y : CategoryTheory.Bicone J} => (f : CategoryTheory.Bicone.left ⟶ Y) → HEq f (CategoryTheory.BiconeHom.left j) → ((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j) CategoryTheory.Bicone.left ⟶ (fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j) Y)) (fun (f : CategoryTheory.Bicone.left ⟶ CategoryTheory.Bicone.diagram j) (h : HEq f (CategoryTheory.BiconeHom.left j)) => c₁.π.app j) (_ : CategoryTheory.Bicone.diagram j = Y) f) (_ : CategoryTheory.Bicone.left = X) f) (fun (j : J) (h : X = CategoryTheory.Bicone.right) => Eq.ndrec (motive := fun {X : CategoryTheory.Bicone J} => (f : X ⟶ Y) → Y = CategoryTheory.Bicone.diagram j → HEq f (CategoryTheory.BiconeHom.right j) → ((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j) X ⟶ (fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j) Y)) (fun (f : CategoryTheory.Bicone.right ⟶ Y) (h : Y = CategoryTheory.Bicone.diagram j) => Eq.ndrec (motive := fun {Y : CategoryTheory.Bicone J} => (f : CategoryTheory.Bicone.right ⟶ Y) → HEq f (CategoryTheory.BiconeHom.right j) → ((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j) CategoryTheory.Bicone.right ⟶ (fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j) Y)) (fun (f : CategoryTheory.Bicone.right ⟶ CategoryTheory.Bicone.diagram j) (h : HEq f (CategoryTheory.BiconeHom.right j)) => c₂.π.app j) (_ : CategoryTheory.Bicone.diagram j = Y) f) (_ : CategoryTheory.Bicone.right = X) f) (fun {j k : J} (f_1 : j ⟶ k) (h : X = CategoryTheory.Bicone.diagram j) => Eq.ndrec (motive := fun {X : CategoryTheory.Bicone J} => (f : X ⟶ Y) → Y = CategoryTheory.Bicone.diagram k → HEq f (CategoryTheory.BiconeHom.diagram f_1) → ((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j) X ⟶ (fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j) Y)) (fun (f : CategoryTheory.Bicone.diagram j ⟶ Y) (h : Y = CategoryTheory.Bicone.diagram k) => Eq.ndrec (motive := fun {Y : CategoryTheory.Bicone J} => (f : CategoryTheory.Bicone.diagram j ⟶ Y) → HEq f (CategoryTheory.BiconeHom.diagram f_1) → ((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j) (CategoryTheory.Bicone.diagram j) ⟶ (fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j) Y)) (fun (f : CategoryTheory.Bicone.diagram j ⟶ CategoryTheory.Bicone.diagram k) (h : HEq f (CategoryTheory.BiconeHom.diagram f_1)) => F.toPrefunctor.map f_1) (_ : CategoryTheory.Bicone.diagram k = Y) f) (_ : CategoryTheory.Bicone.diagram j = X) f) (_ : X = X) (_ : Y = Y) (_ : HEq f f)

@[simp]

theorem CategoryTheory.biconeMk_obj (J : Type v₁) [CategoryTheory.SmallCategory J] {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor J C} (c₁ : CategoryTheory.Limits.Cone F) (c₂ : CategoryTheory.Limits.Cone F) (X : CategoryTheory.Bicone J) : (CategoryTheory.biconeMk J c₁ c₂).toPrefunctor.obj X = CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.toPrefunctor.obj j

def CategoryTheory.biconeMk (J : Type v₁) [CategoryTheory.SmallCategory J] {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor J C} (c₁ : CategoryTheory.Limits.Cone F) (c₂ : CategoryTheory.Limits.Cone F) : CategoryTheory.Functor (CategoryTheory.Bicone J) C

Given a diagram F : J ⥤ C and two Cone Fs, we can join them into a diagram Bicone J ⥤ C.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.finBiconeHom (J : Type v₁) [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (j : CategoryTheory.Bicone J) (k : CategoryTheory.Bicone J) : Fintype (j ⟶ k)

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.biconeSmallCategory (J : Type v₁) [CategoryTheory.SmallCategory J] : CategoryTheory.SmallCategory (CategoryTheory.Bicone J)

Equations

• CategoryTheory.biconeSmallCategory J = CategoryTheory.biconeCategory J

instance CategoryTheory.biconeFinCategory (J : Type v₁) [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] : CategoryTheory.FinCategory (CategoryTheory.Bicone J)

Equations

• CategoryTheory.biconeFinCategory J = CategoryTheory.FinCategory.mk