    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Some properties about signs
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Data.Sign.Properties where

    open import Algebra.Bundles
      using (Magma; Semigroup; CommutativeSemigroup; Monoid; CommutativeMonoid
            ; Group; AbelianGroup)
    open import Data.Sign.Base using (Sign; opposite; _*_; +; -)
    open import Data.Product.Base using (_,_)
    open import Function.Base using (_$_; id)
    open import Function.Definitions using (Injective)
    open import Level using (0ℓ)
    open import Relation.Binary.Definitions using (Decidable; DecidableEquality)
    open import Relation.Binary.Structures using (IsDecEquivalence)
    open import Relation.Binary.Bundles using (Setoid; DecSetoid)
    open import Relation.Binary.PropositionalEquality.Core
      using (_≡_; refl; _≢_; sym; cong₂)
    open import Relation.Binary.PropositionalEquality.Properties
      using (setoid; decSetoid; isDecEquivalence; isEquivalence)
    open import Relation.Nullary.Decidable using (yes; no)
    open import Relation.Nullary.Negation.Core using (contradiction)

    open import Algebra.Structures {A = Sign} _≡_
    open import Algebra.Definitions {A = Sign} _≡_
    open import Algebra.Consequences.Propositional
      using (selfInverse⇒involutive; selfInverse⇒injective)

    ------------------------------------------------------------------------
    -- Equality

    infix 4 _≟_

    _≟_ : DecidableEquality Sign
    - ≟ - = yes refl
    - ≟ + = no λ()
    + ≟ - = no λ()
    + ≟ + = yes refl

    ≡-setoid : Setoid 0ℓ 0ℓ
    ≡-setoid = setoid Sign

    ≡-decSetoid : DecSetoid 0ℓ 0ℓ
    ≡-decSetoid = decSetoid _≟_

    ≡-isDecEquivalence : IsDecEquivalence _≡_
    ≡-isDecEquivalence = isDecEquivalence _≟_

    ------------------------------------------------------------------------
    -- opposite

    -- Algebraic properties of opposite

    opposite-selfInverse : SelfInverse opposite
    opposite-selfInverse { - } { + } refl = refl
    opposite-selfInverse { + } { - } refl = refl

    opposite-involutive : Involutive opposite
    opposite-involutive = selfInverse⇒involutive opposite-selfInverse

    opposite-injective : Injective _≡_ _≡_ opposite
    opposite-injective = selfInverse⇒injective opposite-selfInverse

    ------------------------------------------------------------------------
    -- other properties of opposite

    s≢opposite[s] : ∀ s → s ≢ opposite s
    s≢opposite[s] - ()
    s≢opposite[s] + ()

    ------------------------------------------------------------------------
    -- _*_

    -- Algebraic properties of _*_

    s*s≡+ : ∀ s → s * s ≡ +
    s*s≡+ + = refl
    s*s≡+ - = refl

    *-identityˡ : LeftIdentity + _*_
    *-identityˡ _ = refl

    *-identityʳ : RightIdentity + _*_
    *-identityʳ - = refl
    *-identityʳ + = refl

    *-identity : Identity + _*_
    *-identity = *-identityˡ  , *-identityʳ

    *-comm : Commutative _*_
    *-comm + + = refl
    *-comm + - = refl
    *-comm - + = refl
    *-comm - - = refl

    *-assoc : Associative _*_
    *-assoc + + _ = refl
    *-assoc + - _ = refl
    *-assoc - + _ = refl
    *-assoc - - + = refl
    *-assoc - - - = refl

    *-cancelʳ-≡ : RightCancellative _*_
    *-cancelʳ-≡ _ - - _  = refl
    *-cancelʳ-≡ _ - + eq = contradiction (sym eq) (s≢opposite[s] _)
    *-cancelʳ-≡ _ + - eq = contradiction eq (s≢opposite[s] _)
    *-cancelʳ-≡ _ + + _  = refl

    *-cancelˡ-≡ : LeftCancellative _*_
    *-cancelˡ-≡ - _ _ eq = opposite-injective eq
    *-cancelˡ-≡ + _ _ eq = eq

    *-cancel-≡ : Cancellative _*_
    *-cancel-≡ = *-cancelˡ-≡ , *-cancelʳ-≡

    *-inverse : Inverse + id _*_
    *-inverse = s*s≡+ , s*s≡+

    *-isMagma : IsMagma _*_
    *-isMagma = record
      { isEquivalence = isEquivalence
      ; ∙-cong        = cong₂ _*_
      }

    *-magma : Magma 0ℓ 0ℓ
    *-magma = record
      { isMagma = *-isMagma
      }

    *-isSemigroup : IsSemigroup _*_
    *-isSemigroup = record
      { isMagma = *-isMagma
      ; assoc   = *-assoc
      }

    *-semigroup : Semigroup 0ℓ 0ℓ
    *-semigroup = record
      { isSemigroup = *-isSemigroup
      }

    *-isCommutativeSemigroup : IsCommutativeSemigroup _*_
    *-isCommutativeSemigroup = record
      { isSemigroup = *-isSemigroup
      ; comm = *-comm
      }

    *-commutativeSemigroup : CommutativeSemigroup 0ℓ 0ℓ
    *-commutativeSemigroup = record
      { isCommutativeSemigroup = *-isCommutativeSemigroup
      }

    *-isMonoid : IsMonoid _*_ +
    *-isMonoid = record
      { isSemigroup = *-isSemigroup
      ; identity    = *-identity
      }

    *-monoid : Monoid 0ℓ 0ℓ
    *-monoid = record
      { isMonoid = *-isMonoid
      }

    *-isCommutativeMonoid : IsCommutativeMonoid _*_ +
    *-isCommutativeMonoid = record
       { isMonoid = *-isMonoid
       ; comm = *-comm
       }

    *-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
    *-commutativeMonoid = record
      { isCommutativeMonoid = *-isCommutativeMonoid
      }

    *-isGroup : IsGroup _*_ + id
    *-isGroup = record
      { isMonoid = *-isMonoid
      ; inverse = *-inverse
      ; ⁻¹-cong = id
      }

    *-group : Group 0ℓ 0ℓ
    *-group = record
      { isGroup = *-isGroup
      }

    *-isAbelianGroup : IsAbelianGroup _*_ + id
    *-isAbelianGroup = record
      { isGroup = *-isGroup
      ; comm = *-comm
      }

    *-abelianGroup : AbelianGroup 0ℓ 0ℓ
    *-abelianGroup = record
      { isAbelianGroup = *-isAbelianGroup
      }

    -- Other properties of _*_

    s*opposite[s]≡- : ∀ s → s * opposite s ≡ -
    s*opposite[s]≡- + = refl
    s*opposite[s]≡- - = refl

    opposite[s]*s≡- : ∀ s → opposite s * s ≡ -
    opposite[s]*s≡- + = refl
    opposite[s]*s≡- - = refl