{-# OPTIONS --cubical --no-import-sorts --allow-unsolved-metas #-}
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Powerset
open import Cubical.Algebra.CommRing
open import Cubical.Relation.Nullary.Base
open import Cubical.Data.Sigma
open import Cubical.Data.Nat
open import Cubical.Data.Vec hiding (foldr; map)
open import Cubical.Data.List

open import AFF2024.Basics
open import AFF2024.Algebra.Basics

module AFF2024.AlgebraicSets.Basics {β„“ : Level} (R…@(R , Rstr) : CommRing β„“) where

open CommRingStr Rstr

𝔸 : β„• β†’ Type β„“
𝔸 n = Vec R n

module _ {n : β„•} where
  𝔸ⁿ-isSet : isSet (𝔸 n)
  𝔸ⁿ-isSet = VecPath.isOfHLevelVec 0 _ is-set

  -- vanishing set of a single polynomial
  V₁ : MultivariatePoly R… n β†’ β„™ (𝔸 n)
  V₁ f = Ξ» xs β†’ (evalT f xs ≑ 0r) , is-set _ _

  V : List (MultivariatePoly R… n) β†’ β„™ (𝔸 n)
  V fs = foldr _βˆͺ_ βˆ… (map V₁ fs)

  IsAlgebraic : β„™ (𝔸 n) β†’ Type (β„“-suc β„“)
  IsAlgebraic M = βˆƒ[ fs ∈ List (MultivariatePoly R… n) ] M ≑ V fs

  Idl : β„™ (𝔸 n) β†’ β„™ (MultivariatePoly R… n)
  Idl M = Ξ» f β†’ ((x : 𝔸 n) β†’ x ∈ M β†’ evalT f x ≑ 0r) , Ξ» r s i x p β†’ is-set _ _ (r x p) (s x p) i