------------------------------------------------------------------------
-- Propositional equality
------------------------------------------------------------------------

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

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

module Relation.Binary.PropositionalEquality.Core where

open import Level
open import Relation.Binary.Core
open import Relation.Binary.Consequences.Core

------------------------------------------------------------------------
-- Some properties

sym :  {a} {A : Set a}  Symmetric (_≡_ {A = A})
sym refl = refl

trans :  {a} {A : Set a}  Transitive (_≡_ {A = A})
trans refl refl = refl

subst :  {a p} {A : Set a}  Substitutive (_≡_ {A = A}) p
subst P refl p = p

resp₂ :  {a } {A : Set a} ( : Rel A )   Respects₂ _≡_
resp₂ _∼_ = subst⟶resp₂ _∼_ subst

isEquivalence :  {a} {A : Set a}  IsEquivalence (_≡_ {A = A})
isEquivalence = record
  { refl  = refl
  ; sym   = sym
  ; trans = trans
  }