ā†‘ Top


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

module Examples.Structures.Signatures where

open import Agda.Primitive         using () renaming ( lzero to ā„“ā‚€ )
open import Data.Unit.Base         using () renaming ( āŠ¤ to šŸ™ ; tt to šŸŽ )
open import Data.Empty             using () renaming ( āŠ„ to šŸ˜ )
open import Base.Overture.Preliminaries using ( šŸš ; šŸ› )
open import Base.Structures.Basic       using ( signature ; structure )

-- Some examples (of finite signatures)
-- The signature with...
-- ... no symbols  (e.g., sets)
Sāˆ… : signature ā„“ā‚€ ā„“ā‚€
Sāˆ… = record { symbol = šŸ˜ ; arity = Ī» () }

-- ... one nullary symbol (e.g., pointed sets)
S1 : signature ā„“ā‚€ ā„“ā‚€
S1 = record { symbol = šŸ™ ; arity = Ī» _ ā†’ šŸ˜ }

S01 : signature ā„“ā‚€ ā„“ā‚€ -- ...one unary
S01 = record { symbol = šŸ™ ; arity = Ī» _ ā†’ šŸ™ }

-- ...one binary symbol (e.g., magmas, semigroups, semilattices)
S001 : signature ā„“ā‚€ ā„“ā‚€
S001 = record { symbol = šŸ™ ; arity = Ī» _ ā†’ šŸš }

-- ...one ternary symbol (e.g., boolean NAE-3-SAT relational structure)
S0001 : signature ā„“ā‚€ ā„“ā‚€
S0001 = record { symbol = šŸ™ ; arity = Ī» _ ā†’ šŸ› }

-- ...0 nullary, 2 unary, and 1 binary
S021 : signature ā„“ā‚€ ā„“ā‚€
S021 = record { symbol = šŸ› ; arity = Ī»{ šŸ›.šŸŽ ā†’ šŸš ; šŸ›.šŸ ā†’ šŸ™ ; šŸ›.šŸ ā†’ šŸ™ } }

-- ...one nullary and one binary (e.g., monoids)
S101 : signature ā„“ā‚€ ā„“ā‚€
S101 = record { symbol = šŸš ; arity = Ī»{ šŸš.šŸŽ ā†’ šŸ˜ ; šŸš.šŸ ā†’ šŸš } }

-- ...one nullary, one unary, and one binary (e.g., groups)
S111 : signature ā„“ā‚€ ā„“ā‚€
S111 = record { symbol = šŸ› ; arity = Ī»{ šŸ›.šŸŽ ā†’ šŸ˜ ; šŸ›.šŸ ā†’ šŸ™ ; šŸ›.šŸ ā†’ šŸš } }