[TAG 0.3 Nils Anders Danielsson **20091223004231 Ignore-this: d73c9a860ce25063878c0b50f67b4b28 ] < [Preparation for the third release. Nils Anders Danielsson **20091222232142 Ignore-this: 39d020a8491d5cf791f63ecdb6ae1699 ] [Added _,′_. Nils Anders Danielsson **20091217161324 Ignore-this: b68c9b0049843a3d7f01184e3b9f4687 ] [Moved some modules related to functions. Nils Anders Danielsson **20091222231816 Ignore-this: 76f87ab0058271c48c94165f0e5aebca ] [Added Surjective. Nils Anders Danielsson **20091222193157 Ignore-this: 5840c129751618e153a74fb30be245a3 ] [Added Lift and lift. Nils Anders Danielsson **20091222193138 Ignore-this: 1739ac00b628441f2ededfad6bf33be5 ] [Added proof-irrelevance (twice). Nils Anders Danielsson **20091217234843 Ignore-this: c3a98de7bc6cb57a05da7590b526adc4 ] [Minor simplification. Nils Anders Danielsson **20091218211939 Ignore-this: 82d174dcf40cedc9af80d18a01fa930f ] [Generalised Induction. Removed Induction1. Nils Anders Danielsson **20091218175912 Ignore-this: f0998d770d0314efefc3bbff3147a3c ] [Generalised Relation.Unary. Removed Relation.Unary1. Nils Anders Danielsson **20091218174354 Ignore-this: e57bc3a8bc46bd7bc58182f7dd98351e ] [Removed Data.Empty1 and Data.Unit1. Nils Anders Danielsson **20091218171358 Ignore-this: d695478437e163b24f7f92db7933297c ] [Removed Rel. Renamed REL to Rel. Added a new definition of REL. Nils Anders Danielsson **20091218170306 Ignore-this: b874020558de497de44d4b41085c93eb ] [Removed the dependency on utf8-string. Nils Anders Danielsson **20091217134607 Ignore-this: 1dfcf36ab3c71b8c8c300e2219c3f4a0 ] [Proved that Any.map is functorial and established some bijections. Nils Anders Danielsson **20091209112721 Ignore-this: aced53b044bcb87ae529993e14556e50 ] [Added eq?. Nils Anders Danielsson **20091203171444 Ignore-this: e242e58685be6bc5ca01bb80b73e1fc2 ] [Defined identity and composition for injections and left inverses. Nils Anders Danielsson **20091203154546 Ignore-this: 48295af30d3d801b407744947a94cae8 ] [Moved injections and left inverses to separate modules. Nils Anders Danielsson **20091203152210 Ignore-this: 4f733a0f30ba59c071a34abbdd9c1530 ] [Added some fixity declarations. Nils Anders Danielsson **20091203143026 Ignore-this: 5c45788481df548def537ec32706e84 ] [Replaced Σ! with ∃!. Nils Anders Danielsson **20091201193251 Ignore-this: 77adb6655862d4686364cd28a4b03a6b ] [Listed Darin as a contributor. Nils Anders Danielsson **20091201192749 Ignore-this: d2423f5f64a13ab15d8c0b6a6c7513ff ] ["Unique" existence wrt an arbitrary endorelation. dwm@cs.nott.ac.uk**20091201181123 Ignore-this: 3ebb4b6588bf79672aeff9a6d9539d9 ] [Another note about contributions. Nils Anders Danielsson **20091202114803 Ignore-this: 67d309cb2e3b50a06a5310deff05d8d4 ] [Generalised Data.Vec. Nils Anders Danielsson **20091202114154 Ignore-this: 5d8b8bfb9b92904b9a2eb9517187c40f ] [Improved the documentation. Nils Anders Danielsson **20091201131544 Ignore-this: cd94f78100a0b4ba1a9b197e30a83fa8 ] [Added ≈-Reasoning, ⊑-Reasoning and ⊆-Reasoning. Nils Anders Danielsson **20091130150528 Ignore-this: ed36bdaaf2b8fcf49de616833939bbe1 ] [Added _⊆_, ⊑⇒⊆ and ⊆-Preorder. Renamed poset to ⊑-Poset. Nils Anders Danielsson **20091130150234 Ignore-this: 175b1cb262aeaea413d15ecbdd88dd40 ] [Added Finite, Infinite and some lemmas. Nils Anders Danielsson **20091115153307 Ignore-this: d3d5e04e628f8fe7a58841f0fcd28c50 ] [Added Relation.Binary.InducedPreorders. Nils Anders Danielsson **20091124184432 Ignore-this: 731398a0f29be4a5ec64d36a82f9041b ] [Defined id, _∘_ and const for _⟶_. Nils Anders Danielsson **20091130145628 Ignore-this: abd9d62f3ed2534eae799f681103ce77 ] [Tried to make some views easier to use. Nils Anders Danielsson **20091130141457 Ignore-this: f490da1b1f08166e324ec7cc94b302fc ] [Renamed decToBool to ⌊_⌋. Nils Anders Danielsson **20091122183401 Ignore-this: be621737c52c60a99d3ccaf764238f15 ] [Generalised the definitions in Relation.Nullary.Decidable. Nils Anders Danielsson **20091122181455 Ignore-this: 3c7865f5f898479555ae4cbfd61dabf6 ] [Defined _**20091122180706 Ignore-this: 93471bf63f4c682b3c90cd4a118a9659 ] [Exported irrefl from IsStrictTotalOrder. Nils Anders Danielsson **20091122175353 Ignore-this: bed016756917d46aa309402458e4cbff ] [Renamed pres(-≈) to cong. Nils Anders Danielsson **20091122115625 Ignore-this: 9c686eab35e9648682ca3eb8f8810bfc ] [Removed Congruential(₂), subst⟶cong and cong+trans⟶cong₂. Nils Anders Danielsson **20091120234917 Ignore-this: b40126bbb9e9c2957472e7c02955c8bc + The definition of Congruential was not general enough to be used in the type signature of, for instance, Relation.Binary.PropositionalEquality.cong. ] [Renamed carrier to Carrier. Nils Anders Danielsson **20091120194648 Ignore-this: 2066ea5d5c7e45311fedb9c87b1a4443 ] [Generalised the remaining definitions in Data.List.Properties. Nils Anders Danielsson **20091124185851 Ignore-this: 8c6d62a7abf63a800b38a97b9e66cbbc + Except for left-identity-unique. ] [Generalised Relation.Binary. Nils Anders Danielsson **20091120194112 Ignore-this: a2cd7cd55afdab57542410fd9b3222b6 ] [Added a COMPILED_DATA directive for Bool. Nils Anders Danielsson **20091122113013 Ignore-this: a08ca2b091e621a7c772f02f011d0321 ] [Mostly cosmetic change. Nils Anders Danielsson **20091120225831 Ignore-this: c2e18fa4c64aaa1841bb81b6241d889c + I aim to use matching letters for sets and their universe levels: A : Set a, P : A → Set p, etc. ] [Mentioned another contributor. Nils Anders Danielsson **20091120222053 Ignore-this: 4af11dae43b4e987c04c34a349278948 ] [Added a missing name. Nils Anders Danielsson **20091120221957 Ignore-this: 198d4a353d613e7910ecc33f447bc084 ] [Remove Data.List1 Nicolas Pouillard **20091120213518 Ignore-this: ab1c1fbb772644a2f62662e2f07cf94c ] [Data.List: generalize using universe polymorphism Nicolas Pouillard **20091120213457 Ignore-this: fbfcf7bc84f69478e7b9995751de21b5 ] [Data.Maybe: generalize Maybe using universe polymorphism Nicolas Pouillard **20091120211919 Ignore-this: 9d9776ccef88bd9bf9892b22925e72e1 ] [Data.Graph.Acyclic: Add a Set annotation Nicolas Pouillard **20091120211832 Ignore-this: 4a63e93261dd25eb2c367a205b39aa01 ] [Cosmetic change. Nils Anders Danielsson **20091120002405 Ignore-this: 88e13834dc549a629b8b227e6169c82e ] [Added more guidelines for contributors. Nils Anders Danielsson **20091120183233 Ignore-this: 12bae9bc5c1c35a03dbae2db7ec7db04 ] [Added ++-comm. Nils Anders Danielsson **20091116231120 Ignore-this: 1dc7568cd417c88361711aa8a9811f94 ] [Generalised →-to-⟶. Nils Anders Danielsson **20091116231045 Ignore-this: 8278ac2885eaced8787f2639f8579f41 ] [Added finite. Nils Anders Danielsson **20091116192813 Ignore-this: 723b9e70bcc87a93cb63e30e5ce077ed ] [Added set-equality. Nils Anders Danielsson **20091116143447 Ignore-this: 55c8cf77e583cc52c5af4d8b522f3f59 ] [Showed that every preorder induces an equivalence relation. Nils Anders Danielsson **20091116143157 Ignore-this: 1c5513f46a5e0b3f5fea14d59f876d26 ] [Definition of and lemmas related to "true infinitely often". Nils Anders Danielsson **20091115172947 Ignore-this: 69c9a32998e7c26060d095a0f163a5bf ] [Removed preorder and setoid. Use decSetoid instead. Nils Anders Danielsson **20091114203527 Ignore-this: ca2c0f6bead29e892228dad2b98fd2c7 ] [Added independence-of-premise and independence-of-premise-⊎. Nils Anders Danielsson **20091114203437 Ignore-this: e1df0a76f11848ca019290e898b24451 ] [Generalised if_then_else_, removed if₁_then_else_. Nils Anders Danielsson **20091114203011 Ignore-this: 3e03e1e44579d30e99223cd283bc4647 ] [Added Stable and stable. Renamed some functions. Nils Anders Danielsson **20091113202427 Ignore-this: a4e14182bbfe829e3a8b448717fc96c4 + Renamed ¬¬-drop to negated-stable and ¬¬-drop-Dec to decidable-stable. ] [Removed preorder, setoid, decSetoid and poset. Nils Anders Danielsson **20091113174223 Ignore-this: 8d7d6032baec64cef6a8c1516cad1d04 + Use decTotalOrder instead. ] [Made _⊎_ universe-polymorphic. Nils Anders Danielsson **20091113172929 Ignore-this: cabf49143541c75fa0f7ebaa1377e725 ] [Improved a comment. Nils Anders Danielsson **20091111160030 Ignore-this: d90df4c540cdb70f989dac4a2cda3a00 ] [Added m≤m⊔n. Nils Anders Danielsson **20091110235509 Ignore-this: 9e0e7e3995adfd57397f03a653af40b3 ] [Added Andrés as a copyright holder. Nils Anders Danielsson **20091109200907 Ignore-this: a90e36dd36fa96f61972be677f2ac7d8 ] [Minor change. Nils Anders Danielsson **20091109200732 Ignore-this: e782f470f27657c652bf4e290bc43fcd ] [Added fromString. Andrés Sicard-Ramírez **20091109170742 Ignore-this: 5387666dbdb65a7385899d5b6dc5fa7d ] [Made m≢1+m+n public. Nils Anders Danielsson **20091109124739 Ignore-this: 5a8ec158234f11d47a135fd5ad53aa6d ] [Made the code in Relation.Nullary.Negation universe-polymorphic. Nils Anders Danielsson **20091109123220 Ignore-this: b0e76763d10f114b9ee5953a26f892ed ] [Generalised ¬∀⟶∃¬-smallest. Nils Anders Danielsson **20091109123055 Ignore-this: 1d9837a5ad4e0b9e2ea2ee29c42d55ad ] [Renamed witnessToTruth to toWitness. Added fromWitness. Nils Anders Danielsson **20091109122531 Ignore-this: c765681d8d8f475ee3c05c9ca3ac1ed6 ] [Improved the documentation. Nils Anders Danielsson **20091108192342 Ignore-this: 6df82294166a73ae0ce189b0af30c0b7 ] [another termination issue ulfn@chalmers.se**20091109084132 Ignore-this: 4171e1634cf7671884fac08da2767891 ] [fixed minor termination issue ulfn@chalmers.se**20091104144126 Ignore-this: fbee2138882c43720d63a3ebc0dcf2bc ] [Generalised ⊥-elim. Nils Anders Danielsson **20091101004033 Ignore-this: c073c4bcef82cdc6879f52727187257e ] [Generalised _⇔_. Nils Anders Danielsson **20091027133858 Ignore-this: c0f206d17b415f2c9c41cb1107b9b8c7 ] [Generalised sym, trans, subst(₂) and cong(₂). Nils Anders Danielsson **20091026173650 Ignore-this: 26119ff02fc9fc818f1de201316c6753 ] [Added snoc and initLast. Nils Anders Danielsson **20091023154154 Ignore-this: 6e020e6320917ca4a8f88502d044e0c7 ] [Defined a view which can make it easier to traverse lists from the end. Nils Anders Danielsson **20091023135834 Ignore-this: bb925a880303d84508672b4cf7cf934f ] [Added length-++. Nils Anders Danielsson **20091023135405 Ignore-this: e1551f1fce396e4812b75e27b1d27ce ] [Made Dec universe polymorphic. Nils Anders Danielsson **20091021233450 Ignore-this: 3c1c314ea719579b008bc2b17d90a292 ] [Made some equality types universe polymorphic. Nils Anders Danielsson **20091021231059 Ignore-this: 1f0fdc7040ca3d2c016195d65734b779 + Removed _≡₁_ and _≅₁_. ] [Made the product types universe polymorphic. Nils Anders Danielsson **20091021223902 Ignore-this: abccce64cce4a6810b8e04d5d3e0d757 + Removed Data.Product1. ] [Started using record constructors. Nils Anders Danielsson **20091020144805 Ignore-this: 9890b1dc40a65f1b3e8b72d8e07f76ef ] [Made ¬_ universe-polymorphic. Nils Anders Danielsson **20091021201521 Ignore-this: e5586ba2182bcda6fa872fcfc9628322 ] [Made ∞ universe-polymorphic. Nils Anders Danielsson **20091021195017 Ignore-this: 4284d479822ad518826d18b5e2e18cdc ] [Generalised many definitions in Data.Function. Nils Anders Danielsson **20090925221824 Ignore-this: 9f7f818dbb4fe66daf2c6461536b1588 + Removed _∘₀_, _∘₁_, id₁, const₁, flip₁, _$₁_, _⟨_⟩₁_, _on₁_, _-[_]₁-_ and _∶₁_. ] [Minor addition: head, tail, [_], ++, concat, splitAt, take, and drop for Vec1. scm@iis.sinica.edu.tw**20091020061413 Ignore-this: 38e227bd2534185aed24e4e7595cb755 ] [Removed Data.List.Equality. Nils Anders Danielsson **20090927155050 Ignore-this: 34098e33191ad2f852d86113eaa9d7b0 ] [Universe levels. Nils Anders Danielsson **20090925211254 Ignore-this: 650cc6e5d82ccedcb38bc9f22ea4b555 ] [Made the code type check when --universe-polymorphism is used. Nils Anders Danielsson **20090925201833 Ignore-this: f0984fb1b7671a0cd0201a1a94e7a159 ] [Motivated a design choice. Nils Anders Danielsson **20090925140032 Ignore-this: e43d17d5c2469d409e08db2752c6b30c ] [Added documentation. Nils Anders Danielsson **20090914223900 Ignore-this: 436dbcb8586a09f9e659e42f6839b20c ] [added trustMe : {A : Set}{a b : A} -> a == b ulfn@chalmers.se**20090914134233 Ignore-this: 2e5069675f6a7bfc75e2055e89df5c78 - this was added as a primitive to Agda - this is used in the decidable equality for strings making it reduce nicely ] [Added HeterogeneousEquality.from-≅. Nils Anders Danielsson **20090906113427 Ignore-this: e25ed385ddb09579121ce4646c7947f7 ] [Added left-identity-unique. Nils Anders Danielsson **20090904105005 Ignore-this: 5d654399a4ed0f6c8962a8e069b20199 ] [Dropped the List- prefix from many names. Nils Anders Danielsson **20090904003254 Ignore-this: aa4fed0c6cbeb48d71058cbee7d63e76 + Furthermore List-≈-respects₂ was renamed to respects₂ and a couple of functions were removed. ] [Added Relation.Binary.List.NonStrictLex. scm@iis.sinica.edu.tw**20090814043416 Ignore-this: 5ed9ce63b7365fcec35710c6061e079b ] [Extended Relation.Binary.NonStrictToStrict with antisym->asym, isPartialOrder->isStrictPartialOrder, isTotalOrder->isStrictTotalOrder, and isDecTotalOrder->isStrictTotalOrder. scm@iis.sinica.edu.tw**20090814042916 Ignore-this: a3e88fc6fc068a4638e530015524cc6a ] [Added Relation.Binary.List.StrictLex. scm@iis.sinica.edu.tw**20090814042812 Ignore-this: 8befffa394a29aaf6811ac6d2a43a10b ] [Data.List.Equality is now defined in terms of Relation.Binary.List.Pointwise. scm@iis.sinica.edu.tw**20090811041213 Ignore-this: c4bcb8c6b6bf778e73b439d62e194721 ] [Added Relation.Binary.List.Pointwise. scm@iis.sinica.edu.tw**20090811023609 Ignore-this: 97d1773b2f8c1f2925204a7f98906790 ] [Simplified _-Ring⟶_. Some fields followed from the others. Nils Anders Danielsson **20090902095324 Ignore-this: d2b048ee822370702be26ebce9d8bfcd + As pointed out by many sources. ] [Added +-group to Ring and CommutativeRing. Nils Anders Danielsson **20090902092118 Ignore-this: 13ed794397a18e403b4f7e465b146960 ] [Added the field ⟦⟧-pres-≈ to _-Ring⟶_, removed _≈_ from RawRing. Nils Anders Danielsson **20090902000702 Ignore-this: 981b788a1e755c4d1d3fa0b4fa13f156 + Furthermore _-RawRing⟶_ was removed. ] [Defined equality for Coℕ. Nils Anders Danielsson **20090828215845 Ignore-this: 4076576282103f822b99dd904a3b030f ] [Modified a comment. Nils Anders Danielsson **20090828212325 Ignore-this: eda1efb082060143815813ecc221e90b ] [Added a snoc-view and a function extracting the last element. Nils Anders Danielsson **20090809100014 Ignore-this: 96b30dbd0e19aac9f29a2613efd5a4c ] [Added _$₁_. Nils Anders Danielsson **20090809093628 Ignore-this: d7e59eda96cb0106ae5a431ce4f1be26 ] [Removed release-specific information. Nils Anders Danielsson **20090707213056 Ignore-this: a7a2da8b41668c08beb7c46c5c7942ca ] [Brought the predist setting up to date. Nils Anders Danielsson **20090707213757 Ignore-this: a8f591fa20135792455988495f5fe762 ] [TAG 0.2 Nils Anders Danielsson **20090707212856 Ignore-this: d41bcf03c33769a41cc72733aa9b9234 ] >