{-# OPTIONS --cubical-compatible --safe #-}
module Data.Parity.Base where
open import Algebra.Bundles.Raw
using (RawMagma; RawMonoid; RawGroup; RawNearSemiring; RawSemiring)
open import Data.Sign.Base using (Sign; +; -)
open import Level using (0ℓ)
open import Relation.Binary.PropositionalEquality.Core using (_≡_)
data Parity : Set where
0ℙ : Parity
1ℙ : Parity
infix 8 _⁻¹
_⁻¹ : Parity → Parity
1ℙ ⁻¹ = 0ℙ
0ℙ ⁻¹ = 1ℙ
infixl 7 _+_
_+_ : Parity → Parity → Parity
0ℙ + p = p
1ℙ + p = p ⁻¹
infixl 7 _*_
_*_ : Parity → Parity → Parity
0ℙ * p = 0ℙ
1ℙ * p = p
+-rawMagma : RawMagma 0ℓ 0ℓ
+-rawMagma = record
{ _≈_ = _≡_
; _∙_ = _+_
}
+-0-rawMonoid : RawMonoid 0ℓ 0ℓ
+-0-rawMonoid = record
{ _≈_ = _≡_
; _∙_ = _+_
; ε = 0ℙ
}
+-0-rawGroup : RawGroup 0ℓ 0ℓ
+-0-rawGroup = record
{ _≈_ = _≡_
; _∙_ = _+_
; _⁻¹ = _⁻¹
; ε = 0ℙ
}
*-rawMagma : RawMagma 0ℓ 0ℓ
*-rawMagma = record
{ _≈_ = _≡_
; _∙_ = _*_
}
*-1-rawMonoid : RawMonoid 0ℓ 0ℓ
*-1-rawMonoid = record
{ _≈_ = _≡_
; _∙_ = _*_
; ε = 1ℙ
}
+-*-rawNearSemiring : RawNearSemiring 0ℓ 0ℓ
+-*-rawNearSemiring = record
{ Carrier = _
; _≈_ = _≡_
; _+_ = _+_
; _*_ = _*_
; 0# = 0ℙ
}
+-*-rawSemiring : RawSemiring 0ℓ 0ℓ
+-*-rawSemiring = record
{ Carrier = _
; _≈_ = _≡_
; _+_ = _+_
; _*_ = _*_
; 0# = 0ℙ
; 1# = 1ℙ
}
toSign : Parity → Sign
toSign 0ℙ = +
toSign 1ℙ = -
fromSign : Sign → Parity
fromSign + = 0ℙ
fromSign - = 1ℙ