← 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: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2013-04-10 10:30:20 UTC
  • mfrom: (2.1.7 experimental)
  • Revision ID: package-import@ubuntu.com-20130410103020-bcspfz3whyy5iafu
Tags: 0.7-1
* [6d52289] Imported Upstream version 0.7
* [54104d0] Update Depends and Build-Depends for this version, compatible
  with Agda 2.3.2
* [b3ddce4] No need for the .install file to be executable (thanks lintian)
* [a9a6cb7] Standards-Version → 3.9.4, no changes required

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Function/Bijection.agda
53
53
    ; surjective = surjective
54
54
    }
55
55
 
56
 
  open Surjection surjection public using (equivalence; right-inverse)
 
56
  open Surjection surjection public
 
57
    using (equivalence; right-inverse; from-to)
57
58
 
58
59
  left-inverse : LeftInverse From To
59
60
  left-inverse = record
62
63
    ; left-inverse-of = left-inverse-of
63
64
    }
64
65
 
 
66
  open LeftInverse left-inverse public using (to-from)
 
67
 
65
68
-- Identity and composition. (Note that these proofs are superfluous,
66
69
-- given that Bijection is equivalent to Function.Inverse.Inverse.)
67
70