[Agda] Definizione di semianello

[caulacau]

Un semigruppo e un monoide si definiscono in Agda come segue:

record Semigroup (a : Set) : Set where
  field
    _o_ : a → a → a
    assoc : ∀  a b c → (a o b) o c ≡ a o (b o c)

record Monoid (a : Set) : Set where
  field
    semigroup : Semigroup a
  open Semigroup semigroup
  field
    z : a
    lId : ∀ x → z o x ≡ x
    rId : ∀ x → x o z ≡ x

Come si definisce, ora, un semianello? Questa definizione typechecka, ma non so (proprio a livello di sintassi) come specificare che l'operazione di monoide è \(\oplus\) e quella di semigruppo \(\circ\):

record Semiring (a : Set) : Set where
  field
    monoid : Monoid a
    semigroup : Semigroup a
  field
    _⊕_ : a → a → a
    _o_ : a → a → a

[caulacau]

Ci sono riuscito, e il risultato è proprio bello.

module MyAlgebra where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_)

-- properties

Commutative :
  ∀ {a} →
  (a → a → a) → Set
Commutative f =
  ∀ x → ∀ y → f x y ≡ f y x

Associative :
  ∀ {a} →
  (a → a → a) → Set
Associative f =
  ∀ x y z → f (f x y) z ≡ f x (f y z)

_distributesOver_ :
  ∀ {a} →
  (a → a → a) →
  (a → a → a) → Set
f distributesOver g =
  ∀ a b c → f a (g b c) ≡ g (f a b) (f a c)

-- structures

record IsSemigroup
  (a : Set)
  (_o_ : a → a → a) : Set where
  field
    assoc : Associative (_o_)

record Semigroup : Set₁ where
  field
    a : Set
    _o_ : a → a → a
    isSemigroup : IsSemigroup a (_o_)

record HasIdentity
  (a : Set)
  (_o_ : a → a → a)
  (z : a) : Set where
  field
    lId : ∀ a → z o a ≡ a
    rId : ∀ a → a o z ≡ a

record HasInverses
  (a : Set)
  (_o_ : a → a → a)
  (z : a)
  (inv : a → a) : Set where
  field
    rInv : ∀ x → x o (inv x) ≡ z
    lInv : ∀ x → (inv x) o x ≡ z

record IsMonoid
  (a : Set)
  (_o_ : a → a → a)
  (z : a) : Set where
  field
    isSemigroup : IsSemigroup a (_o_)
    hasIdentity : HasIdentity a (_o_) z

record IsGroup
  (a : Set)
  (_o_ : a → a → a)
  (z : a)
  (i : a → a) : Set where
  field
    isMonoid : IsMonoid a (_o_) z
    hasInverses : HasInverses a (_o_) z i

record IsAbelianMonoid
  (a : Set)
  (_o_ : a → a → a)
  (z : a) : Set where
  field
    isMonoid : IsMonoid a (_o_) z
    isAbelian : Commutative (_o_)

record IsAbelianGroup
  (a : Set)
  (_o_ : a → a → a)
  (z : a)
  (i : a → a) : Set where
  field
    isGroup : IsGroup a (_o_) z i
    isCommutativeCirc : Commutative (_o_)

record IsRing
  (a : Set)
  (_o_ : a → a → a)
  (_⊕_ : a → a → a)
  (z : a)
  (i : a → a) : Set where
  field
    isAbelianGroup : IsAbelianGroup a (_o_) z i
    isMonoid : IsMonoid a (_o_) z
    isRing : (_o_) distributesOver (_⊕_)

record IsUnitaryRing
  (a : Set)
  (_o_ : a → a → a)
  (_⊕_ : a → a → a)
  (z : a)
  (i : a → a)
  (u : a) : Set where
  field
    isRing : IsRing a (_o_) (_⊕_) z i
    isUnitary : IsMonoid a (_o_) u

record IsCommutativeRing
  (a : Set)
  (_o_ : a → a → a)
  (_⊕_ : a → a → a)
  (z : a)
  (i : a → a)
  (u : a) : Set where
  field
    isUnitaryRing : IsUnitaryRing a (_o_) (_⊕_) z i u
    isCommutativeCirc : IsAbelianMonoid a (_o_) z

(ma c'è un modo di avere della syntax highlighting nell'ambiente code?)

[caulacau]

Partendo da qui, sapete dimostrare che, dato un insieme $X$, l'algebra di Boole \((2^X, \land, \lor)\) è un anello booleano?