AFF2024.AlgebraicSets.Examples

{-# OPTIONS --cubical --no-import-sorts -WnoUnsupportedIndexedMatch --allow-unsolved-metas #-}
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Powerset
open import Cubical.Algebra.CommRing
open import Cubical.Data.List
open import Cubical.Data.Vec
open import Cubical.Data.Sigma

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

module AFF2024.AlgebraicSets.Examples {ℓ : Level} (R…@(R , Rstr) : CommRing ℓ) where

open AFF2024.AlgebraicSets.Basics R…

module TwistedCubic where
  open CommRingStr Rstr

  X : ℙ (𝔸 3)
  X (x ∷ y ∷ z ∷ []) = ((y - x · x ≡ 0r) × (z - x · x ≡ 0r)) , {!!}

  X' : ℙ (𝔸 3)
  X' (x ∷ y ∷ z ∷ []) = (∃[ t ∈ R ] ((x ≡ t) × (y ≡ t · t) × (z ≡ t · t · t))) , {!!}

  X→X' : (p : 𝔸 3) → p ∈ X → p ∈ X'
  X→X' = {!!}

  X'→X : (p : 𝔸 3) → p ∈ X' → p ∈ X
  X'→X = {!!}