agda-spa/Lattice/Builder.agda

module Lattice.Builder where

open import Lattice
open import Equivalence
open import Utils using (fins; fins-complete)
open import Data.Nat as Nat using (ℕ)
open import Data.Fin as Fin using (Fin; suc; zero; _≟_)
open import Data.Maybe as Maybe using (Maybe; just; nothing; _>>=_; maybe)
open import Data.Maybe.Properties using (just-injective)
open import Data.Unit using (⊤; tt)
open import Data.List.NonEmpty using (List⁺; tail; toList) renaming (_∷_ to _∷⁺_)
open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_; mapWith∈ to mapWith∈ˡ)
open import Data.List.Membership.Propositional.Properties using () renaming (∈-++⁺ʳ to ∈ˡ-++⁺ʳ)
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Data.List.Relation.Unary.All using (All; []; _∷_; map)
open import Data.List using (List; _∷_; []; cartesianProduct; cartesianProductWith; foldr) renaming (_++_ to _++ˡ_)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (Σ; _,_; _×_; proj₁; proj₂)
open import Data.Empty using (⊥; ⊥-elim)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_)