------------------------------------------------------------------------
-- The Agda standard library
--
-- Additional properties for setoids
------------------------------------------------------------------------

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

open import Relation.Binary.Bundles using (PartialSetoid)

module Relation.Binary.Properties.PartialSetoid
  {a ℓ} (S : PartialSetoid a ℓ) where

open import Data.Product.Base using (_,_; _×_)
open import Relation.Binary.Definitions using (LeftTrans; RightTrans)
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)

open PartialSetoid S

private
  variable
    x y z : Carrier

------------------------------------------------------------------------
-- Proofs for partial equivalence relations

trans-reflˡ : LeftTrans _≡_ _≈_
trans-reflˡ ≡.refl p = p

trans-reflʳ : RightTrans _≈_ _≡_
trans-reflʳ p ≡.refl = p

partial-reflˡ : x ≈ y → x ≈ x
partial-reflˡ p = trans p (sym p)

partial-reflʳ : x ≈ y → y ≈ y
partial-reflʳ p = trans (sym p) p

partial-refl : x ≈ y → x ≈ x × y ≈ y
partial-refl p = partial-reflˡ p , partial-reflʳ p

partial-reflexiveˡ : x ≈ y → x ≡ z → x ≈ z
partial-reflexiveˡ p ≡.refl = partial-reflˡ p

partial-reflexiveʳ : x ≈ y → y ≡ z → y ≈ z
partial-reflexiveʳ p ≡.refl = partial-reflʳ p