    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Raw bundles for homogeneous binary relations
    ------------------------------------------------------------------------

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

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

    module Relation.Binary.Bundles.Raw where

    open import Function.Base using (flip)
    open import Level using (Level; suc; _⊔_)
    open import Relation.Binary.Core using (Rel)
    open import Relation.Nullary.Negation.Core using (¬_)

    ------------------------------------------------------------------------
    -- RawSetoid
    ------------------------------------------------------------------------

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

      infix 4 _≉_
      _≉_ : Rel Carrier _
      x ≉ y = ¬ (x ≈ y)

    ------------------------------------------------------------------------
    -- RawRelation: basis for Relation.Binary.Bundles.*Order
    ------------------------------------------------------------------------

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

      rawSetoid : RawSetoid c ℓ₁
      rawSetoid = record { _≈_ = _≈_ }

      open RawSetoid rawSetoid public
        using (_≉_)

      infix 4 _≁_
      _≁_ : Rel Carrier _
      x ≁ y = ¬ (x ∼ y)

      infix 4 _∼ᵒ_
      _∼ᵒ_ = flip _∼_

      infix 4 _≁ᵒ_
      _≁ᵒ_ = flip _≁_