------------------------------------------------------------------------
-- The Agda standard library
--
-- Definitions of the lexicographic product of two operators.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Bundles using (Magma)
open import Algebra.Definitions
open import Data.Bool.Base using (true; false)
open import Data.Product.Base using (_×_; _,_)
open import Data.Product.Relation.Binary.Pointwise.NonDependent using (Pointwise)
open import Data.Sum.Base using (inj₁; inj₂; map)
open import Function.Base using (_∘_)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Nullary.Decidable.Core using (does; yes; no)
open import Relation.Nullary.Negation.Core using (¬_; contradiction; contradiction₂)
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
module Algebra.Construct.LexProduct
{ℓ₁ ℓ₂ ℓ₃ ℓ₄} (M : Magma ℓ₁ ℓ₂) (N : Magma ℓ₃ ℓ₄)
(_≟₁_ : Decidable (Magma._≈_ M))
where
open Magma M using (_∙_ ; ∙-cong)
renaming
( Carrier to A
; _≈_ to _≈₁_
; _≉_ to _≉₁_
)
open Magma N using ()
renaming
( Carrier to B
; _∙_ to _◦_
; _≈_ to _≈₂_
; refl to ≈₂-refl
)
import Algebra.Construct.LexProduct.Inner M N _≟₁_ as InnerLex
private
infix 4 _≋_
_≋_ : Rel (A × B) _
_≋_ = Pointwise _≈₁_ _≈₂_
variable
a b : A
------------------------------------------------------------------------
-- Definition
------------------------------------------------------------------------
open import Algebra.Construct.LexProduct.Base _∙_ _◦_ _≟₁_ public
renaming (lex to _⊕_)
------------------------------------------------------------------------
-- Properties
------------------------------------------------------------------------
-- Basic cases
case₁ : ∀ {a b} → (a ∙ b) ≈₁ a → (a ∙ b) ≉₁ b →
∀ x y → (a , x) ⊕ (b , y) ≋ (a , x)
case₁ ab≈a ab≉b _ _ = ab≈a , InnerLex.case₁ ab≈a ab≉b
case₂ : ∀ {a b} → (a ∙ b) ≉₁ a → (a ∙ b) ≈₁ b →
∀ x y → (a , x) ⊕ (b , y) ≋ (b , y)
case₂ ab≉a ab≈b _ _ = ab≈b , InnerLex.case₂ ab≉a ab≈b
case₃ : ∀ {a b} → (a ∙ b) ≈₁ a → (a ∙ b) ≈₁ b →
∀ x y → (a , x) ⊕ (b , y) ≋ (a , x ◦ y)
case₃ ab≈a ab≈b _ _ = ab≈a , InnerLex.case₃ ab≈a ab≈b
------------------------------------------------------------------------
-- Algebraic properties
cong : Congruent₂ _≋_ _⊕_
cong (a≈b , w≈x) (c≈d , y≈z) =
∙-cong a≈b c≈d ,
InnerLex.cong a≈b c≈d w≈x y≈z
assoc : Associative _≈₁_ _∙_ → Commutative _≈₁_ _∙_ →
Selective _≈₁_ _∙_ → Associative _≈₂_ _◦_ →
Associative _≋_ _⊕_
assoc ∙-assoc ∙-comm ∙-sel ◦-assoc (a , x) (b , y) (c , z) =
∙-assoc a b c ,
InnerLex.assoc ∙-assoc ∙-comm ∙-sel ◦-assoc a b c x y z
comm : Commutative _≈₁_ _∙_ → Commutative _≈₂_ _◦_ →
Commutative _≋_ _⊕_
comm ∙-comm ◦-comm (a , x) (b , y) =
∙-comm a b ,
InnerLex.comm ∙-comm ◦-comm a b x y
zeroʳ : ∀ {e f} → RightZero _≈₁_ e _∙_ → RightZero _≈₂_ f _◦_ →
RightZero _≋_ (e , f) _⊕_
zeroʳ ze₁ ze₂ (x , a) = ze₁ x , InnerLex.zeroʳ ze₁ ze₂
identityʳ : ∀ {e f} → RightIdentity _≈₁_ e _∙_ → RightIdentity _≈₂_ f _◦_ →
RightIdentity _≋_ (e , f) _⊕_
identityʳ id₁ id₂ (x , a) = id₁ x , InnerLex.identityʳ id₁ id₂
sel : Selective _≈₁_ _∙_ → Selective _≈₂_ _◦_ → Selective _≋_ _⊕_
sel ∙-sel ◦-sel (a , x) (b , y) with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b
... | no ab≉a | no ab≉b = contradiction₂ (∙-sel a b) ab≉a ab≉b
... | yes ab≈a | no _ = inj₁ (ab≈a , ≈₂-refl)
... | no _ | yes ab≈b = inj₂ (ab≈b , ≈₂-refl)
... | yes ab≈a | yes ab≈b = map (ab≈a ,_) (ab≈b ,_) (◦-sel x y)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4