{-# OPTIONS --cubical --no-import-sorts --allow-unsolved-metas #-} module AFF2024.AlgebraicSets.Sizes where open import Cubical.Foundations.Prelude open import Cubical.Algebra.CommRing open import Cubical.Data.Nat open import AFF2024.Basics open import AFF2024.Algebra.Basics open import Cubical.Data.List import AFF2024.AlgebraicSets.Basics module _ {ℓ : Level} (R…@(R , Rstr) : CommRing ℓ) (is-field : IsField R…) where open AFF2024.AlgebraicSets.Basics R… part-b : {n : ℕ} (f : MultivariatePoly R… n) → IsExploding (V₁ {n = n} f) part-b = {!!} part-b' : {n : ℕ} (fs : List (MultivariatePoly R… n)) → IsExploding (V {n = n} fs) part-b' = {!!}