← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Function/Bijection.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/Bijection.agda
 
1
------------------------------------------------------------------------
 
2
-- Bijections
 
3
------------------------------------------------------------------------
 
4
 
 
5
{-# OPTIONS --universe-polymorphism #-}
 
6
 
 
7
module Function.Bijection where
 
8
 
 
9
open import Data.Product
 
10
open import Level
 
11
open import Relation.Binary
 
12
open import Function.Equality as F
 
13
  using (_⟶_; _⟨$⟩_) renaming (_∘_ to _⟪∘⟫_)
 
14
open import Function.Injection   as Inj  hiding (id; _∘_)
 
15
open import Function.Surjection  as Surj hiding (id; _∘_)
 
16
open import Function.LeftInverse as Left hiding (id; _∘_)
 
17
 
 
18
-- Bijective functions.
 
19
 
 
20
record Bijective {f₁ f₂ t₁ t₂}
 
21
                 {From : Setoid f₁ f₂} {To : Setoid t₁ t₂}
 
22
                 (to : From ⟶ To) :
 
23
                 Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
 
24
  field
 
25
    injective  : Injective  to
 
26
    surjective : Surjective to
 
27
 
 
28
  open Surjective surjective public
 
29
 
 
30
  left-inverse-of : from LeftInverseOf to
 
31
  left-inverse-of x = injective (right-inverse-of (to ⟨$⟩ x))
 
32
 
 
33
-- The set of all bijections between two setoids.
 
34
 
 
35
record Bijection {f₁ f₂ t₁ t₂}
 
36
                 (From : Setoid f₁ f₂) (To : Setoid t₁ t₂) :
 
37
                 Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
 
38
  field
 
39
    to        : From ⟶ To
 
40
    bijective : Bijective to
 
41
 
 
42
  open Bijective bijective public
 
43
 
 
44
  injection : Injection From To
 
45
  injection = record
 
46
    { to        = to
 
47
    ; injective = injective
 
48
    }
 
49
 
 
50
  surjection : Surjection From To
 
51
  surjection = record
 
52
    { to         = to
 
53
    ; surjective = surjective
 
54
    }
 
55
 
 
56
  open Surjection surjection public using (equivalent; right-inverse)
 
57
 
 
58
  left-inverse : LeftInverse From To
 
59
  left-inverse = record
 
60
    { to              = to
 
61
    ; from            = from
 
62
    ; left-inverse-of = left-inverse-of
 
63
    }
 
64
 
 
65
-- Identity and composition. (Note that these proofs are superfluous,
 
66
-- given that Bijection is equivalent to Function.Inverse.Inverse.)
 
67
 
 
68
id : ∀ {s₁ s₂} {S : Setoid s₁ s₂} → Bijection S S
 
69
id {S = S} = record
 
70
  { to        = F.id
 
71
  ; bijective = record
 
72
    { injective  =  Injection.injective   (Inj.id {S = S})
 
73
    ; surjective = Surjection.surjective (Surj.id {S = S})
 
74
    }
 
75
  }
 
76
 
 
77
infixr 9 _∘_
 
78
 
 
79
_∘_ : ∀ {f₁ f₂ m₁ m₂ t₁ t₂}
 
80
        {F : Setoid f₁ f₂} {M : Setoid m₁ m₂} {T : Setoid t₁ t₂} →
 
81
      Bijection M T → Bijection F M → Bijection F T
 
82
f ∘ g = record
 
83
  { to        = to f ⟪∘⟫ to g
 
84
  ; bijective = record
 
85
    { injective  =  Injection.injective   (Inj._∘_  (injection f)  (injection g))
 
86
    ; surjective = Surjection.surjective (Surj._∘_ (surjection f) (surjection g))
 
87
    }
 
88
  } where open Bijection