---
layout: default
title : "Examples.Structures.Basic module (Agda Universal Algebra Library)"
date : "2021-07-29"
author: "agda-algebras development team"
---

### Examples of Structures

This is the [Examples.Structures.Basic][] module of the [Agda Universal Algebra Library][].

Two tiny worked examples of the general `structure` type of the frozen
`Legacy.Base` tree, which packages operation symbols and relation symbols in one
signature pair: a purely algebraic structure and a purely relational one.  The
signatures come from [Examples.Structures.Signatures][].

<!--
```agda
{-# OPTIONS --without-K --exact-split --safe #-}

module Examples.Structures.Basic where

open import Level                           using ( 0ℓ )
open import Data.Product                    using ( _,_ ; _×_  )
open import Relation.Unary                  using ( Pred ; _∈_ )

open import Overture                        using ( 𝟚 ; 𝟛 )
open import Legacy.Base.Structures          using ( structure )
open import Examples.Structures.Signatures  using ( S001 ; S∅ ; S0001 )
```
-->

`SL` is a three-element meet semilattice presented as a `structure` with one binary
operation symbol (`S001`) and no relation symbols (`S∅`).  The meet of two distinct
elements is `𝟎`, so the induced order has bottom `𝟎` below the incomparable pair
`𝟏`, `𝟐`.

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

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

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}).


```agda
data NAE3SAT : Pred (𝟚 × 𝟚 × 𝟚) 0ℓ 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
                 }
```