------------------------------------------------------------------------
-- The Agda standard library
--
-- Parity
------------------------------------------------------------------------

{-# 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 (_≡_)

------------------------------------------------------------------------
-- Definition

data Parity : Set where
  0ℙ : Parity
  1ℙ : Parity

------------------------------------------------------------------------
-- Operations

-- The opposite parity.

_⁻¹ : Parity → Parity
1ℙ ⁻¹ = 0ℙ
0ℙ ⁻¹ = 1ℙ

-- Addition.

infixl  _+_

_+_ : Parity → Parity → Parity
0ℙ + p = p
1ℙ + p = p ⁻¹

-- Multiplication.

infixl  _*_

_*_ : Parity → Parity → Parity
0ℙ * p = 0ℙ
1ℙ * p = p

------------------------------------------------------------------------
-- Raw Bundles

+-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ℙ
  }


------------------------------------------------------------------------
-- Homomorphisms between Parity and Sign

toSign : Parity → Sign
toSign 0ℙ = +
toSign 1ℙ = -

fromSign : Sign → Parity
fromSign + = 0ℙ
fromSign - = 1ℙ