------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of divisibility over monoids
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Bundles using (Monoid)
module Algebra.Properties.Monoid.Divisibility
{a ℓ} (M : Monoid a ℓ) where
open import Data.Product.Base using (_,_)
open import Relation.Binary.Core using (_⇒_)
open import Relation.Binary.Bundles using (Preorder)
open import Relation.Binary.Structures using (IsPreorder; IsEquivalence)
open import Relation.Binary.Definitions using (Reflexive)
open Monoid M
------------------------------------------------------------------------
-- Re-export semigroup divisibility
open import Algebra.Properties.Semigroup.Divisibility semigroup public
------------------------------------------------------------------------
-- Additional properties for right divisibility
infix 4 ε∣ʳ_
ε∣ʳ_ : ∀ x → ε ∣ʳ x
ε∣ʳ x = x , identityʳ x
∣ʳ-refl : Reflexive _∣ʳ_
∣ʳ-refl {x} = ε , identityˡ x
∣ʳ-reflexive : _≈_ ⇒ _∣ʳ_
∣ʳ-reflexive x≈y = ε , trans (identityˡ _) x≈y
∣ʳ-isPreorder : IsPreorder _≈_ _∣ʳ_
∣ʳ-isPreorder = record
{ isEquivalence = isEquivalence
; reflexive = ∣ʳ-reflexive
; trans = ∣ʳ-trans
}
∣ʳ-preorder : Preorder a ℓ _
∣ʳ-preorder = record
{ isPreorder = ∣ʳ-isPreorder
}
------------------------------------------------------------------------
-- Additional properties for left divisibility
infix 4 ε∣ˡ_
ε∣ˡ_ : ∀ x → ε ∣ˡ x
ε∣ˡ x = x , identityˡ x
∣ˡ-refl : Reflexive _∣ˡ_
∣ˡ-refl {x} = ε , identityʳ x
∣ˡ-reflexive : _≈_ ⇒ _∣ˡ_
∣ˡ-reflexive x≈y = ε , trans (identityʳ _) x≈y
∣ˡ-isPreorder : IsPreorder _≈_ _∣ˡ_
∣ˡ-isPreorder = record
{ isEquivalence = isEquivalence
; reflexive = ∣ˡ-reflexive
; trans = ∣ˡ-trans
}
∣ˡ-preorder : Preorder a ℓ _
∣ˡ-preorder = record
{ isPreorder = ∣ˡ-isPreorder
}
------------------------------------------------------------------------
-- Properties of mutual divisibiity
∥-refl : Reflexive _∥_
∥-refl = ∣ʳ-refl , ∣ʳ-refl
∥-reflexive : _≈_ ⇒ _∥_
∥-reflexive x≈y = ∣ʳ-reflexive x≈y , ∣ʳ-reflexive (sym x≈y)
∥-isEquivalence : IsEquivalence _∥_
∥-isEquivalence = record
{ refl = ∥-refl
; sym = ∥-sym
; trans = ∥-trans
}
------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.
-- Version 2.3
∣∣-refl = ∥-refl
{-# WARNING_ON_USAGE ∣∣-refl
"Warning: ∣∣-refl was deprecated in v2.3.
Please use ∥-refl instead. "
#-}
∣∣-reflexive = ∥-reflexive
{-# WARNING_ON_USAGE ∣∣-reflexive
"Warning: ∣∣-reflexive was deprecated in v2.3.
Please use ∥-reflexive instead. "
#-}
∣∣-isEquivalence = ∥-isEquivalence
{-# WARNING_ON_USAGE ∣∣-isEquivalence
"Warning: ∣∣-isEquivalence was deprecated in v2.3.
Please use ∥-isEquivalence instead. "
#-}
infix 4 ε∣_
ε∣_ = ε∣ʳ_
{-# WARNING_ON_USAGE ε∣_
"Warning: ε∣_ was deprecated in v2.3.
Please use ε∣ʳ_ instead. "
#-}
∣-refl = ∣ʳ-refl
{-# WARNING_ON_USAGE ∣-refl
"Warning: ∣-refl was deprecated in v2.3.
Please use ∣ʳ-refl instead. "
#-}
∣-reflexive = ∣ʳ-reflexive
{-# WARNING_ON_USAGE ∣-reflexive
"Warning: ∣-reflexive was deprecated in v2.3.
Please use ∣ʳ-reflexive instead. "
#-}
∣-isPreorder = ∣ʳ-isPreorder
{-# WARNING_ON_USAGE ∣ʳ-isPreorder
"Warning: ∣-isPreorder was deprecated in v2.3.
Please use ∣ʳ-isPreorder instead. "
#-}
∣-preorder = ∣ʳ-preorder
{-# WARNING_ON_USAGE ∣-preorder
"Warning: ∣-preorder was deprecated in v2.3.
Please use ∣ʳ-preorder instead. "
#-}
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