Algebra.Bundles.Raw

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335
------------------------------------------------------------------------
-- The Agda standard library
--
-- Definitions of 'raw' bundles
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Algebra.Bundles.Raw where
 
open import Algebra.Core
open import Relation.Binary.Core using (Rel)
open import Level using (suc; _⊔_)
open import Relation.Nullary.Negation.Core using (¬_)
 
------------------------------------------------------------------------
-- Raw bundles with 1 unary operation & 1 element
------------------------------------------------------------------------
 
-- A raw SuccessorSet is a SuccessorSet without any laws.
 
record RawSuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    suc#    : Op₁ Carrier
    zero#   : Carrier
 
------------------------------------------------------------------------
-- Raw bundles with 1 binary operation
------------------------------------------------------------------------
 
record RawMagma c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
 
  infix 4 _≉_
  _≉_ : Rel Carrier _
  x ≉ y = ¬ (x ≈ y)
 
------------------------------------------------------------------------
-- Raw bundles with 1 binary operation & 1 element
------------------------------------------------------------------------
 
-- A raw monoid is a monoid without any laws.
 
record RawMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
    ε       : Carrier
 
  rawMagma : RawMagma c ℓ
  rawMagma = record
    { _≈_ = _≈_
    ; _∙_ = _∙_
    }
 
  open RawMagma rawMagma public
    using (_≉_)
 
------------------------------------------------------------------------
-- Raw bundles with 1 binary operation, 1 unary operation & 1 element
------------------------------------------------------------------------
 
record RawGroup c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  8 _⁻¹
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
    ε       : Carrier
    _⁻¹     : Op₁ Carrier
 
  rawMonoid : RawMonoid c ℓ
  rawMonoid = record
    { _≈_ = _≈_
    ; _∙_ = _∙_
    ; ε   = ε
    }
 
  open RawMonoid rawMonoid public
    using (_≉_; rawMagma)
 
------------------------------------------------------------------------
-- Raw bundles with 2 binary operations & 1 element
------------------------------------------------------------------------
 
record RawNearSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _+_     : Op₂ Carrier
    _*_     : Op₂ Carrier
    0#      : Carrier
 
  +-rawMonoid : RawMonoid c ℓ
  +-rawMonoid = record
    { _≈_ = _≈_
    ; _∙_ = _+_
    ;  ε  = 0#
    }
 
  open RawMonoid +-rawMonoid public
    using (_≉_) renaming (rawMagma to +-rawMagma)
 
  *-rawMagma : RawMagma c ℓ
  *-rawMagma = record
    { _≈_ = _≈_
    ; _∙_ = _*_
    }
 
------------------------------------------------------------------------
-- Raw bundles with 2 binary operations & 2 elements
------------------------------------------------------------------------
 
record RawSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _+_     : Op₂ Carrier
    _*_     : Op₂ Carrier
    0#      : Carrier
    1#      : Carrier
 
  rawNearSemiring : RawNearSemiring c ℓ
  rawNearSemiring = record
    { _≈_ = _≈_
    ; _+_ = _+_
    ; _*_ = _*_
    ; 0#  = 0#
    }
 
  open RawNearSemiring rawNearSemiring public
    using (_≉_; +-rawMonoid; +-rawMagma; *-rawMagma)
 
  *-rawMonoid : RawMonoid c ℓ
  *-rawMonoid = record
    { _≈_ = _≈_
    ; _∙_ = _*_
    ; ε   = 1#
    }
 
------------------------------------------------------------------------
-- Raw bundles with 2 binary operations, 1 unary operation & 1 element
------------------------------------------------------------------------
 
record RawRingWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _+_     : Op₂ Carrier
    _*_     : Op₂ Carrier
    -_      : Op₁ Carrier
    0#      : Carrier
 
  +-rawGroup : RawGroup c ℓ
  +-rawGroup = record
    { _≈_ = _≈_
    ; _∙_ = _+_
    ; ε   = 0#
    ; _⁻¹ = -_
    }
 
  open RawGroup +-rawGroup public
    using (_≉_) renaming (rawMagma to +-rawMagma; rawMonoid to +-rawMonoid)
 
  *-rawMagma : RawMagma c ℓ
  *-rawMagma = record
    { _≈_ = _≈_
    ; _∙_ = _*_
    }
 
------------------------------------------------------------------------
-- Raw bundles with 2 binary operations, 1 unary operation & 2 elements
------------------------------------------------------------------------
 
-- A raw ring is a ring without any laws.
 
record RawRing c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _+_     : Op₂ Carrier
    _*_     : Op₂ Carrier
    -_      : Op₁ Carrier
    0#      : Carrier
    1#      : Carrier
 
  rawSemiring : RawSemiring c ℓ
  rawSemiring = record
    { _≈_ = _≈_
    ; _+_ = _+_
    ; _*_ = _*_
    ; 0#  = 0#
    ; 1#  = 1#
    }
 
  open RawSemiring rawSemiring public
    using
    ( _≉_
    ; +-rawMagma; +-rawMonoid
    ; *-rawMagma; *-rawMonoid
    )
 
  rawRingWithoutOne : RawRingWithoutOne c ℓ
  rawRingWithoutOne = record
    { _≈_ = _≈_
    ; _+_ = _+_
    ; _*_ = _*_
    ; -_ = -_
    ; 0# = 0#
    }
 
  open RawRingWithoutOne rawRingWithoutOne public
    using (+-rawGroup)
 
------------------------------------------------------------------------
-- Raw bundles with 3 binary operations
------------------------------------------------------------------------
 
record RawQuasigroup c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infixl 7 _\\_
  infixl 7 _//_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
    _\\_    : Op₂ Carrier
    _//_    : Op₂ Carrier
 
  ∙-rawMagma : RawMagma c ℓ
  ∙-rawMagma = record
    { _≈_ = _≈_
    ; _∙_ = _∙_
    }
 
  \\-rawMagma : RawMagma c ℓ
  \\-rawMagma = record
    { _≈_ = _≈_
    ; _∙_ = _\\_
    }
 
  //-rawMagma : RawMagma c ℓ
  //-rawMagma = record
    { _≈_ = _≈_
    ; _∙_ = _//_
    }
 
  open RawMagma \\-rawMagma public
    using (_≉_)
 
------------------------------------------------------------------------
-- Raw bundles with 3 binary operations & 1 element
------------------------------------------------------------------------
 
record RawLoop  c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infixl 7 _\\_
  infixl 7 _//_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
    _\\_    : Op₂ Carrier
    _//_    : Op₂ Carrier
    ε       : Carrier
 
  rawQuasigroup : RawQuasigroup c ℓ
  rawQuasigroup = record
    { _≈_ = _≈_
    ; _∙_ = _∙_
    ; _\\_ = _\\_
    ; _//_ = _//_
    }
 
  open RawQuasigroup rawQuasigroup public
    using (_≉_ ; ∙-rawMagma; \\-rawMagma; //-rawMagma)
 
record RawKleeneAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  8 _⋆
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _+_     : Op₂ Carrier
    _*_     : Op₂ Carrier
    _⋆      : Op₁ Carrier
    0#      : Carrier
    1#      : Carrier
 
  rawSemiring : RawSemiring c ℓ
  rawSemiring = record
    { _≈_ = _≈_
    ; _+_ = _+_
    ; _*_ = _*_
    ; 0#  = 0#
    ; 1#  = 1#
    }
 
  open RawSemiring rawSemiring public
    using
    ( _≉_
    ; +-rawMagma; +-rawMonoid
    ; *-rawMagma; *-rawMonoid
    )