← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Function/Equivalence.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/Function/Equivalence.agda
 
1
------------------------------------------------------------------------
 
2
-- Equivalence (coinhabitance)
 
3
------------------------------------------------------------------------
 
4
 
 
5
{-# OPTIONS --universe-polymorphism #-}
 
6
 
 
7
module Function.Equivalence where
 
8
 
 
9
open import Function using (flip)
 
10
open import Function.Equality as F
 
11
  using (_⟶_; _⟨$⟩_) renaming (_∘_ to _⟪∘⟫_)
 
12
open import Level
 
13
open import Relation.Binary
 
14
import Relation.Binary.PropositionalEquality as P
 
15
 
 
16
-- Setoid equivalence.
 
17
 
 
18
record Equivalent {f₁ f₂ t₁ t₂}
 
19
                  (From : Setoid f₁ f₂) (To : Setoid t₁ t₂) :
 
20
                  Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
 
21
  field
 
22
    to   : From ⟶ To
 
23
    from : To ⟶ From
 
24
 
 
25
-- Set equivalence.
 
26
 
 
27
infix 3 _⇔_
 
28
 
 
29
_⇔_ : ∀ {f t} → Set f → Set t → Set _
 
30
From ⇔ To = Equivalent (P.setoid From) (P.setoid To)
 
31
 
 
32
equivalent : ∀ {f t} {From : Set f} {To : Set t} →
 
33
             (From → To) → (To → From) → From ⇔ To
 
34
equivalent to from = record { to = P.→-to-⟶ to; from = P.→-to-⟶ from }
 
35
 
 
36
------------------------------------------------------------------------
 
37
-- Map and zip
 
38
 
 
39
map : ∀ {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂}
 
40
        {f₁′ f₂′ t₁′ t₂′}
 
41
        {From′ : Setoid f₁′ f₂′} {To′ : Setoid t₁′ t₂′} →
 
42
      ((From ⟶ To) → (From′ ⟶ To′)) →
 
43
      ((To ⟶ From) → (To′ ⟶ From′)) →
 
44
      Equivalent From To → Equivalent From′ To′
 
45
map t f eq = record { to = t to; from = f from }
 
46
  where open Equivalent eq
 
47
 
 
48
zip : ∀ {f₁₁ f₂₁ t₁₁ t₂₁}
 
49
        {From₁ : Setoid f₁₁ f₂₁} {To₁ : Setoid t₁₁ t₂₁}
 
50
        {f₁₂ f₂₂ t₁₂ t₂₂}
 
51
        {From₂ : Setoid f₁₂ f₂₂} {To₂ : Setoid t₁₂ t₂₂}
 
52
        {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂} →
 
53
      ((From₁ ⟶ To₁) → (From₂ ⟶ To₂) → (From ⟶ To)) →
 
54
      ((To₁ ⟶ From₁) → (To₂ ⟶ From₂) → (To ⟶ From)) →
 
55
      Equivalent From₁ To₁ → Equivalent From₂ To₂ → Equivalent From To
 
56
zip t f eq₁ eq₂ =
 
57
  record { to = t (to eq₁) (to eq₂); from = f (from eq₁) (from eq₂) }
 
58
  where open Equivalent
 
59
 
 
60
------------------------------------------------------------------------
 
61
-- Equivalent is an equivalence relation
 
62
 
 
63
-- Identity and composition (reflexivity and transitivity).
 
64
 
 
65
id : ∀ {s₁ s₂} → Reflexive (Equivalent {s₁} {s₂})
 
66
id {x = S} = record
 
67
  { to   = F.id
 
68
  ; from = F.id
 
69
  }
 
70
 
 
71
infixr 9 _∘_
 
72
 
 
73
_∘_ : ∀ {f₁ f₂ m₁ m₂ t₁ t₂} →
 
74
      TransFlip (Equivalent {f₁} {f₂} {m₁} {m₂})
 
75
                (Equivalent {m₁} {m₂} {t₁} {t₂})
 
76
                (Equivalent {f₁} {f₂} {t₁} {t₂})
 
77
f ∘ g = record
 
78
  { to   = to   f ⟪∘⟫ to   g
 
79
  ; from = from g ⟪∘⟫ from f
 
80
  } where open Equivalent
 
81
 
 
82
-- Symmetry.
 
83
 
 
84
sym : ∀ {f₁ f₂ t₁ t₂} →
 
85
      Sym (Equivalent {f₁} {f₂} {t₁} {t₂}) (Equivalent {t₁} {t₂} {f₁} {f₂})
 
86
sym eq = record
 
87
  { from       = to
 
88
  ; to         = from
 
89
  } where open Equivalent eq
 
90
 
 
91
-- For fixed universe levels we can construct setoids.
 
92
 
 
93
setoid : (s₁ s₂ : Level) → Setoid (suc (s₁ ⊔ s₂)) (s₁ ⊔ s₂)
 
94
setoid s₁ s₂ = record
 
95
  { Carrier       = Setoid s₁ s₂
 
96
  ; _≈_           = Equivalent
 
97
  ; isEquivalence = record {refl = id; sym = sym; trans = flip _∘_}
 
98
  }
 
99
 
 
100
⇔-setoid : (ℓ : Level) → Setoid (suc ℓ) ℓ
 
101
⇔-setoid ℓ = record
 
102
  { Carrier       = Set ℓ
 
103
  ; _≈_           = _⇔_
 
104
  ; isEquivalence = record {refl = id; sym = sym; trans = flip _∘_}
 
105
  }