← Back to branch summary

~ubuntu-branches/ubuntu/saucy/agda-stdlib/saucy-proposed

« back to all changes in this revision

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

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2010-01-08 23:35:09 UTC
  • Revision ID: james.westby@ubuntu.com-20100108233509-l6ejt9xji64xysfb
Tags: upstream-0.3
Import upstream version 0.3

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Relation/Binary/PropositionalEquality/Core.agda
 
1
------------------------------------------------------------------------
 
2
-- Propositional equality
 
3
------------------------------------------------------------------------
 
4
 
 
5
{-# OPTIONS --universe-polymorphism #-}
 
6
 
 
7
-- This file contains some core definitions which are reexported by
 
8
-- Relation.Binary.PropositionalEquality.
 
9
 
 
10
module Relation.Binary.PropositionalEquality.Core where
 
11
 
 
12
open import Level
 
13
open import Relation.Binary.Core
 
14
open import Relation.Binary.Consequences.Core
 
15
 
 
16
------------------------------------------------------------------------
 
17
-- Some properties
 
18
 
 
19
sym : ∀ {a} {A : Set a} → Symmetric (_≡_ {A = A})
 
20
sym refl = refl
 
21
 
 
22
trans : ∀ {a} {A : Set a} → Transitive (_≡_ {A = A})
 
23
trans refl refl = refl
 
24
 
 
25
subst : ∀ {a p} {A : Set a} → Substitutive (_≡_ {A = A}) p
 
26
subst P refl p = p
 
27
 
 
28
resp₂ : ∀ {a ℓ} {A : Set a} (∼ : Rel A ℓ) → ∼ Respects₂ _≡_
 
29
resp₂ _∼_ = subst⟶resp₂ _∼_ subst
 
30
 
 
31
isEquivalence : ∀ {a} {A : Set a} → IsEquivalence (_≡_ {A = A})
 
32
isEquivalence = record
 
33
  { refl  = refl
 
34
  ; sym   = sym
 
35
  ; trans = trans
 
36
  }