------------------------------------------------------------------------
-- 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 _≁_