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