← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda-stdlib/raring

« back to all changes in this revision

Viewing changes to src/Data/Function/Equality.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2011-02-25 22:28:40 UTC
  • mfrom: (1.1.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20110225222840-jt16gl302kca7h0g
Tags: 0.5-1~ubuntu1
https://launchpad.net/bugs/725364
http://bugs.debian.org/573807
http://bugs.debian.org/598708

* Upload to Ubuntu from Debian's VCS due to delays in unstable caused by
  the GHC 7 transition (LP: #725364)
* [ba20206] Make package architecture independent (Closes: #573807, #598708,
  #599958)
* [0fb0600] Standards-Version → 3.9.1, no changes required
* [d3f13b8] Update required Agda version to 2.2.8
* [cc1f5c8] Imported Upstream version 0.4
* [2c82171] Add watch file
* [9251e0b] Imported Upstream version 0.5
* [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

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Function/Equality.agda
1
 
------------------------------------------------------------------------
2
 
------------------------------------------------------------------------
3
 
 
4
 
{-# OPTIONS --universe-polymorphism #-}
5
 
 
6
 
module Data.Function.Equality where
7
 
 
8
 
open import Data.Function as Fun using (_on_)
9
 
open import Level
10
 
open import Relation.Binary
11
 
 
12
 
------------------------------------------------------------------------
13
 
 
14
 
infixr 0 _⟶_
15
 
 
16
 
record _⟶_ {f₁ f₂ t₁ t₂} (From : Setoid f₁ f₂) (To : Setoid t₁ t₂) :
17
 
           Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
18
 
  open Setoid
19
 
  infixl 5 _⟨$⟩_
20
 
  field
21
 
    _⟨$⟩_ : Carrier From → Carrier To
22
 
    cong  : _⟨$⟩_ Preserves _≈_ From ⟶ _≈_ To
23
 
 
24
 
open _⟶_ public
25
 
 
26
 
id : ∀ {a₁ a₂} {A : Setoid a₁ a₂} → A ⟶ A
27
 
id = record { _⟨$⟩_ = Fun.id; cong = Fun.id }
28
 
 
29
 
infixr 9 _∘_
30
 
 
31
 
_∘_ : ∀ {a₁ a₂} {A : Setoid a₁ a₂}
32
 
        {b₁ b₂} {B : Setoid b₁ b₂}
33
 
        {c₁ c₂} {C : Setoid c₁ c₂} →
34
 
      B ⟶ C → A ⟶ B → A ⟶ C
35
 
f ∘ g = record
36
 
  { _⟨$⟩_ = Fun._∘_ (_⟨$⟩_ f) (_⟨$⟩_ g)
37
 
  ; cong  = Fun._∘_ (cong  f) (cong  g)
38
 
  }
39
 
 
40
 
const : ∀ {a₁ a₂} {A : Setoid a₁ a₂}
41
 
          {b₁ b₂} {B : Setoid b₁ b₂} →
42
 
        Setoid.Carrier B → A ⟶ B
43
 
const {B = B} b = record
44
 
  { _⟨$⟩_ = Fun.const b
45
 
  ; cong  = Fun.const (Setoid.refl B)
46
 
  }
47
 
 
48
 
------------------------------------------------------------------------
49
 
 
50
 
infixr 0 _↝_
51
 
 
52
 
_↝_ : ∀ {a b c d ℓ₁ ℓ₂}
53
 
        {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
54
 
      (∼₁ : REL A B ℓ₁) (∼₂ : REL C D ℓ₂) → REL (A → C) (B → D) _
55
 
_∼₁_ ↝ _∼₂_ = λ f g → ∀ {x y} → x ∼₁ y → f x ∼₂ g y
56
 
 
57
 
↝-isEquivalence : ∀ {a b c ℓ₁ ℓ₂} {A : Set a} {B : Set b} {C : Set c}
58
 
                    {∼₁ : Rel A ℓ₁} {∼₂ : Rel B ℓ₂}
59
 
                  (fun : C → (A → B)) →
60
 
                  (∀ f → fun f Preserves ∼₁ ⟶ ∼₂) →
61
 
                  IsEquivalence ∼₁ → IsEquivalence ∼₂ →
62
 
                  IsEquivalence ((∼₁ ↝ ∼₂) on fun)
63
 
↝-isEquivalence _ cong eq₁ eq₂ = record
64
 
  { refl  = λ {f} x∼₁y → cong f x∼₁y
65
 
  ; sym   = λ f∼g x∼y → sym eq₂ (f∼g (sym eq₁ x∼y))
66
 
  ; trans = λ f∼g g∼h x∼y → trans eq₂ (f∼g (refl eq₁)) (g∼h x∼y)
67
 
  } where open IsEquivalence
68
 
 
69
 
 
70
 
≡↝ : ∀ {a b c ℓ} {A : Set a} {B : A → Set b} {C : A → Set c} →
71
 
     (∀ x → REL (B x) (C x) ℓ) →
72
 
     REL ((x : A) → B x) ((x : A) → C x) _
73
 
≡↝ R = λ f g → ∀ x → R x (f x) (g x)
74
 
 
75
 
≡↝-isEquivalence :
76
 
  ∀ {a b ℓ} {A : Set a} {B : A → Set b} {R : ∀ x → Rel (B x) ℓ} →
77
 
  (∀ x → IsEquivalence (R x)) → IsEquivalence (≡↝ R)
78
 
≡↝-isEquivalence eq = record
79
 
  { refl  = λ _ → refl
80
 
  ; sym   = λ f∼g x → sym (f∼g x)
81
 
  ; trans = λ f∼g g∼h x → trans (f∼g x) (g∼h x)
82
 
  } where open module Eq {x} = IsEquivalence (eq x)
83
 
 
84
 
------------------------------------------------------------------------
85
 
 
86
 
infixr 0 _⇨_ _≡⇨_
87
 
 
88
 
_⇨_ : ∀ {f₁ f₂ t₁ t₂} → Setoid f₁ f₂ → Setoid t₁ t₂ → Setoid _ _
89
 
S₁ ⇨ S₂ = record
90
 
  { Carrier       = S₁ ⟶ S₂
91
 
  ; _≈_           = (_≈_ S₁ ↝ _≈_ S₂) on _⟨$⟩_
92
 
  ; isEquivalence =
93
 
      ↝-isEquivalence (_⟨$⟩_ {From = S₁} {To = S₂})
94
 
                      cong (isEquivalence S₁) (isEquivalence S₂)
95
 
  } where open Setoid; open _⟶_
96
 
 
97
 
_≡⇨_ : ∀ {a s₁ s₂} (A : Set a) → (A → Setoid s₁ s₂) → Setoid _ _
98
 
A ≡⇨ S = record
99
 
  { Carrier       = (x : A) → Carrier (S x)
100
 
  ; _≈_           = ≡↝ (λ x → _≈_ (S x))
101
 
  ; isEquivalence = ≡↝-isEquivalence (λ x → isEquivalence (S x))
102
 
  } where open Setoid