← Back to branch summary

~ubuntu-branches/ubuntu/utopic/agda-stdlib/utopic

« back to all changes in this revision

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

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2011-05-24 10:26:15 UTC
  • mfrom: (1.1.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20110524102615-9tontf43bq9ym690
Tags: 0.5-1
http://bugs.debian.org/573807
http://bugs.debian.org/598708
* [9251e0b] Imported Upstream version 0.5
* [ba20206] Make package architecture independent (Closes: #573807, #598708,
  #599958)
* [2c82171] Add watch file
* [0518fa6] No longer need procps | hurd BD as we no longer have the ticker
* [daf2445] Don't use upstream's make install — handled ourselves by
  dh_install
* [1b86533] Update watchfile to point at new location
* [637f47d] Remove debian/gbp.conf as we are no longer building for exp
* [cc88671] Require Agda 2.2.10
* [e99dab5] Set maximum stack size to 1G to prevent overflows in the build
* [251cd1d] Run the test suite manually
* [a7db697] Set the variable in the emacs loading script properly
* [540ca3f] Improve short description
* [6b3e794] Add dependencies on compatible versions of the Agda library
* [7127678] Standards-Version bump to 3.9.2, no changes required
* [9d0ae30] Update to use ghc instead of ghc6
* [3f6879a] Set Maintainer to my d.o email address

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Relation/Binary/HeterogeneousEquality.agda
6
6
 
7
7
module Relation.Binary.HeterogeneousEquality where
8
8
 
9
 
open import Data.Function
10
9
open import Data.Product
 
10
open import Function
 
11
open import Function.Inverse using (Inverse)
11
12
open import Level
12
13
open import Relation.Nullary
13
14
open import Relation.Binary
14
15
open import Relation.Binary.Consequences
 
16
open import Relation.Binary.Indexed as I using (_at_)
15
17
open import Relation.Binary.PropositionalEquality as PropEq
16
18
  using (_≡_; refl)
17
19
 
99
101
  ; isEquivalence = isEquivalence
100
102
  }
101
103
 
 
104
indexedSetoid : ∀ {a b} {A : Set a} → (A → Set b) → I.Setoid A _ _
 
105
indexedSetoid B = record
 
106
  { Carrier       = B
 
107
  ; _≈_           = λ x y → x ≅ y
 
108
  ; isEquivalence = record
 
109
    { refl  = refl
 
110
    ; sym   = sym
 
111
    ; trans = trans
 
112
    }
 
113
  }
 
114
 
 
115
≡⇿≅ : ∀ {a b} {A : Set a} (B : A → Set b) {x : A} →
 
116
      Inverse (PropEq.setoid (B x)) (indexedSetoid B at x)
 
117
≡⇿≅ B = record
 
118
  { to         = record { _⟨$⟩_ = id; cong = ≡-to-≅ }
 
119
  ; from       = record { _⟨$⟩_ = id; cong = ≅-to-≡ }
 
120
  ; inverse-of = record
 
121
    { left-inverse-of  = λ _ → refl
 
122
    ; right-inverse-of = λ _ → refl
 
123
    }
 
124
  }
 
125
 
102
126
decSetoid : ∀ {a} {A : Set a} →
103
127
            Decidable {A = A} {B = A} (λ x y → x ≅ y) →
104
128
            DecSetoid _ _
116
140
  { isEquivalence = isEquivalence
117
141
  ; reflexive     = id
118
142
  ; trans         = trans
119
 
  ; ∼-resp-≈      = resp₂ (λ x y → x ≅ y)
120
143
  }
121
144
 
122
145
isPreorder-≡ : ∀ {a} {A : Set a} →
125
148
  { isEquivalence = PropEq.isEquivalence
126
149
  ; reflexive     = reflexive
127
150
  ; trans         = trans
128
 
  ; ∼-resp-≈      = PropEq.resp₂ (λ x y → x ≅ y)
129
151
  }
130
152
 
131
153
preorder : ∀ {a} → Set a → Preorder _ _ _