[TAG 0.4
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100927062308
 Ignore-this: d9c2b8b70a0ef83dffcf101a6d3ea11f
] 
<
[Preparation for the fourth release.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100927062236
 Ignore-this: 6eb820af7cb4621fc2cfaca013d670e3
] 
[Changed the type of _≡_ to ∀ {a} {A : Set a} → A → A → Set a.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100926182453
 Ignore-this: 330ba93350c65c182aa75cb7e9689fe9
] 
[Made some code universe-polymorphic.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100926182221
 Ignore-this: 824b0e9ac1615ab646192dc34cf71472
] 
[Proved that ¬_ preserves isomorphisms.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100926172442
 Ignore-this: c5727d26fe7fa91d406a7a38b6259566
] 
[Generalised Extensionality.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100926164952
 Ignore-this: 691ece1705000d0964163f2266e2acc4
] 
[Added ⊗-cong.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100926131906
 Ignore-this: 849b715be8daf85c35e4504863c57110
] 
[Restored the unfold function, which was inadvertently removed.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100917152822
 Ignore-this: 97f3366bda396cae977a6d49094a8610
] 
[Made Rec a data type.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100916161404
 Ignore-this: c4cc8cbbc38d5023f0d33fb15161e662
 + Pattern matching on records is now translated to uses of projection
   functions, so if Rec were a record type the termination checker
   would reject the definition of ℕ-rec which is used to motivate the
   presence of Rec.
] 
[Added Reflection.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100916154838
 Ignore-this: 149b5538d6e318be2ed42ca5f361219a
] 
[Renamed _∋_ to type-signature, with syntax type-signature A x = x ∶ A.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100915175116
 Ignore-this: 34f62e5d406935d3ecc3056ede2d60d7
] 
[Added the syntax Σ[ x ∶ A ] B for Σ A (λ x → B).
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100915174716
 Ignore-this: 9a319d0297c5ac8cf517dea1da35e19a
] 
[Changed some bound names in type signatures.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100915094643
 Ignore-this: 9cd475db014b330109d185e4e8863cf5
] 
[Updated code to reflect changes to Agda.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100915090219
 Ignore-this: 998ccad084e64af0a96ea4a9c427c1e6
 + Record pattern matching no longer destroys η-equality.
] 
[Updated code to reflect changes to Agda.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100905204312
 Ignore-this: 2938162a4dd0764c08ef03199fc4b063
] 
[Changed -> by →. 
Andrés Sicard-Ramírez <andres.sicard.ramirez@gmail.com>**20100903031705
 Ignore-this: 485916f0cdea482423b7bbdbae24db80
] 
[Renamed Function._∶_ to _∋_.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100901125938
 Ignore-this: 2996ce43ad49e939e0d314a1fa13dbd9
] 
[Made _≛_, Normal, ⟦_⟧-Normal and normalise public.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100822085805
 Ignore-this: 6a892260c9c774e7dbdad5777195bd67
 + ⟦_⟧-Normal was previously known as ⟦_⟧-NF.
] 
[Updated code to reflect changes to Agda.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100719141249
 Ignore-this: 134076a61b0e77ea4f104b81f89cf041
] 
[Added Monad.cong and the Applicative module.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100704010009
 Ignore-this: 794eafa29fbc69442e9e4770f88d11e9
] 
[Added ⊛-cong and ⊛-left-distributive.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100704005923
 Ignore-this: 83a2f3614cb0595bd53b2c5d2f3c2644
] 
[Replaced ⊥⇿∈[] with ⊥⇿Any[], which is more general.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100704005702
 Ignore-this: 73feb54765dfd7616ceee1d35d5b5d00
] 
[Removed equivalent from Surjective/_InverseOf_.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100629131124
 Ignore-this: 614f79a7aeb5f9e903cfee3baf50bc7c
] 
[Proved that bijections are invertible.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100629124700
 Ignore-this: fbe687e146629a44de49853de5ddb80f
] 
[Minor simplification, suggested by Eric Mertens.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100618140242
 Ignore-this: 745b0c802d4cf18d60be659d525a7e55
] 
[Added ⇒≈ and ≡⇒.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100607161417
 Ignore-this: 2e9c7b54c9617833e25627a9f5ec0611
] 
[Removed an empty line.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100606122505
 Ignore-this: 61739609f1a2ad316e2fe7f07102ba0
] 
[Made the definitions in Relation.Binary.Sum universe polymorphic.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100603134631
 Ignore-this: 19ec553ae719cb2dbd64f64a91a776cc
] 
[Modified a comment.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100603131413
 Ignore-this: 51f44b75265a804fa5a796e90f63cb19
] 
[Added ⊥⇿Any⊥ and ⊥⇿∈[].
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100528144441
 Ignore-this: def92929e7b7b23119153bc1bec0615
] 
[Made the example private.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100521141321
 Ignore-this: d0a91aa76d90d3e4cbb557c544308a13
] 
[Parametrised the partiality monad equality on an underlying relation.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100521141304
 Ignore-this: ecb662d95d9aff54073eaccb7dc18675
] 
[Defined equality for Maybe, including Setoid and DecSetoid transformers.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100511132329
 Ignore-this: 703c3ec9b95b5725daa5d60327a0dfef
 + Modified drop-just and decSetoid.
] 
[Added zipWith-cong and _⋎-cong_.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100517011945
 Ignore-this: 2125c854a67749e3fbecf27977a2d64b
] 
[∃ is now (again) defined in terms of Σ instead of the other way around.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100511102258
 Ignore-this: 4a5bb5f4ffc176568e12f1365ca84ab
 + When using "guardedness-preserving type constructors" I prefer to
   use ∃, but unfortunately types like A × B are often printed as
   ∃ λ _ → B when the underlying type is ∃.
] 
[Added evens and odds.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100507000442
 Ignore-this: 82c82fba105234ec402b5551cdd8edf
] 
[Reduced the use of where clauses in order to simplify proofs.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100430123834
 Ignore-this: 79cb81e900d348d353f3e547e86d4f6f
] 
[Some combinators for proving accessibility/well-foundedness.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100427154847
 Ignore-this: 3438bcac88aac70f028233b8844d2381
 + I saw that fax and glguy were discussing one of these lemmas on
   #agda, and thought it was suitable for the library.
] 
[Generalised lexicographic induction from _×_ to Σ.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100427125658
 Ignore-this: 38bdbd826a4769aa69eb08eec5c43b8
 + A while ago Conor McBride showed me a module which was almost
   α-equivalent to Induction.Lexicographic. The main difference was
   that his code was defined for Σ rather than _×_. Now
   Induction.Lexicographic also supports Σ.
] 
[Added a reference for the technique in Induction.*.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100427083919
 Ignore-this: ac0ea5a08e1a570d2a8c81c62e9c48ac
] 
[Updated code to reflect changes to Agda.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100419144459
 Ignore-this: 4ff7f5981923cf4de752dde5ad10fe69
] 
[Updated the usage info.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100409171811
 Ignore-this: 158ba23e90732c8f04e16f9f9290b30b
] 
[Σ is now defined in terms of ∃ instead of the other way around.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100404091311
 Ignore-this: 27c762aaa0a2395d3730b72d60a8df67
 + I prefer to have ∃ printed in goal types, error messages etc.
] 
[Increased the precedence of ♯_.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100401101734
 Ignore-this: 3909435c8bfd7cc9d1899ebe63f4cf0f
] 
[Added Rec.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100330030203
 Ignore-this: b60d834a52e13aab8e981653c76eb818
] 
[Removed Data.Map and Data.Sets.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100329020504
 Ignore-this: 8c296ae512d229b7f108f2690efb8a80
 + For implementations of finite maps and sets, see Data.AVL.Map and
   Data.AVL.Sets.
] 
[Added a Cabal file for the helper programs.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100325064606
 Ignore-this: 7771f212514381da33e83b27fb7ca26d
] 
[Stopped using utf8-string in AllNonAsciiChars.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100325064536
 Ignore-this: cbb617e7bf59a526fca54e653b281966
 + The IO library shipped with GHC 6.12.1 (base 4.2.0.0) makes the use
   of utf8-string unnecessary (and sometimes incorrect).
] 
[Alternative definition of bag and set equality.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100316012037
 Ignore-this: 6414e358747e35455b7e409f95c571e3
] 
[Added Extensionality.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100316012011
 Ignore-this: 7289b26ab34ef34b4b881def715a752e
] 
[Added linear-identity.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100315160728
 Ignore-this: a46b7821ef6edf802606f7653fd000b4
] 
[Containers, including some related definitions and properties.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100314231629
 Ignore-this: f960618f9aa4ab1cc60cf580091cfb96
] 
[Generalised ΠΠ⇿ΠΠ and ∃∃⇿∃∃.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100314215541
 Ignore-this: d111cf964706df2fca8d5a71b7ef9fc
] 
[Proved that implicit and explicit function spaces are isomorphic.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100314152425
 Ignore-this: 907da885b082c50192eff913723eb29f
] 
[Changed some comments.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100311125841
 Ignore-this: 29ff24208e976babc249ff2474cb6da4
] 
[Generalised IsJust and IsNothing.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100306211749
 Ignore-this: d1633f100f5e45cac6a9f757db34af0d
] 
[Made some definitions shorter.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100306211705
 Ignore-this: 8fc9e60eddb87fef1dee39ac26e1590a
] 
[Listed Peter Berry as a contributor.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100303152016
 Ignore-this: f598a5683e5c320f47fba284f36eb4e6
] 
[Added some definitions to the DecPoset module.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100303151840
 Ignore-this: a365a4eb754b1da022ca345a27cd5ed2
] 
[Add decidable posets
Peter Berry <pwberry@gmail.com>**20100226015116
 Ignore-this: 5365988797047d48781041ccbc74e854
] 
[Defined _∈_ in terms of Any.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100301191703
 Ignore-this: ac27ea7d4c8ee0022ad382f6b0a0289c
] 
[Removed the field ∼-resp-≈ from IsPreorder.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100222145328
 Ignore-this: a9d769ee52b4fcd2b2071ed8c7713154
 + Wolfram Kahl noticed that ∼-resp-≈ could be implemented, given the
   other fields.
] 
[Added Isomorphism, which can be instantiated to either _⇔_ or _⇿_.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100222143953
 Ignore-this: 5a26810154af64c530604094151af78d
 + Used this definition to reduce code duplication. Merged
   Data.List.Any.BagEquality and Data.List.Any.SetEquality.
 + InducedEquivalence₁ and InducedEquivalence₂ are now parametrised by
   a Set-valued relation rather than a Setoid-valued one.
] 
[Defined ⊆-Reasoning._≈_.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100221182400
 Ignore-this: fbbecbf8b0589ce2451790d4f9fb45d5
] 
[Moved ++-idempotent and changed its type.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100220172851
 Ignore-this: 4e90866986a6d8a0ebfa751874b2e687
] 
[Added swap.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100220134434
 Ignore-this: ee09052cefbc70fe1e7237e1d950d090
] 
[Added a module containing some simple type isomorphisms.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100220134327
 Ignore-this: cd9f16f7b99d66c0cdac953d24209558
] 
[Turned Lift into a record type. Named the destructor lower.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100220134147
 Ignore-this: eb5ebf22257dd1b9192b00dfb5991779
] 
[Changed the definitions of commutative monoid and commutative semiring.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100220134109
 Ignore-this: a2a78f7f7eaf28d2e118e3ba7935d1e1
 + The new definitions, which are equivalent to the old ones, may be
   slightly easier to use. Instead of proving that a structure has both
   a left and right identity it is now enough to prove that it has a
   left identity, and in the case of commutative semirings it suffices
   to establish distributivity from the right.
] 
[Generalised Algebra by using universe polymorphism.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100220132934
 Ignore-this: 40ca2dc3b998053ff94d89989fa9e05
] 
[Made some proofs more readable.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100218193523
 Ignore-this: 5baa14956415cc51fde099a89130645d
] 
[Added some "equational reasoning" modules.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100218193511
 Ignore-this: 3ef89705b060d55a63d8ce9d37225936
] 
[Simplified the development under Data.List.Any.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100218161131
 Ignore-this: 18f17b8a32dc1d958eab7887b199afde
 + Many lemmas have been removed (or made private), but the same
   functionality can in many cases be recovered via other lemmas.
 + The lemmas in Data.List.Any.Membership which were parametrised on
   arbitrary setoids have been removed, in favour of a simpler
   development based on propositional equality.
] 
[Proved that _×_ is a commutative monoid. Added ∃×⇿×∃.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100218160420
 Ignore-this: bb47facf08a400ec9704bc1874aaf078
] 
[Added specialised variants of (×/⊎-)equivalent and (×/⊎-)inverse.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100218160312
 Ignore-this: aeddb1f11abfe602f4168ecaa915a017
] 
[Added steps. Made the type of >>=-inversion-⇓ more informative.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100216005532
 Ignore-this: b89abb637c8ee025c1bf68aa73cb760a
] 
[Added ≤-Reasoning._<⟨_⟩_.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100216004057
 Ignore-this: 5ad50d970e0624cd21437b1e581b2798
] 
[Added _⇓_, _⇓[_]_, _⇑ and _⇑[_].
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100216003436
 Ignore-this: 577bcfbe689ba05f3686bb761c87b274
] 
[Added unlines.
Andrés Sicard-Ramírez <andres.sicard.ramirez@gmail.com>**20100209191347
 Ignore-this: 545dcd53fbbee0c7eb7c2c08495e73f7
] 
[Generalised some definitions.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100211104949
 Ignore-this: 7289ea5bbdf59042a27f000b998da34f
] 
[Added a module for equational reasoning.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100209190233
 Ignore-this: 7762ece933414fc9e3d6325a95720248
] 
[Added a partial order.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100209184809
 Ignore-this: a6385ee2a7982d6bc30e83504282a87b
] 
[Added an alternative, but equivalent, formulation of equality.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100208174120
 Ignore-this: 8fb191e2a83e33b0fe2bb972853d6833
] 
[Defined strong equality.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100208141213
 Ignore-this: 4b175f78841ae2ff2b5ad2b0aafc96a8
] 
[Defined equality, proved some properties, renamed some things.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100208130637
 Ignore-this: 813bbbe1ba71f1aa0b64a5dd322a6d91
] 
[Added Excluded-Middle and Double-Negation-Elimination.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100208130454
 Ignore-this: 2bbf593e389831e5308107907d2d4d97
] 
[Added wrappers for IO.Primitive.appendFile.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100206003852
 Ignore-this: be87daff54eac1939b38e3ade66e3259
] 
[Added appendFile.
Andrés Sicard-Ramírez <andres.sicard.ramirez@gmail.com>**20100204162443
 Ignore-this: eadd7b4f5523613f942ae7b507d13475
] 
[Proved that _>>=_ distributes from the left over _++_.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100203013222
 Ignore-this: 2daec5caff401a16336b1b8caea98d6d
 + Assuming that bag or set equality is used.
] 
[Proved some monad (with a zero and plus) laws.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100202233616
 Ignore-this: bd6923cadd6c10c0097def30d575d2bf
] 
[Renamed (LeftInverse|Surjection|Inverse).equivalence to equivalent.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100202135604
 Ignore-this: 8f48dcdfbbff23b069e58a7b0898928b
] 
[Mirrored changes to Data.List.Any.BagEquality.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100202134822
 Ignore-this: 2ae28792f2b39db9170efff6d1d136ae
] 
[Proved that concat and _>>=_ are congruences.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100202134700
 Ignore-this: 851209fc26de640a408ff1b4444fc54d
] 
[Small refactoring.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100202133352
 Ignore-this: 8ec8a629e6c6395f74bdd7d3cfc07acb
] 
[Changed the definitions of concat-∈⁺/⁻. Proved that they are inverses.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100202133207
 Ignore-this: 5b1c56a4ab9d9362e1e42afae336ded8
] 
[Moved parts of Data.List.Any.Properties to a new module.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100201181859
 Ignore-this: fe9ed21a46ce8f39ff18a1b466c5825a
] 
[Added map and zip.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100201135615
 Ignore-this: 82ebcccd8dc5603fcb202db5e02bbf9a
] 
[Added map and zip.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100201135606
 Ignore-this: 5ca2ed20999278f7639d3985e439890c
] 
[Added Any-cong. Simplified a proof.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100117141407
 Ignore-this: 9448308b6c112e3671dce0771fa81801
] 
[Proved that _++_ and [] form a commutative monoid. Removed _++-cong_.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100117141319
 Ignore-this: 89c6b30195311cca435c016ac0272bf5
] 
[Updated copyright year range.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100130213014
 Ignore-this: ce3de0d707560c446d030421a8f82c8e
] 
[Improved a comment.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100120214004
 Ignore-this: 5d374d2fa0e29c7e8f160a614e260cd4
] 
[Moved a comment.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100118000224
 Ignore-this: 2b476d7436a4a20affc5b4a8214e7d40
] 
[Proved that find and lose are inverses.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100117130502
 Ignore-this: 9954126caa6b52b1d4c038cb5b664d8f
] 
[Made uncurry less strict. Added uncurry′.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100117125415
 Ignore-this: 3aeb8e217105e5b49c8753020c61c639
] 
[Removed unnecessary direct importation of Core modules.
Andrés Sicard-Ramírez <andres.sicard.ramirez@gmail.com>**20100114151524
 Ignore-this: d0d9f0fdeeac6794cd0ac2bf26792c35
] 
[Turned Σ into a record type.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100113223253
 Ignore-this: 45f510af79ccba9fec9bf9fb30a5f072
] 
[Removed the need for --injective-type-constructors.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100108192113
 Ignore-this: 23deedc66dbf3fcdc209190f2a55425d
] 
[Minor changes.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100107194437
 Ignore-this: f9c4fbeacf4662727d9ba095d0b68026
] 
[Generalised some lemmas, proved that ++-comm has an inverse.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100107193830
 Ignore-this: d4f1e22db07beaed552b2ecefafa94ad
] 
[Properties related to set equality.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100106163910
 Ignore-this: 97106021035d45dba66bab19f90813dc
] 
[Properties related to bag equality.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100106163903
 Ignore-this: b8bd962216352b145635242235b61cd2
] 
[Pointwise "dependent products" of binary relations.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100106162205
 Ignore-this: bec1d04a4227d32055e05be66ed2fef5
] 
[Added indexedSetoid and ≡⇿≅.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100106161809
 Ignore-this: ef01c5bea30480e5c51a3c19022c39b5
] 
[Established some inverses more formally.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100106161616
 Ignore-this: 3c320db541bf050c6a2c544bb2b2c332
] 
[Defined "Π-setoids". Removed some definitions.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100106153958
 Ignore-this: a2aeb6f0f7f120eb608ff50b1c5e3095
] 
[Some properties related to equivalences and inverses.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100106151537
 Ignore-this: 57934250f71146428e5ae14489e1c637
] 
[Some properties related to equivalences and inverses.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100106151411
 Ignore-this: 52b8885aa67ab32359acb4cb155602e2
] 
[Some definitions related to indexed binary relations.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100106151333
 Ignore-this: f63b10054a5d26f229075d0f16c518a9
] 
[Changed a comment.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100106020352
 Ignore-this: 941f040b8fbb120b68911caf5f04ad54
] 
[Removed some unnecessary imports.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100106020306
 Ignore-this: 2b586ba789f41dbd4c331e83190f871
] 
[Changed the type of _with-≡_.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100104171239
 Ignore-this: b4acf66dbbc890c87342af02912febda
 + Replaced y ≡ x with x ≡ y. The latter type seems to be more
   convenient when used with the rewrite construct.
] 
[Changed the definitions of bag and set equality.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100103222655
 Ignore-this: 69f839f6612a7e4819ed0b8f2a1a15c8
 + The definition of Membership.Bag-equality, which uses propositional
   equality, was moved to Membership-≡.
 + Removed Membership.Set-equality. Changed the definition of
   Membership-≡.Set-equality to match Membership-≡.Bag-equality.
] 
[Moved _⇔_ to Function.Equivalence and changed its definition.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100102215938
 Ignore-this: 7340e6bd00aba99b0805f3cfebd1c3fa
] 
[Added _⇿_.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100102185856
 Ignore-this: 60120c5f2b486d0ffcd781bf53a8a8be
] 
[Added Function.Equivalence.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100102185525
 Ignore-this: 6f1d0d8bfd158eb5610428c6c013fa31
] 
[Defined bag equality.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100101223518
 Ignore-this: e0bb114eb355be8cab76f38bb9bbd507
] 
[Added InducedEquivalence₁ and InducedEquivalence₂.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100101223419
 Ignore-this: 4af412ede73123b7bd98d0bb35ad4aa
] 
[Renamed set-equality to Set-equality.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100101170848
 Ignore-this: c07798fc1c3af7a4b9bb69fdab589a64
] 
[Renamed inducedEquivalence to InducedEquivalence.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20100101170701
 Ignore-this: c035dbea559f76aca89279ea9006c91a
] 
[Proved that _∷ʳ_ is injective (in both arguments).
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20091230222830
 Ignore-this: eeefadb6d72c6faa6e9739b0cd28d1b6
] 
[Renamed Data.Function to Function.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20091229144903
 Ignore-this: 9357ef6a5024005600d70fba1ef77d35
] 
[Added modules for surjections, bijections and inverses.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20091229144223
 Ignore-this: bbb6c639f5ddf56ad6fe8950770d5cea
] 
[Removed release-specific information.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20091223163021
 Ignore-this: 268384a55f497f0872b96b995b60b12c
] 
[TAG 0.3
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20091223004231
 Ignore-this: d73c9a860ce25063878c0b50f67b4b28
] 
>