### Examples of Structures

```{-# OPTIONS --without-K --exact-split --safe #-}

module Examples.Structures.Basic where

open import Agda.Primitive                  using ( Level ) renaming ( Set to Type ; lzero to ℓ₀ )
open import Data.Product                    using ( _,_ ; _×_  )
open import Relation.Unary                  using ( Pred ; _∈_ )

open import Overture                        using ( 𝟚 ; 𝟛 )
open import Base.Structures                 using ( signature ; structure )
open import Examples.Structures.Signatures  using ( S001 ; S∅ ; S0001 )

-- An example of a (purely) algebraic structure is a 3-element meet semilattice.

SL : structure  S001   -- (one binary operation symbol)
S∅     -- (no relation symbols)
{ρ = ℓ₀}

SL = record { carrier = 𝟛
; op = λ _ x → meet (x 𝟚.𝟎) (x 𝟚.𝟏)
; rel = λ ()
} where
meet : 𝟛 → 𝟛 → 𝟛
meet 𝟛.𝟎 𝟛.𝟎 = 𝟛.𝟎
meet 𝟛.𝟎 𝟛.𝟏 = 𝟛.𝟎
meet 𝟛.𝟎 𝟛.𝟐 = 𝟛.𝟎
meet 𝟛.𝟏 𝟛.𝟎 = 𝟛.𝟎
meet 𝟛.𝟏 𝟛.𝟏 = 𝟛.𝟏
meet 𝟛.𝟏 𝟛.𝟐 = 𝟛.𝟎
meet 𝟛.𝟐 𝟛.𝟎 = 𝟛.𝟎
meet 𝟛.𝟐 𝟛.𝟏 = 𝟛.𝟎
meet 𝟛.𝟐 𝟛.𝟐 = 𝟛.𝟐

```

An example of a (purely) relational structure is the 2 element structure with the ternary NAE-3-SAT relation, R = S³ - {(0,0,0), (1,1,1)} (where S = {0, 1}).

```data NAE3SAT : Pred (𝟚 × 𝟚 × 𝟚) ℓ₀ where
r1 : (𝟚.𝟎 , 𝟚.𝟎 , 𝟚.𝟏) ∈ NAE3SAT
r2 : (𝟚.𝟎 , 𝟚.𝟏 , 𝟚.𝟎) ∈ NAE3SAT
r3 : (𝟚.𝟎 , 𝟚.𝟏 , 𝟚.𝟏) ∈ NAE3SAT
r4 : (𝟚.𝟏 , 𝟚.𝟎 , 𝟚.𝟎) ∈ NAE3SAT
r5 : (𝟚.𝟏 , 𝟚.𝟎 , 𝟚.𝟏) ∈ NAE3SAT
r6 : (𝟚.𝟏 , 𝟚.𝟏 , 𝟚.𝟎) ∈ NAE3SAT

nae3sat : structure S∅    -- (no operation symbols)
S0001 -- (one ternary relation symbol)

nae3sat = record { carrier = 𝟚
; op = λ ()
; rel = λ _ x → ((x 𝟛.𝟎) , (x 𝟛.𝟏) , (x 𝟛.𝟐)) ∈ NAE3SAT
}

```