{-# 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 (_≡_)
data Sign : Set where
- : Sign
+ : Sign
opposite : Sign → Sign
opposite - = +
opposite + = -
infixl 7 _*_
_*_ : Sign → Sign → Sign
+ * s₂ = s₂
- * s₂ = opposite s₂
*-rawMagma : RawMagma 0ℓ 0ℓ
*-rawMagma = record
{ _≈_ = _≡_
; _∙_ = _*_
}
*-1-rawMonoid : RawMonoid 0ℓ 0ℓ
*-1-rawMonoid = record
{ _≈_ = _≡_
; _∙_ = _*_
; ε = +
}
*-1-rawGroup : RawGroup 0ℓ 0ℓ
*-1-rawGroup = record
{ _≈_ = _≡_
; _∙_ = _*_
; _⁻¹ = opposite
; ε = +
}