------------------------------------------------------------------------ -- The Agda standard library -- -- Algebraic properties of products ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Data.Product.Algebra where open import Algebra open import Data.Bool.Base using (true; false) open import Data.Empty.Polymorphic using (⊥; ⊥-elim) open import Data.Product.Base open import Data.Product.Properties open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′) open import Data.Sum.Algebra open import Data.Unit.Polymorphic using (⊤; tt) open import Function.Base using (_∘′_) open import Function.Bundles using (_↔_; Inverse; mk↔ₛ′) open import Function.Properties.Inverse using (↔-isEquivalence) open import Level using (Level; suc) open import Relation.Binary.PropositionalEquality.Core import Function.Definitions as FuncDef ------------------------------------------------------------------------ private variable a b c d p : Level A B C D : Set a ------------------------------------------------------------------------ -- Properties of Σ -- Σ is associative Σ-assoc : {B : A → Set b} {C : (a : A) → B a → Set c} → Σ (Σ A B) (uncurry C) ↔ Σ A (λ a → Σ (B a) (C a)) Σ-assoc = mk↔ₛ′ assocʳ assocˡ cong′ cong′ -- Σ is associative, alternate formulation Σ-assoc-alt : {B : A → Set b} {C : Σ A B → Set c} → Σ (Σ A B) C ↔ Σ A (λ a → Σ (B a) (curry C a)) Σ-assoc-alt = mk↔ₛ′ assocʳ-curried assocˡ-curried cong′ cong′ ------------------------------------------------------------------------ -- Algebraic properties -- × is a congruence ×-cong : A ↔ B → C ↔ D → (A × C) ↔ (B × D) ×-cong i j = mk↔ₛ′ (map I.to J.to) (map I.from J.from) (λ {(a , b) → cong₂ _,_ (I.strictlyInverseˡ a) (J.strictlyInverseˡ b)}) (λ {(a , b) → cong₂ _,_ (I.strictlyInverseʳ a) (J.strictlyInverseʳ b)}) where module I = Inverse i; module J = Inverse j -- × is commutative. -- (we don't use Commutative because it isn't polymorphic enough) ×-comm : (A : Set a) (B : Set b) → (A × B) ↔ (B × A) ×-comm _ _ = mk↔ₛ′ swap swap swap-involutive swap-involutive module _ (ℓ : Level) where -- × is associative ×-assoc : Associative {ℓ = ℓ} _↔_ _×_ ×-assoc _ _ _ = mk↔ₛ′ assocʳ′ assocˡ′ cong′ cong′ -- ⊤ is the identity for × ×-identityˡ : LeftIdentity {ℓ = ℓ} _↔_ ⊤ _×_ ×-identityˡ _ = mk↔ₛ′ proj₂ (tt ,_) cong′ cong′ ×-identityʳ : RightIdentity {ℓ = ℓ} _↔_ ⊤ _×_ ×-identityʳ _ = mk↔ₛ′ proj₁ (_, tt) cong′ cong′ ×-identity : Identity _↔_ ⊤ _×_ ×-identity = ×-identityˡ , ×-identityʳ -- ⊥ is the zero for × ×-zeroˡ : LeftZero {ℓ = ℓ} _↔_ ⊥ _×_ ×-zeroˡ A = mk↔ₛ′ proj₁ ⊥-elim ⊥-elim λ () ×-zeroʳ : RightZero {ℓ = ℓ} _↔_ ⊥ _×_ ×-zeroʳ A = mk↔ₛ′ proj₂ ⊥-elim ⊥-elim λ () ×-zero : Zero _↔_ ⊥ _×_ ×-zero = ×-zeroˡ , ×-zeroʳ -- × distributes over ⊎ ×-distribˡ-⊎ : _DistributesOverˡ_ {ℓ = ℓ} _↔_ _×_ _⊎_ ×-distribˡ-⊎ _ _ _ = mk↔ₛ′ (uncurry λ x → [ inj₁ ∘′ (x ,_) , inj₂ ∘′ (x ,_) ]′) [ map₂ inj₁ , map₂ inj₂ ]′ Sum.[ cong′ , cong′ ] (uncurry λ _ → Sum.[ cong′ , cong′ ]) ×-distribʳ-⊎ : _DistributesOverʳ_ {ℓ = ℓ} _↔_ _×_ _⊎_ ×-distribʳ-⊎ _ _ _ = mk↔ₛ′ (uncurry [ curry inj₁ , curry inj₂ ]′) [ map₁ inj₁ , map₁ inj₂ ]′ Sum.[ cong′ , cong′ ] (uncurry Sum.[ (λ _ → cong′) , (λ _ → cong′) ]) ×-distrib-⊎ : _DistributesOver_ {ℓ = ℓ} _↔_ _×_ _⊎_ ×-distrib-⊎ = ×-distribˡ-⊎ , ×-distribʳ-⊎ ------------------------------------------------------------------------ -- Algebraic structures ×-isMagma : IsMagma {ℓ = ℓ} _↔_ _×_ ×-isMagma = record { isEquivalence = ↔-isEquivalence ; ∙-cong = ×-cong } ×-isSemigroup : IsSemigroup _↔_ _×_ ×-isSemigroup = record { isMagma = ×-isMagma ; assoc = λ _ _ _ → Σ-assoc } ×-isMonoid : IsMonoid _↔_ _×_ ⊤ ×-isMonoid = record { isSemigroup = ×-isSemigroup ; identity = ×-identityˡ , ×-identityʳ } ×-isCommutativeMonoid : IsCommutativeMonoid _↔_ _×_ ⊤ ×-isCommutativeMonoid = record { isMonoid = ×-isMonoid ; comm = ×-comm } ⊎-×-isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _↔_ _⊎_ _×_ ⊥ ⊤ ⊎-×-isSemiringWithoutAnnihilatingZero = record { +-isCommutativeMonoid = ⊎-isCommutativeMonoid ℓ ; *-cong = ×-cong ; *-assoc = ×-assoc ; *-identity = ×-identity ; distrib = ×-distrib-⊎ } ⊎-×-isSemiring : IsSemiring _↔_ _⊎_ _×_ ⊥ ⊤ ⊎-×-isSemiring = record { isSemiringWithoutAnnihilatingZero = ⊎-×-isSemiringWithoutAnnihilatingZero ; zero = ×-zero } ⊎-×-isCommutativeSemiring : IsCommutativeSemiring _↔_ _⊎_ _×_ ⊥ ⊤ ⊎-×-isCommutativeSemiring = record { isSemiring = ⊎-×-isSemiring ; *-comm = ×-comm } ------------------------------------------------------------------------ -- Algebraic bundles ×-magma : Magma (suc ℓ) ℓ ×-magma = record { isMagma = ×-isMagma } ×-semigroup : Semigroup (suc ℓ) ℓ ×-semigroup = record { isSemigroup = ×-isSemigroup } ×-monoid : Monoid (suc ℓ) ℓ ×-monoid = record { isMonoid = ×-isMonoid } ×-commutativeMonoid : CommutativeMonoid (suc ℓ) ℓ ×-commutativeMonoid = record { isCommutativeMonoid = ×-isCommutativeMonoid } ×-⊎-commutativeSemiring : CommutativeSemiring (suc ℓ) ℓ ×-⊎-commutativeSemiring = record { isCommutativeSemiring = ⊎-×-isCommutativeSemiring }