------------------------------------------------------------------------
-- The Agda standard library
--
-- Heterogeneous equality
------------------------------------------------------------------------

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

{-# OPTIONS --with-K --safe #-}

module Relation.Binary.HeterogeneousEquality.Core where

open import Level using (Level)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

private
  variable
    a b : Level
    A : Set a

------------------------------------------------------------------------
-- Heterogeneous equality

infix  _≅_

data _≅_ {A : Set a} (x : A) : {B : Set b} → B → Set a where
   refl : x ≅ x

------------------------------------------------------------------------
-- Conversion

≅-to-≡ : ∀ {x y : A} → x ≅ y → x ≡ y
≅-to-≡ refl = refl

≡-to-≅ : ∀ {x y : A} → x ≡ y → x ≅ y
≡-to-≅ refl = refl