------------------------------------------------------------------------
-- Indexed binary relations
------------------------------------------------------------------------

{-# OPTIONS --universe-polymorphism #-}

-- This file contains some core definitions which are reexported by
-- Relation.Binary.Indexed.

module Relation.Binary.Indexed.Core where

open import Function
open import Level
import Relation.Binary.Core as B
import Relation.Binary.Core as P

------------------------------------------------------------------------
-- Indexed binary relations

-- Heterogeneous.

REL :  {i₁ i₂ a₁ a₂} {I₁ : Set i₁} {I₂ : Set i₂} 
      (I₁  Set a₁)  (I₂  Set a₂)  ( : Level)  Set _
REL A₁ A₂  =  {i₁ i₂}  A₁ i₁  A₂ i₂  Set 

-- Homogeneous.

Rel :  {i a} {I : Set i}  (I  Set a)  ( : Level)  Set _
Rel A  = REL A A 

------------------------------------------------------------------------
-- Simple properties of indexed binary relations

-- Reflexivity.

Reflexive :  {i a } {I : Set i} (A : I  Set a)  Rel A   Set _
Reflexive _ _∼_ =  {i}  B.Reflexive (_∼_ {i})

-- Symmetry.

Symmetric :  {i a } {I : Set i} (A : I  Set a)  Rel A   Set _
Symmetric _ _∼_ =  {i j}  B.Sym (_∼_ {i} {j}) _∼_

-- Transitivity.

Transitive :  {i a } {I : Set i} (A : I  Set a)  Rel A   Set _
Transitive _ _∼_ =  {i j k}  B.Trans _∼_ (_∼_ {j}) (_∼_ {i} {k})

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

record IsEquivalence {i a } {I : Set i} (A : I  Set a)
                     (_≈_ : Rel A ) : Set (i  a  ) where
  field
    refl  : Reflexive A _≈_
    sym   : Symmetric A _≈_
    trans : Transitive A _≈_

  reflexive :  {i}  P._≡_  B._⇒_  _≈_ {i}
  reflexive P.refl = refl

record Setoid {i} (I : Set i) c  : Set (suc (i  c  )) where
  infix 4 _≈_
  field
    Carrier       : I  Set c
    _≈_           : Rel Carrier 
    isEquivalence : IsEquivalence Carrier _≈_

  open IsEquivalence isEquivalence public