Classical.Bundles.Ring

Bundle bridge for rings

This is the Classical.Bundles.Ring module of the Agda Universal Algebra Library.

Here we encode the bidirectional bridge between the Σ-typed core of Classical.Structures.Ring and the record-typed Algebra.Bundles.Ring in the standard library. The round-trip is stated pointwise;¹ the eleven curried laws arrive ready-made from Ring-Op, so the core-to-bundle direction is a (deeply nested) record-shuffle and the reverse direction is one Func plus the eleven equation clauses.

{-# OPTIONS --without-K --exact-split --safe #-}

module Classical.Bundles.Ring where

-- Imports from the Agda Standard Library -----------------------------------------
open import Algebra.Bundles     using () renaming ( Ring to stdlib-Ring )
open import Data.Fin.Patterns   using ( 0F ; 1F ; 2F )
open import Data.Product        using ( _,_ )
open import Function            using ( Func )
open import Level               using ( Level )
open import Relation.Binary     using ( Setoid )
import Relation.Binary.PropositionalEquality as ≡
open Func renaming ( to to _⟨$⟩_ )

-- Imports from the Agda Universal Algebra Library --------------------------------
open import Classical.Signatures.Ring  using  ( Sig-Ring ; +-Op ; 0-Op
                                              ; -Op ; ·-Op ; 1-Op )
open import Classical.Structures.Ring  using  ( Ring ; module Ring-Op )
open import Classical.Theories.Ring    using  ( +-assoc ; +-idˡ ; +-idʳ ; +-invˡ
                                              ; +-invʳ ; +-comm ; ·-assoc ; ·-idˡ
                                              ; ·-idʳ ; distribˡ ; distribʳ )
open import Setoid.Algebras.Basic      using  ( Algebra ; 𝕌[_] ; 𝔻[_] )
open import Setoid.Signatures          using  ( ⟨_⟩ )

private variable α ρ : Level

Core to stdlib bundle

⟨_⟩ʳᵍ : Ring α ρ → stdlib-Ring α ρ
⟨ 𝑹 , eqns ⟩ʳᵍ = record
  { Carrier = 𝕌[ 𝑹 ]
  ; _≈_     = _≈_
  ; _+_     = _+_
  ; _*_     = _·_
  ; -_      = -_
  ; 0#      = 0R
  ; 1#      = 1R
  ; isRing  = record
      { +-isAbelianGroup = record
          { isGroup = record
              { isMonoid = record
                  { isSemigroup = record
                      { isMagma = record { isEquivalence = isEquivalence ; ∙-cong = +-cong }
                      ; assoc   = +-assoc-law
                      }
                  ; identity = +-idˡ-law , +-idʳ-law
                  }
              ; inverse = +-invˡ-law , +-invʳ-law
              ; ⁻¹-cong = neg-cong
              }
          ; comm = +-comm-law
          }
      ; *-cong     = ·-cong
      ; *-assoc    = ·-assoc-law
      ; *-identity = ·-idˡ-law , ·-idʳ-law
      ; distrib    = distribˡ-law , distribʳ-law
      }
  }
  where
  open Ring-Op (𝑹 , eqns)
  open Setoid 𝔻[ 𝑹 ]

Stdlib bundle to core

The reverse direction reassembles the bundle's carrier setoid and five operations into a Sig-Ring-algebra and pairs it with a proof of Th-Ring, each of the eleven equations extracted from the corresponding record field applied to the variables the environment supplies. The interpretation has one clause per operation symbol, and congruence likewise: +-cong, *-cong, and -‿cong come from the bundle, and the two nullary cases (0-Op, 1-Op) are the setoid's reflexivity.

⟪_⟫ʳᵍ : stdlib-Ring α ρ → Ring α ρ
⟪ R ⟫ʳᵍ = 𝑨 , λ  { +-assoc   ρ → R-+assoc    (ρ 0F) (ρ 1F) (ρ 2F)
                 ; +-idˡ     ρ → R-+idˡ      (ρ 0F)
                 ; +-idʳ     ρ → R-+idʳ      (ρ 0F)
                 ; +-invˡ    ρ → R-+invˡ     (ρ 0F)
                 ; +-invʳ    ρ → R-+invʳ     (ρ 0F)
                 ; +-comm    ρ → R-+comm     (ρ 0F) (ρ 1F)
                 ; ·-assoc   ρ → R-*assoc    (ρ 0F) (ρ 1F) (ρ 2F)
                 ; ·-idˡ     ρ → R-*idˡ      (ρ 0F)
                 ; ·-idʳ     ρ → R-*idʳ      (ρ 0F)
                 ; distribˡ  ρ → R-distribˡ  (ρ 0F) (ρ 1F) (ρ 2F)
                 ; distribʳ  ρ → R-distribʳ  (ρ 0F) (ρ 1F) (ρ 2F) }
  where
  open stdlib-Ring R using ( setoid ; +-cong ; -‿cong ; *-cong )
    renaming  ( _+_         to _⊕_         ; _*_         to _⊛_ ; -_  to ⊖_
              ; 0#          to z           ; 1#          to e
              ; +-assoc     to R-+assoc    ; +-comm      to R-+comm
              ; +-identityˡ to R-+idˡ      ; +-identityʳ to R-+idʳ
              ; -‿inverseˡ  to R-+invˡ     ; -‿inverseʳ  to R-+invʳ
              ; *-assoc     to R-*assoc
              ; *-identityˡ to R-*idˡ      ; *-identityʳ to R-*idʳ
              ; distribˡ    to R-distribˡ  ; distribʳ    to R-distribʳ )

  𝑨 : Algebra {𝑆 = Sig-Ring} _ _
  𝑨 = record { Domain = setoid ; Interp = interp }
    where
    interp : Func (⟨ Sig-Ring ⟩ setoid) setoid
    interp ⟨$⟩ (+-Op , args)                             = args 0F ⊕ args 1F
    interp ⟨$⟩ (0-Op , _)                                = z
    interp ⟨$⟩ (-Op  , args)                             = ⊖ (args 0F)
    interp ⟨$⟩ (·-Op , args)                             = args 0F ⊛ args 1F
    interp ⟨$⟩ (1-Op , _)                                = e
    cong interp {+-Op , _} {.+-Op , _} (≡.refl , args≈)  = +-cong (args≈ 0F) (args≈ 1F)
    cong interp {0-Op , _} {.0-Op , _} (≡.refl , _)      = Setoid.refl setoid
    cong interp { -Op , _} {.-Op  , _} (≡.refl , args≈)  = -‿cong (args≈ 0F)
    cong interp {·-Op , _} {.·-Op , _} (≡.refl , args≈)  = *-cong (args≈ 0F) (args≈ 1F)
    cong interp {1-Op , _} {.1-Op , _} (≡.refl , _)      = Setoid.refl setoid

Pointwise round-trip

Both round-trips are definitional, stated pointwise per operation, five in each direction.

Going core to bundle and back, roundtrip-cbc-+-ring, roundtrip-cbc-·-ring, roundtrip-cbc-neg-ring, roundtrip-cbc-0-ring, and roundtrip-cbc-1-ring say the reassembled operations and constants agree with the originals, each discharged by the ring setoid's refl.

Going bundle to core and back, roundtrip-bcb-+-ring, roundtrip-bcb-·-ring, roundtrip-bcb-neg-ring, roundtrip-bcb-0-ring, and roundtrip-bcb-1-ring state the same agreement on the bundle's own equivalence.

module _ {(𝑹 , eqns) : Ring α ρ} where
  open Ring-Op (𝑹 , eqns)
  open Setoid 𝔻[ 𝑹 ]
  open Ring-Op ⟪ ⟨ 𝑹 , eqns ⟩ʳᵍ ⟫ʳᵍ renaming  ( _+_  to _+'_
                                              ; _·_  to _·'_
                                              ; -_   to -'_
                                              ; 0R   to 0R'
                                              ; 1R   to 1R' )

  roundtrip-cbc-+-ring : (a b : 𝕌[ 𝑹 ]) → a +' b ≈ a + b
  roundtrip-cbc-+-ring a b = refl

  roundtrip-cbc-·-ring : (a b : 𝕌[ 𝑹 ]) → a ·' b ≈ a · b
  roundtrip-cbc-·-ring a b = refl

  roundtrip-cbc-neg-ring : (a : 𝕌[ 𝑹 ]) → -' a ≈ - a
  roundtrip-cbc-neg-ring a = refl

  roundtrip-cbc-0-ring : 0R' ≈ 0R
  roundtrip-cbc-0-ring = refl

  roundtrip-cbc-1-ring : 1R' ≈ 1R
  roundtrip-cbc-1-ring = refl

module _ {R : stdlib-Ring α ρ} where

  open stdlib-Ring R  using ( _≈_ ; _+_ ; _*_ ; -_ ; 0# ; 1# ; refl )
                      renaming ( Carrier to A )

  open stdlib-Ring ⟨ ⟪ R ⟫ʳᵍ ⟩ʳᵍ using () renaming  ( _+_ to _+'_
                                                    ; _*_ to _*'_
                                                    ; -_  to -'_
                                                    ; 0#  to 0#'
                                                    ; 1#  to 1#' )

  roundtrip-bcb-+-ring : (a b : A) → a + b ≈ a +' b
  roundtrip-bcb-+-ring a b = refl

  roundtrip-bcb-·-ring : (a b : A) → a * b ≈ a *' b
  roundtrip-bcb-·-ring a b = refl

  roundtrip-bcb-neg-ring : (a : A) → - a ≈ -' a
  roundtrip-bcb-neg-ring a = refl

  roundtrip-bcb-0-ring : 0# ≈ 0#'
  roundtrip-bcb-0-ring = refl

  roundtrip-bcb-1-ring : 1# ≈ 1#'
  roundtrip-bcb-1-ring = refl

---

---

1. per ADR-002 v2 §6. ↩