{-# OPTIONS --cubical #-}
open import Cubical.Algebra.CommRing.Ideal
open import Cubical.Algebra.ZariskiLattice.Base
open import Categories.Category