Constructors for projective-injective copresentations

noncomputable def CategoryTheory.Preadditive.LeftFreyd.ProjectiveInjectiveCopresentation.ofTwoStepMinimalInjectivePresentation {C : Type u} [Category.{v, u} C] [Abelian C] {P : C} (I : MagnitudeConjecture.TwoStepMinimalInjectivePresentation P) (hI₀Projective : Projective I.augmentation.J) (hI₁Projective : Projective I.cosyzygyPresentation.J) : ProjectiveInjectiveCopresentation P

Regard a two-step minimal injective presentation whose two injective terms are also projective as a projective-injective copresentation.