------------------------------------------------------------------------
-- 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  ε∣ʳ_

ε∣ʳ_ : ∀ 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  ε∣ˡ_

ε∣ˡ_ : ∀ 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  ε∣_
ε∣_ = ε∣ʳ_
{-# 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. "
#-}