{-# 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' = {!!}