Lean4
/-- In a preadditive category, we can construct a binary biproduct for `X Y : C` from
any binary bicone `b` satisfying `total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.X`.
(That is, such a bicone is a limit cone and a colimit cocone.)
-/
def isBinaryBilimitOfTotal {X Y : C} (b : BinaryBicone X Y) (total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt) :
b.IsBilimit
where
isLimit :=
{ lift := fun s => (BinaryFan.fst s ≫ b.inl : s.pt ⟶ b.pt) + (BinaryFan.snd s ≫ b.inr : s.pt ⟶ b.pt)
uniq := fun s m h => by
have hₗ := h ⟨.left⟩
have hᵣ := h ⟨.right⟩
dsimp at hₗ hᵣ
simpa [← hₗ, ← hᵣ] using m ≫= total.symm
fac := fun s j => by rcases j with ⟨⟨⟩⟩ <;> simp }
isColimit :=
{ desc := fun s => (b.fst ≫ BinaryCofan.inl s : b.pt ⟶ s.pt) + (b.snd ≫ BinaryCofan.inr s : b.pt ⟶ s.pt)
uniq := fun s m h => by
have hₗ := h ⟨.left⟩
have hᵣ := h ⟨.right⟩
dsimp at hₗ hᵣ
simpa [← hₗ, ← hᵣ] using total.symm =≫ m
fac := fun s j => by rcases j with ⟨⟨⟩⟩ <;> simp }
