------------------------------------------------------------------------
-- 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 4 _≅_
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
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4