------------------------------------------------------------------------
-- 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  _≈_
  field
    Carrier              : Set a
    _≈_                  : Rel Carrier ℓ

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


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

record RawRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix  _≈_ _∼_
  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  _≁_
  _≁_ : Rel Carrier _
  x ≁ y = ¬ (x ∼ y)

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

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