    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Bundles for homogeneous binary relations
    ------------------------------------------------------------------------

    -- The contents of this module should be accessed via `Relation.Binary`.

    {-# OPTIONS --cubical-compatible --safe #-}

    module Relation.Binary.Bundles where

    open import Function.Base using (flip)
    open import Level using (Level; suc; _⊔_)
    open import Relation.Binary.Core using (Rel)
    open import Relation.Binary.Bundles.Raw using (RawRelation; RawSetoid)
    open import Relation.Binary.Structures -- most of it
    open import Relation.Nullary.Negation.Core using (¬_)

    ------------------------------------------------------------------------
    -- Setoids
    ------------------------------------------------------------------------

    record PartialSetoid a ℓ : Set (suc (a ⊔ ℓ)) where
      infix 4 _≈_
      field
        Carrier              : Set a
        _≈_                  : Rel Carrier ℓ
        isPartialEquivalence : IsPartialEquivalence _≈_

      open IsPartialEquivalence isPartialEquivalence public

      rawSetoid : RawSetoid _ _
      rawSetoid = record { _≈_ = _≈_ }

      open RawSetoid rawSetoid public
        hiding (Carrier; _≈_ )

    record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where
      infix 4 _≈_
      field
        Carrier       : Set c
        _≈_           : Rel Carrier ℓ
        isEquivalence : IsEquivalence _≈_

      open IsEquivalence isEquivalence public
        using (refl; reflexive; isPartialEquivalence)

      partialSetoid : PartialSetoid c ℓ
      partialSetoid = record
        { isPartialEquivalence = isPartialEquivalence
        }

      open PartialSetoid partialSetoid public
        hiding (Carrier; _≈_; isPartialEquivalence)

    record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where
      infix 4 _≈_
      field
        Carrier          : Set c
        _≈_              : Rel Carrier ℓ
        isDecEquivalence : IsDecEquivalence _≈_

      open IsDecEquivalence isDecEquivalence public
        using (_≟_; isEquivalence)

      setoid : Setoid c ℓ
      setoid = record
        { isEquivalence = isEquivalence
        }

      open Setoid setoid public
        hiding (Carrier; _≈_; isEquivalence)

    ------------------------------------------------------------------------
    -- Preorders
    ------------------------------------------------------------------------

    record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
      infix 4 _≈_ _≲_
      field
        Carrier    : Set c
        _≈_        : Rel Carrier ℓ₁  -- The underlying equality.
        _≲_        : Rel Carrier ℓ₂  -- The relation.
        isPreorder : IsPreorder _≈_ _≲_

      open IsPreorder isPreorder public
        hiding (module Eq)

      module Eq where
        setoid : Setoid c ℓ₁
        setoid = record
          { isEquivalence = isEquivalence
          }

        open Setoid setoid public

      rawRelation : RawRelation _ _ _
      rawRelation = record { _≈_ = _≈_ ; _∼_ = _≲_ }

      open RawRelation rawRelation public
        renaming (_≁_ to _⋦_; _∼ᵒ_ to _≳_; _≁ᵒ_ to _⋧_)
        hiding (Carrier; _≈_)
      -- Deprecated.
      {-# WARNING_ON_USAGE _∼_
      "Warning: _∼_ was deprecated in v2.0.
      Please use _≲_ instead. "
      #-}

    record TotalPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
      infix 4 _≈_ _≲_
      field
        Carrier         : Set c
        _≈_             : Rel Carrier ℓ₁  -- The underlying equality.
        _≲_             : Rel Carrier ℓ₂  -- The relation.
        isTotalPreorder : IsTotalPreorder _≈_ _≲_

      open IsTotalPreorder isTotalPreorder public
        using (total; isPreorder)

      preorder : Preorder c ℓ₁ ℓ₂
      preorder = record
        { isPreorder = isPreorder
        }

      open Preorder preorder public
        hiding (Carrier; _≈_; _≲_; isPreorder)

    record DecPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
      field
        Carrier         : Set c
        _≈_             : Rel Carrier ℓ₁  -- The underlying equality.
        _≲_             : Rel Carrier ℓ₂  -- The relation.
        isDecPreorder   : IsDecPreorder _≈_ _≲_

      private module DPO = IsDecPreorder isDecPreorder

      open DPO public
        using (_≟_; _≲?_; isPreorder)

      preorder : Preorder c ℓ₁ ℓ₂
      preorder = record
        { isPreorder = isPreorder
        }

      open Preorder preorder public
        hiding (Carrier; _≈_; _≲_; isPreorder; module Eq)

      module Eq where
        decSetoid : DecSetoid c ℓ₁
        decSetoid = record
          { isDecEquivalence = DPO.Eq.isDecEquivalence
          }

        open DecSetoid decSetoid public

    ------------------------------------------------------------------------
    -- Partial orders
    ------------------------------------------------------------------------

    record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
      infix 4 _≈_ _≤_
      field
        Carrier        : Set c
        _≈_            : Rel Carrier ℓ₁
        _≤_            : Rel Carrier ℓ₂
        isPartialOrder : IsPartialOrder _≈_ _≤_

      open IsPartialOrder isPartialOrder public
        using (antisym; isPreorder)

      preorder : Preorder c ℓ₁ ℓ₂
      preorder = record
        { isPreorder = isPreorder
        }

      open Preorder preorder public
        hiding (Carrier; _≈_; _≲_; isPreorder; _⋦_; _≳_; _⋧_)
        renaming
        ( ≲-respˡ-≈ to ≤-respˡ-≈
        ; ≲-respʳ-≈ to ≤-respʳ-≈
        ; ≲-resp-≈  to ≤-resp-≈
        )

      open RawRelation rawRelation public
        renaming (_≁_ to _≰_; _∼ᵒ_ to _≥_; _≁ᵒ_ to _≱_)
        hiding (Carrier; _≈_ ; _∼_; _≉_; rawSetoid)

    record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
      infix 4 _≈_ _≤_
      field
        Carrier           : Set c
        _≈_               : Rel Carrier ℓ₁
        _≤_               : Rel Carrier ℓ₂
        isDecPartialOrder : IsDecPartialOrder _≈_ _≤_

      private module DPO = IsDecPartialOrder isDecPartialOrder

      open DPO public
        using (_≟_; _≤?_; isPartialOrder; isDecPreorder)

      poset : Poset c ℓ₁ ℓ₂
      poset = record
        { isPartialOrder = isPartialOrder
        }

      open Poset poset public
        hiding (Carrier; _≈_; _≤_; isPartialOrder; module Eq)

      decPreorder : DecPreorder c ℓ₁ ℓ₂
      decPreorder = record { isDecPreorder = isDecPreorder }

      open DecPreorder decPreorder public
        using (module Eq)

    record StrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
      infix 4 _≈_ _<_
      field
        Carrier              : Set c
        _≈_                  : Rel Carrier ℓ₁
        _<_                  : Rel Carrier ℓ₂
        isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_

      open IsStrictPartialOrder isStrictPartialOrder public
        hiding (module Eq)

      module Eq where
        setoid : Setoid c ℓ₁
        setoid = record
          { isEquivalence = isEquivalence
          }

        open Setoid setoid public

      rawRelation : RawRelation _ _ _
      rawRelation = record { _≈_ = _≈_ ; _∼_ = _<_ }

      open RawRelation rawRelation public
        renaming (_≁_ to _≮_; _∼ᵒ_ to _>_; _≁ᵒ_ to _≯_)
        hiding (Carrier; _≈_ ; _∼_)

    record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
      infix 4 _≈_ _<_
      field
        Carrier                 : Set c
        _≈_                     : Rel Carrier ℓ₁
        _<_                     : Rel Carrier ℓ₂
        isDecStrictPartialOrder : IsDecStrictPartialOrder _≈_ _<_

      private module DSPO = IsDecStrictPartialOrder isDecStrictPartialOrder

      open DSPO public
        using (_<?_; _≟_; isStrictPartialOrder)

      strictPartialOrder : StrictPartialOrder c ℓ₁ ℓ₂
      strictPartialOrder = record
        { isStrictPartialOrder = isStrictPartialOrder
        }

      open StrictPartialOrder strictPartialOrder public
        hiding (Carrier; _≈_; _<_; isStrictPartialOrder; module Eq)

      module Eq where

        decSetoid : DecSetoid c ℓ₁
        decSetoid = record
          { isDecEquivalence = DSPO.Eq.isDecEquivalence
          }

        open DecSetoid decSetoid public

    ------------------------------------------------------------------------
    -- Total orders
    ------------------------------------------------------------------------

    record TotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
      infix 4 _≈_ _≤_
      field
        Carrier      : Set c
        _≈_          : Rel Carrier ℓ₁
        _≤_          : Rel Carrier ℓ₂
        isTotalOrder : IsTotalOrder _≈_ _≤_

      open IsTotalOrder isTotalOrder public
        using (total; isPartialOrder; isTotalPreorder)

      poset : Poset c ℓ₁ ℓ₂
      poset = record
        { isPartialOrder = isPartialOrder
        }

      open Poset poset public
        hiding (Carrier; _≈_; _≤_; isPartialOrder)

      totalPreorder : TotalPreorder c ℓ₁ ℓ₂
      totalPreorder = record
        { isTotalPreorder = isTotalPreorder
        }

    record DecTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
      infix 4 _≈_ _≤_
      field
        Carrier         : Set c
        _≈_             : Rel Carrier ℓ₁
        _≤_             : Rel Carrier ℓ₂
        isDecTotalOrder : IsDecTotalOrder _≈_ _≤_

      private module DTO = IsDecTotalOrder isDecTotalOrder

      open DTO public
        using (_≟_; _≤?_; isTotalOrder; isDecPartialOrder)

      totalOrder : TotalOrder c ℓ₁ ℓ₂
      totalOrder = record
        { isTotalOrder = isTotalOrder
        }

      open TotalOrder totalOrder public
        hiding (Carrier; _≈_; _≤_; isTotalOrder; module Eq)

      decPoset : DecPoset c ℓ₁ ℓ₂
      decPoset = record
        { isDecPartialOrder = isDecPartialOrder
        }

      open DecPoset decPoset public
        using (module Eq)

    -- Note that these orders are decidable. The current implementation
    -- of `Trichotomous` subsumes irreflexivity and asymmetry. Any reasonable
    -- definition capturing these three properties implies decidability
    -- as `Trichotomous` necessarily separates out the equality case.

    record StrictTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
      infix 4 _≈_ _<_
      field
        Carrier            : Set c
        _≈_                : Rel Carrier ℓ₁
        _<_                : Rel Carrier ℓ₂
        isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_

      open IsStrictTotalOrder isStrictTotalOrder public
        using
        ( _≟_; _<?_; compare; isStrictPartialOrder
        ; isDecStrictPartialOrder; isDecEquivalence
        )

      strictPartialOrder : StrictPartialOrder c ℓ₁ ℓ₂
      strictPartialOrder = record
        { isStrictPartialOrder = isStrictPartialOrder
        }

      open StrictPartialOrder strictPartialOrder public
        hiding (Carrier; _≈_; _<_; isStrictPartialOrder; module Eq)

      decStrictPartialOrder : DecStrictPartialOrder c ℓ₁ ℓ₂
      decStrictPartialOrder = record
        { isDecStrictPartialOrder = isDecStrictPartialOrder
        }

      open DecStrictPartialOrder decStrictPartialOrder public
        using (module Eq)

      decSetoid : DecSetoid c ℓ₁
      decSetoid = record
        { isDecEquivalence = Eq.isDecEquivalence
        }
      {-# WARNING_ON_USAGE decSetoid
      "Warning: decSetoid was deprecated in v1.3.
      Please use Eq.decSetoid instead."
      #-}

    record DenseLinearOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
      infix 4 _≈_ _<_
      field
        Carrier            : Set c
        _≈_                : Rel Carrier ℓ₁
        _<_                : Rel Carrier ℓ₂
        isDenseLinearOrder : IsDenseLinearOrder _≈_ _<_

      open IsDenseLinearOrder isDenseLinearOrder public
        using (isStrictTotalOrder; dense)

      strictTotalOrder : StrictTotalOrder c ℓ₁ ℓ₂
      strictTotalOrder = record
        { isStrictTotalOrder = isStrictTotalOrder
        }

      open StrictTotalOrder strictTotalOrder public
        hiding (Carrier; _≈_; _<_; isStrictTotalOrder)

    ------------------------------------------------------------------------
    -- Apartness relations
    ------------------------------------------------------------------------

    record ApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
      infix 4 _≈_ _#_
      field
        Carrier             : Set c
        _≈_                 : Rel Carrier ℓ₁
        _#_                 : Rel Carrier ℓ₂
        isApartnessRelation : IsApartnessRelation _≈_ _#_

      open IsApartnessRelation isApartnessRelation public
        hiding (_¬#_)

      rawRelation : RawRelation _ _ _
      rawRelation = record { _≈_ = _≈_ ; _∼_ = _#_ }

      open RawRelation rawRelation public
        renaming (_≁_ to _¬#_; _∼ᵒ_ to _#ᵒ_; _≁ᵒ_ to _¬#ᵒ_)
        hiding (Carrier; _≈_ ; _∼_)