← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Function/Injection.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/Function/Injection.agda
 
1
------------------------------------------------------------------------
 
2
-- Injections
 
3
------------------------------------------------------------------------
 
4
 
 
5
{-# OPTIONS --universe-polymorphism #-}
 
6
 
 
7
module Function.Injection where
 
8
 
 
9
open import Function as Fun using () renaming (_∘_ to _⟨∘⟩_)
 
10
open import Level
 
11
open import Relation.Binary
 
12
open import Function.Equality as F
 
13
  using (_⟶_; _⟨$⟩_) renaming (_∘_ to _⟪∘⟫_)
 
14
 
 
15
-- Injective functions.
 
16
 
 
17
Injective : ∀ {a₁ a₂ b₁ b₂} {A : Setoid a₁ a₂} {B : Setoid b₁ b₂} →
 
18
            A ⟶ B → Set _
 
19
Injective {A = A} {B} f = ∀ {x y} → f ⟨$⟩ x ≈₂ f ⟨$⟩ y → x ≈₁ y
 
20
  where
 
21
  open Setoid A renaming (_≈_ to _≈₁_)
 
22
  open Setoid B renaming (_≈_ to _≈₂_)
 
23
 
 
24
-- The set of all injections between two setoids.
 
25
 
 
26
record Injection {f₁ f₂ t₁ t₂}
 
27
                 (From : Setoid f₁ f₂) (To : Setoid t₁ t₂) :
 
28
                 Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
 
29
  field
 
30
    to        : From ⟶ To
 
31
    injective : Injective to
 
32
 
 
33
-- Identity and composition.
 
34
 
 
35
infixr 9 _∘_
 
36
 
 
37
id : ∀ {s₁ s₂} {S : Setoid s₁ s₂} → Injection S S
 
38
id = record { to = F.id; injective = Fun.id }
 
39
 
 
40
_∘_ : ∀ {f₁ f₂ m₁ m₂ t₁ t₂}
 
41
        {F : Setoid f₁ f₂} {M : Setoid m₁ m₂} {T : Setoid t₁ t₂} →
 
42
      Injection M T → Injection F M → Injection F T
 
43
f ∘ g = record
 
44
  { to        =          to        f  ⟪∘⟫ to        g
 
45
  ; injective = (λ {_} → injective g) ⟨∘⟩ injective f
 
46
  } where open Injection