← Back to branch summary

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

« back to all changes in this revision

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