← Back to branch summary

~ubuntu-branches/ubuntu/precise/agda-stdlib/precise

« back to all changes in this revision

Viewing changes to src/Relation/Binary/HeterogeneousEquality/Core.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2011-11-29 17:00:35 UTC
  • mfrom: (2.1.4 sid)
  • Revision ID: package-import@ubuntu.com-20111129170035-be8cbok8ojft5tjl
Tags: 0.6~darcs20111129t1640-1
* [ef445ab] Imported Upstream version 0.6~darcs20111129t1640
  + Darcs snapshot required for Agda 2.3.0 compatibility
* [f801f83] Update BDs and deps to require Agda 2.3.0
* [c52be90] Use 3.0 (quilt) for bz2 orig

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Relation/Binary/HeterogeneousEquality/Core.agda
 
1
------------------------------------------------------------------------
 
2
-- The Agda standard library
 
3
--
 
4
-- Heterogeneous equality
 
5
------------------------------------------------------------------------
 
6
 
 
7
-- This file contains some core definitions which are reexported by
 
8
-- Relation.Binary.HeterogeneousEquality.
 
9
 
 
10
module Relation.Binary.HeterogeneousEquality.Core where
 
11
 
 
12
open import Relation.Binary.Core using (_≡_; refl)
 
13
 
 
14
------------------------------------------------------------------------
 
15
-- Heterogeneous equality
 
16
 
 
17
infix 4 _≅_
 
18
 
 
19
data _≅_ {a} {A : Set a} (x : A) : ∀ {b} {B : Set b} → B → Set where
 
20
  refl : x ≅ x
 
21
 
 
22
------------------------------------------------------------------------
 
23
-- Conversion
 
24
 
 
25
≅-to-≡ : ∀ {a} {A : Set a} {x y : A} → x ≅ y → x ≡ y
 
26
≅-to-≡ refl = refl