------------------------------------------------------------------------
-- The Agda standard library
--
-- Signs
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Data.Sign.Base where
 
open import Algebra.Bundles.Raw using (RawMagma; RawMonoid; RawGroup)
open import Level using (0ℓ)
open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
------------------------------------------------------------------------
-- Definition
 
data Sign : Set where
  - : Sign
  + : Sign
 
------------------------------------------------------------------------
-- Operations
 
-- The opposite sign.
 
opposite : Sign → Sign
opposite - = +
opposite + = -
 
-- "Multiplication".
 
infixl  _*_
 
_*_ : Sign → Sign → Sign
+ * s₂ = s₂
- * s₂ = opposite s₂
 
------------------------------------------------------------------------
-- Raw Bundles
 
*-rawMagma : RawMagma 0ℓ 0ℓ
*-rawMagma = record
  { _≈_ = _≡_
  ; _∙_ = _*_
  }
 
*-1-rawMonoid : RawMonoid 0ℓ 0ℓ
*-1-rawMonoid = record
  { _≈_ = _≡_
  ; _∙_ = _*_
  ; ε = +
  }
 
*-1-rawGroup : RawGroup 0ℓ 0ℓ
*-1-rawGroup = record
  { _≈_ = _≡_
  ; _∙_ = _*_
  ; _⁻¹ = opposite
  ; ε = +
  }