------------------------------------------------------------------------
-- The Agda standard library
--
-- Algebraic properties of constructions over unary relations
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Relation.Unary.Algebra where
open import Algebra.Bundles
using (Magma; Semigroup; Band
; Monoid; CommutativeMonoid; IdempotentCommutativeMonoid
; SemiringWithoutAnnihilatingZero; Semiring; CommutativeSemiring)
import Algebra.Definitions as AlgebraicDefinitions
open import Algebra.Lattice.Bundles
using (Semilattice; Lattice; DistributiveLattice)
import Algebra.Lattice.Structures as AlgebraicLatticeStructures
using (IsLattice; IsDistributiveLattice; IsSemilattice)
import Algebra.Structures as AlgebraicStructures
using (IsMagma; IsSemigroup; IsBand; IsMonoid; IsCommutativeMonoid
; IsIdempotentCommutativeMonoid; IsSemiringWithoutAnnihilatingZero
; IsSemiring; IsCommutativeSemiring)
open import Data.Empty.Polymorphic using (⊥-elim)
open import Data.Product.Base as Product
using (_,_; proj₁; proj₂; <_,_>; curry; uncurry)
open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_])
open import Data.Unit.Polymorphic using (tt)
open import Function.Base using (id; const; _∘_)
open import Level using (Level; _⊔_)
open import Relation.Unary hiding (∅; U)
open import Relation.Unary.Polymorphic using (∅; U)
open import Relation.Unary.Relation.Binary.Equality using (≐-isEquivalence)
module _ {a ℓ : Level} {A : Set a} where
open AlgebraicDefinitions {A = Pred A ℓ} _≐_
------------------------------------------------------------------------
-- Properties of _∩_
∩-cong : Congruent₂ _∩_
∩-cong (P⊆Q , Q⊆P) (R⊆S , S⊆R) = Product.map P⊆Q R⊆S , Product.map Q⊆P S⊆R
∩-comm : Commutative _∩_
∩-comm _ _ = Product.swap , Product.swap
∩-assoc : Associative _∩_
∩-assoc _ _ _ = Product.assocʳ′ , Product.assocˡ′
∩-idem : Idempotent _∩_
∩-idem _ = proj₁ , < id , id >
∩-identityˡ : LeftIdentity U _∩_
∩-identityˡ _ = proj₂ , < const tt , id >
∩-identityʳ : RightIdentity U _∩_
∩-identityʳ _ = proj₁ , < id , const tt >
∩-identity : Identity U _∩_
∩-identity = ∩-identityˡ , ∩-identityʳ
∩-zeroˡ : LeftZero ∅ _∩_
∩-zeroˡ _ = proj₁ , ⊥-elim
∩-zeroʳ : RightZero ∅ _∩_
∩-zeroʳ _ = proj₂ , ⊥-elim
∩-zero : Zero ∅ _∩_
∩-zero = ∩-zeroˡ , ∩-zeroʳ
------------------------------------------------------------------------
-- Properties of _∪_
∪-cong : Congruent₂ _∪_
∪-cong (P⊆Q , Q⊆P) (R⊆S , S⊆R) = Sum.map P⊆Q R⊆S , Sum.map Q⊆P S⊆R
∪-comm : Commutative _∪_
∪-comm _ _ = Sum.swap , Sum.swap
∪-assoc : Associative _∪_
∪-assoc _ _ _ = Sum.assocʳ , Sum.assocˡ
∪-idem : Idempotent _∪_
∪-idem _ = [ id , id ] , inj₁
∪-identityˡ : LeftIdentity ∅ _∪_
∪-identityˡ _ = [ ⊥-elim , id ] , inj₂
∪-identityʳ : RightIdentity ∅ _∪_
∪-identityʳ _ = [ id , ⊥-elim ] , inj₁
∪-identity : Identity ∅ _∪_
∪-identity = ∪-identityˡ , ∪-identityʳ
------------------------------------------------------------------------
-- Properties of _∩_ and _∪_
∩-distribˡ-∪ : _∩_ DistributesOverˡ _∪_
∩-distribˡ-∪ _ _ _ =
( uncurry (λ x∈P → [ inj₁ ∘ (x∈P ,_) , inj₂ ∘ (x∈P ,_) ])
, [ Product.map₂ inj₁ , Product.map₂ inj₂ ]
)
∩-distribʳ-∪ : _∩_ DistributesOverʳ _∪_
∩-distribʳ-∪ _ _ _ =
( uncurry [ curry inj₁ , curry inj₂ ]
, [ Product.map₁ inj₁ , Product.map₁ inj₂ ]
)
∩-distrib-∪ : _∩_ DistributesOver _∪_
∩-distrib-∪ = ∩-distribˡ-∪ , ∩-distribʳ-∪
∪-distribˡ-∩ : _∪_ DistributesOverˡ _∩_
∪-distribˡ-∩ _ _ _ =
( [ < inj₁ , inj₁ > , Product.map inj₂ inj₂ ]
, uncurry [ const ∘ inj₁ , (λ x∈Q → [ inj₁ , inj₂ ∘ (x∈Q ,_) ]) ]
)
∪-distribʳ-∩ : _∪_ DistributesOverʳ _∩_
∪-distribʳ-∩ _ _ _ =
( [ Product.map inj₁ inj₁ , < inj₂ , inj₂ > ]
, uncurry [ (λ x∈Q → [ inj₁ ∘ (x∈Q ,_) , inj₂ ]) , const ∘ inj₂ ]
)
∪-distrib-∩ : _∪_ DistributesOver _∩_
∪-distrib-∩ = ∪-distribˡ-∩ , ∪-distribʳ-∩
∩-abs-∪ : _∩_ Absorbs _∪_
∩-abs-∪ _ _ = proj₁ , < id , inj₁ >
∪-abs-∩ : _∪_ Absorbs _∩_
∪-abs-∩ _ _ = [ id , proj₁ ] , inj₁
∪-∩-absorptive : Absorptive _∪_ _∩_
∪-∩-absorptive = ∪-abs-∩ , ∩-abs-∪
∩-∪-absorptive : Absorptive _∩_ _∪_
∩-∪-absorptive = ∩-abs-∪ , ∪-abs-∩
module _ {a : Level} (A : Set a) (ℓ : Level) where
open AlgebraicStructures {A = Pred A ℓ} _≐_
open AlgebraicLatticeStructures {A = Pred A ℓ} _≐_
------------------------------------------------------------------------
-- Algebraic structures of _∩_
∩-isMagma : IsMagma _∩_
∩-isMagma = record
{ isEquivalence = ≐-isEquivalence
; ∙-cong = ∩-cong
}
∩-isSemigroup : IsSemigroup _∩_
∩-isSemigroup = record
{ isMagma = ∩-isMagma
; assoc = ∩-assoc
}
∩-isBand : IsBand _∩_
∩-isBand = record
{ isSemigroup = ∩-isSemigroup
; idem = ∩-idem
}
∩-isSemilattice : IsSemilattice _∩_
∩-isSemilattice = record
{ isBand = ∩-isBand
; comm = ∩-comm
}
∩-isMonoid : IsMonoid _∩_ U
∩-isMonoid = record
{ isSemigroup = ∩-isSemigroup
; identity = ∩-identity
}
∩-isCommutativeMonoid : IsCommutativeMonoid _∩_ U
∩-isCommutativeMonoid = record
{ isMonoid = ∩-isMonoid
; comm = ∩-comm
}
∩-isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid _∩_ U
∩-isIdempotentCommutativeMonoid = record
{ isCommutativeMonoid = ∩-isCommutativeMonoid
; idem = ∩-idem
}
------------------------------------------------------------------------
-- Algebraic structures of _∪_
∪-isMagma : IsMagma _∪_
∪-isMagma = record
{ isEquivalence = ≐-isEquivalence
; ∙-cong = ∪-cong
}
∪-isSemigroup : IsSemigroup _∪_
∪-isSemigroup = record
{ isMagma = ∪-isMagma
; assoc = ∪-assoc
}
∪-isBand : IsBand _∪_
∪-isBand = record
{ isSemigroup = ∪-isSemigroup
; idem = ∪-idem
}
∪-isSemilattice : IsSemilattice _∪_
∪-isSemilattice = record
{ isBand = ∪-isBand
; comm = ∪-comm
}
∪-isMonoid : IsMonoid _∪_ ∅
∪-isMonoid = record
{ isSemigroup = ∪-isSemigroup
; identity = ∪-identity
}
∪-isCommutativeMonoid : IsCommutativeMonoid _∪_ ∅
∪-isCommutativeMonoid = record
{ isMonoid = ∪-isMonoid
; comm = ∪-comm
}
∪-isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid _∪_ ∅
∪-isIdempotentCommutativeMonoid = record
{ isCommutativeMonoid = ∪-isCommutativeMonoid
; idem = ∪-idem
}
------------------------------------------------------------------------
-- Algebraic structures of _∩_ and _∪_
∪-∩-isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _∪_ _∩_ ∅ U
∪-∩-isSemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = ∪-isCommutativeMonoid
; *-cong = ∩-cong
; *-assoc = ∩-assoc
; *-identity = ∩-identity
; distrib = ∩-distrib-∪
}
∪-∩-isSemiring : IsSemiring _∪_ _∩_ ∅ U
∪-∩-isSemiring = record
{ isSemiringWithoutAnnihilatingZero = ∪-∩-isSemiringWithoutAnnihilatingZero
; zero = ∩-zero
}
∪-∩-isCommutativeSemiring : IsCommutativeSemiring _∪_ _∩_ ∅ U
∪-∩-isCommutativeSemiring = record
{ isSemiring = ∪-∩-isSemiring
; *-comm = ∩-comm
}
∪-∩-isLattice : IsLattice _∪_ _∩_
∪-∩-isLattice = record
{ isEquivalence = ≐-isEquivalence
; ∨-comm = ∪-comm
; ∨-assoc = ∪-assoc
; ∨-cong = ∪-cong
; ∧-comm = ∩-comm
; ∧-assoc = ∩-assoc
; ∧-cong = ∩-cong
; absorptive = ∪-∩-absorptive
}
∪-∩-isDistributiveLattice : IsDistributiveLattice _∪_ _∩_
∪-∩-isDistributiveLattice = record
{ isLattice = ∪-∩-isLattice
; ∨-distrib-∧ = ∪-distrib-∩
; ∧-distrib-∨ = ∩-distrib-∪
}
∩-∪-isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _∩_ _∪_ U ∅
∩-∪-isSemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = ∩-isCommutativeMonoid
; *-cong = ∪-cong
; *-assoc = ∪-assoc
; *-identity = ∪-identity
; distrib = ∪-distrib-∩
}
------------------------------------------------------------------------
-- Algebraic bundles of _∩_
∩-magma : Magma _ _
∩-magma = record
{ isMagma = ∩-isMagma
}
∩-semigroup : Semigroup _ _
∩-semigroup = record
{ isSemigroup = ∩-isSemigroup
}
∩-band : Band _ _
∩-band = record
{ isBand = ∩-isBand
}
∩-semilattice : Semilattice _ _
∩-semilattice = record
{ isSemilattice = ∩-isSemilattice
}
∩-monoid : Monoid _ _
∩-monoid = record
{ isMonoid = ∩-isMonoid
}
∩-commutativeMonoid : CommutativeMonoid _ _
∩-commutativeMonoid = record
{ isCommutativeMonoid = ∩-isCommutativeMonoid
}
∩-idempotentCommutativeMonoid : IdempotentCommutativeMonoid _ _
∩-idempotentCommutativeMonoid = record
{ isIdempotentCommutativeMonoid = ∩-isIdempotentCommutativeMonoid
}
------------------------------------------------------------------------
-- Algebraic bundles of _∪_
∪-magma : Magma _ _
∪-magma = record
{ isMagma = ∪-isMagma
}
∪-semigroup : Semigroup _ _
∪-semigroup = record
{ isSemigroup = ∪-isSemigroup
}
∪-band : Band _ _
∪-band = record
{ isBand = ∪-isBand
}
∪-semilattice : Semilattice _ _
∪-semilattice = record
{ isSemilattice = ∪-isSemilattice
}
∪-monoid : Monoid _ _
∪-monoid = record
{ isMonoid = ∪-isMonoid
}
∪-commutativeMonoid : CommutativeMonoid _ _
∪-commutativeMonoid = record
{ isCommutativeMonoid = ∪-isCommutativeMonoid
}
∪-idempotentCommutativeMonoid : IdempotentCommutativeMonoid _ _
∪-idempotentCommutativeMonoid = record
{ isIdempotentCommutativeMonoid = ∪-isIdempotentCommutativeMonoid
}
------------------------------------------------------------------------
-- Algebraic bundles of _∩_ and _∪_
∪-∩-semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero _ _
∪-∩-semiringWithoutAnnihilatingZero = record
{ isSemiringWithoutAnnihilatingZero = ∪-∩-isSemiringWithoutAnnihilatingZero
}
∪-∩-semiring : Semiring _ _
∪-∩-semiring = record
{ isSemiring = ∪-∩-isSemiring
}
∪-∩-commutativeSemiring : CommutativeSemiring _ _
∪-∩-commutativeSemiring = record
{ isCommutativeSemiring = ∪-∩-isCommutativeSemiring
}
∪-∩-lattice : Lattice _ _
∪-∩-lattice = record
{ isLattice = ∪-∩-isLattice
}
∪-∩-distributiveLattice : DistributiveLattice _ _
∪-∩-distributiveLattice = record
{ isDistributiveLattice = ∪-∩-isDistributiveLattice
}
∩-∪-semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero _ _
∩-∪-semiringWithoutAnnihilatingZero = record
{ isSemiringWithoutAnnihilatingZero = ∩-∪-isSemiringWithoutAnnihilatingZero
}
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