@[reducible, inline]

abbrev SymplecticSumData {Ω₁ : ℕ → Type u_1} {VF₁ : Type u_2} {Ω₂ : ℕ → Type u_3} {VF₂ : Type u_4} {Ω_Q : ℕ → Type u_5} {VF_Q : Type u_6} [inst₁ : DifferentialFormSpace Ω₁ VF₁] [inst₂ : DifferentialFormSpace Ω₂ VF₂] [inst_Q : DifferentialFormSpace Ω_Q VF_Q] [dim_M₁ : SymplecticManifoldDim Ω₁ VF₁] [dim_M₂ : SymplecticManifoldDim Ω₂ VF₂] [dim_Q : SymplecticManifoldDim Ω_Q VF_Q] [IsCompactManifold Ω_Q VF_Q] : Type (max (max u_1 u_3) u_5)

Data describing a symplectic sum (Definition 3): the differential-form structure on the connected sum of two symplectic manifolds glued along a codimension-2 symplectic submanifold, here aliased to the underlying FiberSum.DFS structure.