Relations in K0 of a full subcategory of ModuleCat from a linear equivalence

To get [Z] = [X] + [Y] in a split K0 indexed by bilimit BinaryBicones on P.FullSubcategory for P : ObjectProperty (ModuleCat R), build the bicone directly from e : Z.obj ≃ₗ[R] X.obj × Y.obj: fst := P.homMk (ofHom (LinearMap.fst R _ _ ∘ₗ e.toLinearMap)), inl := P.homMk (ofHom (e.symm.toLinearMap ∘ₗ LinearMap.inl R _ _)), etc. Each bicone axiom is ObjectProperty.hom_ext _ (ModuleCat.hom_ext (LinearMap.ext fun x => by simp)), and the total identity for isBinaryBilimitOfTotal reduces to e.symm ((e z).1,0) + e.symm (0,(e z).2) = z via ← map_add. Going the other way (bilimit bicone ⇒ linear equiv) works by mapping the bicone along P.ι, using IsLimit.conePointUniqueUpToIso with BinaryBiproduct.isLimit, then ModuleCat.biprodIsoProd and Iso.toLinearEquiv. Also: ObjectProperty.ιOfLE has no Additive instance; instance : (ιOfLE h).Additive where map_add := rfl works.