← Back to branch summary

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

« back to all changes in this revision

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

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 09:46:46 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805094646-zqd0c4m8ndngqg6x
Tags: 0.8-1
* [4ca6fd0] Update debian/watch to fetch tarballs from github
* [84d4313] Imported Upstream version 0.8
* [7b08243] debian/control: Require agda 2.4.x per upstream
* [37e7e10] debian/control: Standards-Version → 3.9.5, no changes required.
* [9051b9d] Run upstream's "GenerateEverything" script

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Relation/Binary/HeterogeneousEquality.agda
9
9
open import Data.Product
10
10
open import Function
11
11
open import Function.Inverse using (Inverse)
 
12
open import Data.Unit.Core
12
13
open import Level
13
14
open import Relation.Nullary
14
15
open import Relation.Binary
27
28
 
28
29
-- Nonequality.
29
30
 
30
 
_≇_ : ∀ {a} {A : Set a} → A → ∀ {b} {B : Set b} → B → Set
 
31
_≇_ : ∀ {ℓ} {A : Set ℓ} → A → {B : Set ℓ} → B → Set ℓ
31
32
x ≇ y = ¬ x ≅ y
32
33
 
33
34
------------------------------------------------------------------------
44
45
reflexive : ∀ {a} {A : Set a} → _⇒_ {A = A} _≡_ (λ x y → x ≅ y)
45
46
reflexive refl = refl
46
47
 
47
 
sym : ∀ {a b} {A : Set a} {B : Set b} {x : A} {y : B} → x ≅ y → y ≅ x
 
48
sym : ∀ {ℓ} {A B : Set ℓ} {x : A} {y : B} → x ≅ y → y ≅ x
48
49
sym refl = refl
49
50
 
50
 
trans : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
51
 
          {x : A} {y : B} {z : C} →
 
51
trans : ∀ {ℓ} {A B C : Set ℓ} {x : A} {y : B} {z : C} →
52
52
        x ≅ y → y ≅ z → x ≅ z
53
53
trans refl eq = eq
54
54
 
73
73
       (f : (x : A) → B x) → x ≅ y → f x ≅ f y
74
74
cong f refl = refl
75
75
 
 
76
cong-app : ∀ {a b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
 
77
           f ≅ g → (x : A) → f x ≅ g x
 
78
cong-app refl x = refl
 
79
 
76
80
cong₂ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : ∀ x → B x → Set c}
77
81
          {x y u v}
78
82
        (f : (x : A) (y : B x) → C x y) → x ≅ y → u ≅ v → f x u ≅ f y v
81
85
resp₂ : ∀ {a ℓ} {A : Set a} (∼ : Rel A ℓ) → ∼ Respects₂ (λ x y → x ≅ y)
82
86
resp₂ _∼_ = subst⟶resp₂ _∼_ subst
83
87
 
84
 
proof-irrelevance : ∀ {a b} {A : Set a} {B : Set b} {x : A} {y : B}
 
88
proof-irrelevance : ∀ {ℓ} {A B : Set ℓ} {x : A} {y : B}
85
89
                    (p q : x ≅ y) → p ≡ q
86
90
proof-irrelevance refl refl = refl
87
91
 
170
174
  infixr 2 _≅⟨_⟩_ _≡⟨_⟩_ _≡⟨⟩_
171
175
  infix  1 begin_
172
176
 
173
 
  data _IsRelatedTo_ {a} {A : Set a} (x : A) {b} {B : Set b} (y : B) :
174
 
                     Set where
 
177
  data _IsRelatedTo_ {ℓ} {A : Set ℓ} (x : A) {B : Set ℓ} (y : B) :
 
178
                     Set ℓ where
175
179
    relTo : (x≅y : x ≅ y) → x IsRelatedTo y
176
180
 
177
 
  begin_ : ∀ {a} {A : Set a} {x : A} {b} {B : Set b} {y : B} →
 
181
  begin_ : ∀ {ℓ} {A : Set ℓ} {x : A} {B} {y : B} →
178
182
           x IsRelatedTo y → x ≅ y
179
183
  begin relTo x≅y = x≅y
180
184
 
181
 
  _≅⟨_⟩_ : ∀ {a} {A : Set a} (x : A) {b} {B : Set b} {y : B}
182
 
             {c} {C : Set c} {z : C} →
 
185
  _≅⟨_⟩_ : ∀ {ℓ} {A : Set ℓ} (x : A) {B} {y : B} {C} {z : C} →
183
186
           x ≅ y → y IsRelatedTo z → x IsRelatedTo z
184
187
  _ ≅⟨ x≅y ⟩ relTo y≅z = relTo (trans x≅y y≅z)
185
188
 
186
 
  _≡⟨_⟩_ : ∀ {a} {A : Set a} (x : A) {y c} {C : Set c} {z : C} →
 
189
  _≡⟨_⟩_ : ∀ {ℓ} {A : Set ℓ} (x : A) {y C} {z : C} →
187
190
           x ≡ y → y IsRelatedTo z → x IsRelatedTo z
188
191
  _ ≡⟨ x≡y ⟩ relTo y≅z = relTo (trans (reflexive x≡y) y≅z)
189
192
 
190
 
  _≡⟨⟩_ : ∀ {a} {A : Set a} (x : A) {b} {B : Set b} {y : B} →
 
193
  _≡⟨⟩_ : ∀ {ℓ} {A : Set ℓ} (x : A) {B} {y : B} →
191
194
          x IsRelatedTo y → x IsRelatedTo y
192
195
  _ ≡⟨⟩ x≅y = x≅y
193
196
 
215
218
  where
216
219
  ext′ : P.Extensionality ℓ₁ ℓ₂
217
220
  ext′ = P.extensionality-for-lower-levels ℓ₁ (suc ℓ₂) ext
 
221
 
 
222
 
 
223
------------------------------------------------------------------------
 
224
-- Inspect on steroids
 
225
 
 
226
-- Inspect on steroids can be used when you want to pattern match on
 
227
-- the result r of some expression e, and you also need to "remember"
 
228
-- that r ≡ e.
 
229
 
 
230
data Reveal_is_ {a} {A : Set a} (x : Hidden A) (y : A) : Set a where
 
231
  [_] : (eq : reveal x ≅ y) → Reveal x is y
 
232
 
 
233
inspect : ∀ {a b} {A : Set a} {B : A → Set b}
 
234
          (f : (x : A) → B x) (x : A) → Reveal (hide f x) is (f x)
 
235
inspect f x = [ refl ]