------------------------------------------------------------------------ -- 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. infix 8 _⁻¹ _⁻¹ : Parity → Parity 1ℙ ⁻¹ = 0ℙ 0ℙ ⁻¹ = 1ℙ -- Addition. infixl 7 _+_ _+_ : Parity → Parity → Parity 0ℙ + p = p 1ℙ + p = p ⁻¹ -- Multiplication. infixl 7 _*_ _*_ : 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ℙ