pristine:0000000374-84974733cc135d67de774887bbfdda2ce8688f374192f241f75b28dda32b09a4 [Added a boring file. Nils Anders Danielsson **20110622072623 Ignore-this: f4d98e1692c99c1de62cb40ac1840f48 ] hash: 0000000247-1dea27a78493354a8ebdd8509771a998b94a45cc6c4b8611e9cc297458887b8b [The beginning of a library for dependently typed syntax. Nils Anders Danielsson **20110624223325 Ignore-this: f8a2a930f15a926bd187e83cdcabf0ea + This patch includes a number of unfinished or bit-rotted experiments, which I plan to delete or update. ] hash: 0000279683-b473a98503d3562188cd1e54ee661a9f107b9a22bef1828d7531bdb4754e17ea [Updated code to reflect changes to library API. Nils Anders Danielsson **20110624223333 Ignore-this: be801fe03e594742a7a9949c9c5b9186 ] hash: 0000004619-889b620695f3e16eccf288df64b5293a94263fff54b6cf52c3bab970f50f9b05 [Removed alternative definition of substitutions. Nils Anders Danielsson **20110624223333 Ignore-this: 98a49969d5ef85c58d12a59db2741121 + These substitutions are not indexed by their semantics (context morphisms). This makes them much harder to work with, because one frequently needs to prove that a substitution has a given semantics. I realised that it was a good idea to index substitutions by their semantics when I introduced substitutions defined as functions instead of data, and I found the representation of substitutions as functions when I decided to implement a map operation for substitutions. ] hash: 0000031711-2b7f1be978ec42ecf181983d05df0624edfe68a1890c20f0d13f23d5b841821f [Replaced heterogeneous equality with equality of telescopes. Nils Anders Danielsson **20110624223611 Ignore-this: 621bb9b52d77b9d4fadb0e365d3aab9e + See deBruijn.Context for motivation. ] hash: 0000190190-56948123c96454cd3722debbb337dcad40d94698946f862651aca75d0f92b7ce [Renamed _/Val_ to _/̂Val_. Added _/Val_. Nils Anders Danielsson **20110624223618 Ignore-this: f5609439c3e442d92ebd61b20259e06d ] hash: 0000007441-f5a97fbf0b13317b74d1ebeea5d47afc779e67d94de9c5d3cb526b497d8354ce [Removed ▻-/̂-++-/̂⁺-/̂⁺-ŵk. Nils Anders Danielsson **20110624223618 Ignore-this: b585695bf43b5105fb76592f5073d4b0 ] hash: 0000000949-d0ce0a5070b803b80c566737216ce6dbcdd6775761d7da1a9f61c14452adaac4 [Added _↑_ and _↑⋆_. Changed the definition of _↑̂_. Removed _⇨̂₁_. Nils Anders Danielsson **20110624223618 Ignore-this: e93e6ba62df8e5545decb48f4840eb13 ] hash: 0000008701-4177d5130b749eeb54c01230006571e81eca32b5a21f399ef5dac76633a98178 [Renamed var-/⊢-↑⁺-wk-↑⁺ to var-/⊢-↑⁺-/⊢-wk-↑⁺. Nils Anders Danielsson **20110624223618 Ignore-this: 2a9658070cb5bc273d49318631b91338 ] hash: 0000001813-46e54d1bd4fece525e7d3c06301b2a0e2e6f589e2df039b96ffa81d9aa95815c [Added variants with more explicit arguments for many combinators. Nils Anders Danielsson **20110625095635 Ignore-this: c3f4a7b7d2b7492e687e8c90fe7e8e32 ] hash: 0000041794-8528caa6bda23bc13654e65cf812f2032f9e0d6d2ed3090a8b8c1ae9118a189a [Removed [Curried-Type] and [Curried-Value]. Changed the type of ƛ. Nils Anders Danielsson **20110625104547 Ignore-this: 5e3fd6bf60e6799a1e684f576e8fdee2 + The type of ƛ was changed from ∀ {Γ σ τ} → Γ ⊢ σ type → Γ ▻ σ ⊢ uc τ → Γ ⊢ k U.π ˢ σ ˢ τ to ∀ {Γ σ τ} → Γ ⊢ σ type → Γ ▻ σ ⊢ τ → Γ ⊢ k U.π ˢ σ ˢ c τ to avoid the use of _≅-Curried-Type_ in ƛ-cong. An example indicates that the new type signature may be more practical. + The use of _≅-Curried-Type_ in ·-cong was avoided by making the lemma less general (with homogeneous instead of heterogeneous input equalities). ] hash: 0000013814-4ad099fd0dcf1b907c792a8cf0dee090af85de4413c95590c21fb675a879748c [Experiment: Made the universe larger. Nils Anders Danielsson **20110625142201 Ignore-this: 4600c4805732158d0efc13d54ce7ea6f ] hash: 0000010488-fe7a4af1c1280c8c29a5544172210b9d9942363a54e95712e7755335b2f312fa [Rolled back an experiment. Nils Anders Danielsson **20110625142248 Ignore-this: caebc100291a575c53ba2f9a4c4becce ] hash: 0000010477-08bc62766993e8435cb24b429d8bbb51e91635aa7b628c2b6dc7e4b321cf4448 [Experiment: curry-cong and ˢ-cong can be replaced by P.cong/P.cong₂. Nils Anders Danielsson **20110625144120 Ignore-this: 35fe249d660e09426673c7ceb8c359c4 ] hash: 0000002817-768585315d700a2a6057eb6967b0e77a91c0dd6aeaba7c15f2cec95a260ebfbb [Rolled back an experiment. Nils Anders Danielsson **20110625144225 Ignore-this: 9be6783d24e5fb96d26165957a886511 rolling back: Sat Jun 25 16:41:20 CEST 2011 Nils Anders Danielsson * Experiment: curry-cong and ˢ-cong can be replaced by P.cong/P.cong₂. M ./README/DependentlyTyped/Substitution.agda -16 +15 ] hash: 0000003019-7ae6c9d0d64266ee7639077f1f6a19fe25c913681cedc26e774184b57c0173aa [Updated README.DependentlyTyped.NormalForm. Nils Anders Danielsson **20110626104121 Ignore-this: 74a824231e2da72e36a0c5677547339f ] hash: 0000019946-047158bdeb2e3611fb05b93a0e06d3b3509dc87e468099d43eadb3c2b61943cd [Updated README.DependentlyTyped.Spine. Nils Anders Danielsson **20110627205314 Ignore-this: 80607ac182210cad2a3f1fa10e7f582b + I am not satisfied with the current definition, because it would be rather awkward to use in README.DependentlyTyped.Kripke-model.Definition. + Removed README.DependentlyTyped.Spine2. ] hash: 0000010813-9b50722d1a6074e80fcee0a9208edb4b75988d3a5138972972c3592052f8aa5f [Updated README.DependentlyTyped.TypeOf. Nils Anders Danielsson **20110628091356 Ignore-this: 6db897aa35949e8a68f0918fda0a55cf ] hash: 0000001709-e7f001adbd5e837a63fca248aa9d906d0f9574e83f8953ca04d22151daa0ff37 [Added /̂∋-⟦⟧⇨. Nils Anders Danielsson **20110628123101 Ignore-this: cb5cc7e3b8a7cf41a08959b90bda6cdb ] hash: 0000001631-d86356876afe0bb2d21ead3b08c6389bd49f5adabf3313e31e6509b379a74d0f [Experiment: Replaced snoc with cons in definition of context extensions. Nils Anders Danielsson **20110628142432 Ignore-this: da24123314a88bb0d13a55bb3adb557c + With this change in place I could simplify deBruijn.Context, but other parts of the development became more awkward. Examples: * deBruijn.TermLike.lift. * deBruijn.Substitution.Data.Simple.wk⁺. * I suspect that the definition of proofs like var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆′ would have become more tricky. ] hash: 0000015645-f2a0cb529ead119a8de6c795d823524edfe838d782daaea8daed86c0d00db974 [Rolled back experiment. Nils Anders Danielsson **20110628142616 Ignore-this: 5b572cfa911863636f5be7adf3b08571 ] hash: 0000015255-9f24b6fab004039fe58d5680f95db00947b608c5f3470376839c495a3400eec1 [Updated README.DependentlyTyped.Kripke-model.Definition. Nils Anders Danielsson **20110704073929 Ignore-this: c90bf01777f0a384fc7fbb6afd68db38 + This module was previously known as README.DependentlyTyped.NBE. + The code still does not pass the termination checker. + README.DependentlyTyped.NBE2 and .NBE5 were removed. ] hash: 0000016247-1fd02be15b0ddc15fe41af0baf87bd0c8e3fc11f572e3869cc403efb1803cec4 [Sketched some more constructions for the Kripke model. Nils Anders Danielsson **20110704074017 Ignore-this: 46a7543dfb5e4747df5d406f627190 + Indexing the values by syntactic types seems to lead to problems. ] hash: 0000004754-6949b4c41290369f19255cb9a3d117b55f68626f80ae0dd5a629f55b4b497682 [Equality of [_⟶_] functions now ignores the proof component. Nils Anders Danielsson **20110704135929 Ignore-this: f2ca1a51edb308dca18a9e6c0b3df36 ] hash: 0000017093-ad157bbae76243a2ea6da877c5610c7758b9077e9daa5c938cca72995138c125 [Cosmetic changes. Nils Anders Danielsson **20110704142345 Ignore-this: e76abff858f960094c1a6b83b7586a5f ] hash: 0000001285-bdb1b816e20f9ba36c5fa2d0f55b3600151e3409408d783f21b9f319747cefa1 [Revived some modules dealing with substitutions defined as functions. Nils Anders Danielsson **20110705123146 Ignore-this: 4abbf5b5f7fb7493f58688f2abeb7a27 ] hash: 0000060482-6286ebac7b2cb0315991f1e2aeb589827a5797f7adc64af970b6be1d83005cf7 [Documented why the lambdas are annotated with types. Nils Anders Danielsson **20110706094727 Ignore-this: bf4f57a241a621a45249e3228942f062 ] hash: 0000000665-5ca990f3b9a7774ec6423049bfdac9b44f44df3a0d2c7120ffc9e6c8ee620238 [Added a README module. Nils Anders Danielsson **20110706094825 Ignore-this: b5165e0e2071fbad0cbca3ae2413484a ] hash: 0000005744-0303b49763f28d1b6658ed8c0ded48c99d9cf43e02159364581e5cf404ad7673 [Kripke model: Tried working with values paired up with syntactic types. Nils Anders Danielsson **20110706094913 Ignore-this: 417b73748a5c966e92db2c34494cafbf + These values are "term-like". + The module is still unfinished. ] hash: 0000010854-aa7d5aad14ece48ee7dccd6635fc669d9eda4a0b907c9a5e8e8414aa1efacbd4 [Switched to indexed universes. Nils Anders Danielsson **20110706153540 Ignore-this: b4487c469487437d1f2cb873c26944f4 ] hash: 0000042299-5cd253ab399561bb0895be53d063e91267fc8a2d3dfc2711be1126ac7bf6536a [Renamed ++-assoc to ++-++. Nils Anders Danielsson **20110818132321 Ignore-this: 3add9084fd0e2515eaf4ccedb15ea62d ] hash: 0000002770-b0b3940fc2b2694d131937aed6228c8f46f1b9cccf708b2fb797aa977637866e [Completed the switch to indexed universes. Nils Anders Danielsson **20110818132756 Ignore-this: d5b06e52a236710dcf84e7ae52466701 ] hash: 0000004966-2e6ef8ded80cc335f5794922f961980c5dfe46352883c28680cf6d2827bed1ab [Added weaken⁺ and wk-subst⁺. Nils Anders Danielsson **20110818132846 Ignore-this: 78c027e6be846b8fffbdb650f1c23597 ] hash: 0000002664-a003632ea611e810d413f98bd5fba6652cd9a78db1f472866c1c61185d709912 [Added _/̂I_ and _≅-IType_. Nils Anders Danielsson **20110818132946 Ignore-this: ab69ecdc606d73d874ae409784d0b0dd ] hash: 0000001626-020796d0c3c33e7072d0529ec3bca2cfe774d1ca2799b379d4b5a8cb0ca37aa5 [Switched to unannotated lambdas. Nils Anders Danielsson **20110818205659 Ignore-this: 16261bd75d4c8f6031928fca163c56ae + This seems to have made the Kripke model much easier to work with. ] hash: 0000050588-abcabab09fc5eaf0a28b3a2da1c9b0e0990ff0978f9b5eed458a1d470d8e6c68 [Defined U recursively instead of as an inductive-recursive family. Nils Anders Danielsson **20110818210044 Ignore-this: f9cf5d0cb9910e433fe3a58b0bf19259 + As a consequence a property which was previously proved using the assumption of extensionality now holds by definition. ] hash: 0000018523-f18342ffede2f75661b455702bf9a9d087879bd5a131b08a86a2b4cd51e54f4e [The "model" functions are now required to be "well-behaved". Nils Anders Danielsson **20110819140306 Ignore-this: 618849b21a4bb39c6c92076956e5ab63 + Using this information I could finish the proof of eval-lemma. (Some of its dependencies are still unfinished.) ] hash: 0000018194-19ca60d8780a989aa7781225e398a695a9c526ce3afdea9176a5878c92343ea7 [Made ˢ-cong take two equality arguments instead of three. Nils Anders Danielsson **20110819151219 Ignore-this: e8611f08be17f2dfb4708f0f3c16fef4 + By using spines and projections to simplify the types of f₁ and f₂. ] hash: 0000003976-ecc9b7cfbe018499bd404f25e85e6a2748642b1bffe145ac730632ec5b3febcd [Changed the type of _·_. Nils Anders Danielsson **20110819152218 Ignore-this: 8f27ea36be3d85fb6f4f67c7277c09b9 ] hash: 0000010342-8fe33f1871835fa70dd3dbd60c010535a643fcd5331c53fac75f7f7c562876bb [Removed some old experiments. Nils Anders Danielsson **20110819152813 Ignore-this: c34331164da2c514cd469dfecb17713c ] hash: 0000016016-799851339aad8e69335743185c2c57b8146608e55d7ae4dfbb76433e8fa604dc [Added _/I_. Nils Anders Danielsson **20110819200051 Ignore-this: c5c0bb9a365ade6d9b990887119b8e4f ] hash: 0000002754-e96e199b6f51143aa2fa621b939f748a503ab80b1e5a10618235d914b18b8cb9 [Renamed _++⁺_ to _⁺++⁺_ and _++_ to _++⁺_. Nils Anders Danielsson **20110819201330 Ignore-this: c16b07bd31b072d2a082b4463778b144 ] hash: 0000020312-d520ec1e714d33415949ff9375bc849d1ad24d9fb4a21b9d9bfa241807b8b4e0 [Added Renaming.≅-∋-⇒-≅-⊢ and Renaming.≅-⊢-⇒-≅-∋. Nils Anders Danielsson **20110822090341 Ignore-this: 33f910413a8c8c03bf3c50708de07c2 ] hash: 0000000713-be7885914389dbb7e53a34647745bf977c1f8e61fa2e136691e662d225e85d55 [Moved _⊢_type out of the mutual definition of _⊢_ and ⟦_⟧. Nils Anders Danielsson **20110822095158 Ignore-this: 999fbaaba697561990f5af9e6612ef6c ] hash: 0000002473-831cfa06201c9f6eb7e4557f2191a72e5a5a4cb0bc4c6a04da159b4611cfe541 [Added cons-based context extensions (Ctxt₊). Nils Anders Danielsson **20110822113943 Ignore-this: 1d73f4853056f73c4fad177f3dd6ec15 + Proved that Ctxt⁺ and Ctxt₊ are isomorphic. + A number of definitions are now duplicated: one variant for Ctxt⁺ and one for Ctxt₊. It turned out that defining the Ctxt₊ variant of wk⁺ (called wk₊) was not awkward after all (once I knew how to do it). + Rearranged some modules. ] hash: 0000067715-c54fbc38c1b7c77641c6786d76e8d6a51499c6f01492087940b911be4d5d1f8a [Changed the definitions of wk-subst⁺ and wk-subst₊. Nils Anders Danielsson **20110822113951 Ignore-this: 4ce3b4346352c9c113347384a7aba92b + The new definitions should be equivalent, but in my opinion the definitional equalities induced by these definitions are more useful. With the new definitions I do not need to prove things like wk-subst₊ (σ ◅ Δ₊) ρ ≅-⇨ wk-subst₊ Δ₊ (wk-subst ρ). + Removed weaken⁺ and weaken₊. ] hash: 0000007927-b839353735a1a39d2ca7f8ac9d41e153d1dd742ededbbed9d4c31179fbeccf5a [Added some lemmas related to wk[⁺₊] and wk-subst[⁺₊]. Nils Anders Danielsson **20110822113951 Ignore-this: 8cd856e13ff447413cb6b277594dbc5a ] hash: 0000011365-11d92df7e1dfd096643fdd29b7d551d1a951d13dc6223c945a1ef250fc70a1e7 [Defined V̌alue using Ctxt₊ instead of Ctxt⁺, finished weakening. Nils Anders Danielsson **20110822113952 Ignore-this: b6df8cea4c81183e97e4a70f8506bf0c + The switch from Ctxt⁺ to Ctxt₊ meant that weakening was much easier to define for me: the new definition does not introduce any new casts. + Now the normaliser is finished, along with its soundness proof. (The definition uses the assumption that propositional equality of functions is extensional.) ] hash: 0000030729-73179bec4cbafe2b4d808ca2f6d9cd22dae7c8908a3ddd5c8bf34dd5389c4cf7 [Renamed some modules, removed an empty module. Nils Anders Danielsson **20110822113952 Ignore-this: 5c165dae8eaac18e42796e6bdd4ac79 ] hash: 0000006138-77c7aba6ada6994ed19d14e8263df52bddba31db3739bdc3d59284db116f0488 [Modified some comments. Nils Anders Danielsson **20110823145247 Ignore-this: 51c78b07b41052822428519868bded34 ] hash: 0000000929-3995bca70b8dbafc77c70ea0fe3140b0072fbdc8daab00051889ba13689e7956 [Added a fixity declaration. Nils Anders Danielsson **20110823220627 Ignore-this: 3daed7d954f8f59fe2ee2850b8272825 ] hash: 0000000267-f5ad75a6b1b70b7d41441c5fcb0f41b911bd1fd1da2043907c3cbdb89943f397 [Added Type-π and IType-π. Nils Anders Danielsson **20110824083509 Ignore-this: 93e01d6705148daabd1432301f61c396 ] hash: 0000005064-f2adf77692aaee6d98921405cc40f0f37e18258c6ab57559cf68de04f03b867f [Workaround for Agda regression. Nils Anders Danielsson **20110824090805 Ignore-this: 9a9150f677a94e7b5bf9f5082624cfb4 ] hash: 0000000354-506ef5faaf919338fd55f2bcead8c96710656e512eb1ecd48696f7a612f4eed4 [Proved that there are no closed terms of "atomic" type. Nils Anders Danielsson **20110824095221 Ignore-this: 24ffdf23aac7920b0f924326c700d731 + Assuming extensionality. ] hash: 0000004617-186d0f3dc48a03ecf230199af00766c33afd4c61595df4f0304e382737cae21e [Added a comment. Nils Anders Danielsson **20110824135826 Ignore-this: b46ed717fdb455989fae0035a0bca0ad ] hash: 0000000582-0364b2055133e414eefc98dd197f9a4e25ab079aef06c64ecfef87ffbb306531 [Cosmetic change. Nils Anders Danielsson **20110825074955 Ignore-this: 7ae6ab2c78faa9a6fbdd320d7ec809d7 ] hash: 0000000419-6553c1ff92129c96b12e4d6ac54393ddbbdde48c7f0fab8ce5267e3f30cd157f [Added (i)fst-cong and (i)snd-cong. Nils Anders Danielsson **20110825075014 Ignore-this: fdac661d1a08f5e9a9776830c9b30b3c ] hash: 0000001301-5f3358715f0f8b5f7ac10654892a55b501227e5e29ff27b7c86bc94c3e05cb45 [Removed workaround for Agda regression. Nils Anders Danielsson **20110825135242 Ignore-this: 67cfd0e25a5da86491816cd32292d3f8 ] hash: 0000000362-f92e7e531d2c25e3b03c6477930d6e992fbdf3c0e2e942809c7c7f33f78442a3 [Updated code to reflect changes to Agda. Nils Anders Danielsson **20110827170616 Ignore-this: 182dd06ca18c7dd650efe296ea606e61 ] hash: 0000005098-c40a0887138b2b14f6658bcd2587757d5616a0b483e7772d773f4a1af3e808ab [Added ⟦̌_∣_⟧-π. Nils Anders Danielsson **20110827224316 Ignore-this: 88227e450b36b197c19d0e10af84ac01 ] hash: 0000006269-e4512eb324614a1baa0d8d678a2f1cb6ef3b737e010164efc511a2939afdf1e1 [Added indexed-type-cong and /I-cong. Nils Anders Danielsson **20110829085741 Ignore-this: bf68099a2175a7eda49ca68406e8cb4 ] hash: 0000001266-f4e6c9295e179fed72533fa44909150da4718d902e0eccf916d58e2c3e78cac9 [Added uncurry-cong. Nils Anders Danielsson **20110829085752 Ignore-this: 2e873fc98fc89ee331a50173283fc0 ] hash: 0000000520-39b40209c4854e7c3c7b9f03660d972fa5df985ff172dc9c78b9578e73d6cb42 [Cosmetic change. Nils Anders Danielsson **20110829091201 Ignore-this: f074298457d00656f239f2103350b9f0 ] hash: 0000001117-08ff10ce40533c8f0747dd080ef0116d939a72e4b2f91627c39c1fb093eca063 [Modified a comment. Nils Anders Danielsson **20110829111646 Ignore-this: c49dedda858783e05a7eb92a20800c0f ] hash: 0000000322-ae65a992ab214c3946f9a7364306a5b8d0b2c0ee7554667e4ab86a2719701c5d [Proved that normal forms are not unique (given some assumptions). Nils Anders Danielsson **20110829122652 Ignore-this: 899e07ca2c529c17a1d1aa6ca47c0592 ] hash: 0000003737-1cfec9c6eeec59456374121525ad6ae216798f2f54ec361f0edf31cfdc0259f1 [Modified a comment. Nils Anders Danielsson **20110829210824 Ignore-this: 847233dfa0f2365b43e66255fc20784b ] hash: 0000000275-d304766ff2fc5b9e00a40281ec96d683f836fb083ee7fccb78bf441b6caa271f [Proved that equality of variables is decidable. Nils Anders Danielsson **20110830115000 Ignore-this: 67fdf8e106187139c00770ad94e34ea8 ] hash: 0000001051-17ce46cf8368932c25d817bc21b23f50391a668354699ab4df4af5c559483b72 [Syntactic contexts. Nils Anders Danielsson **20110830115226 Ignore-this: c9c9525031dbb6a21235943bccbb2ca7 ] hash: 0000000507-254ba7dbb559e1a2542c3277efac2f095de2cf617179fd7fb6c5683938a5f953 [Raw terms. Nils Anders Danielsson **20110830115512 Ignore-this: a6806abaf8946dc1d71a303465202bc6 + Incomplete definition distinguishing between "checkable" and "inferrable" terms. About to be changed. ] hash: 0000002565-65830bca0100a1e3162b60d91bce5f6789e0acc0fdbde029750cb2c63031eb6c [Changed the definition of raw terms. Nils Anders Danielsson **20110830115518 Ignore-this: 49c0813127338594c3715d25139dac9d ] hash: 0000004315-09ca150d6db3e62a8de50b0a2fbe0207e0a5dda30c04f7268cd8ceeba792588a [Implemented a (sound) type-checker. Nils Anders Danielsson **20110830130041 Ignore-this: a0609bc91472877dd051a1cf88a9befb ] hash: 0000014518-56d5fddde05990b1fb9233e13643c5842e2b3a0e5d25f5a2765ff05386e8c2e5 [Minor rearrangement. Nils Anders Danielsson **20110830144518 Ignore-this: cfeabc1d847a5bba0e9fb539076e4efb ] hash: 0000000308-92e1ede0feba9f9530ca3a4805dde16b93e2a6faa4ee91f38b1a7569664cabcf [Made some implicit arguments explicit. Nils Anders Danielsson **20110830145119 Ignore-this: 7b912ac1d46db7d5cab2e1b647707bcf ] hash: 0000004811-567e17374d5ce1ab248c821fd481cbbf7adf5fceaa36fbe89798141129aa0026 [Removed a comment. Nils Anders Danielsson **20110830145202 Ignore-this: 50979e26f5565eabfaae8b4de850e886 ] hash: 0000000302-a6084e307b7428715c05a1d378516bb1a5f29c5ea268102c120ecf477b771606 [Added a comment. Nils Anders Danielsson **20110905090426 Ignore-this: 64b73382d672412924735520d7125e3e ] hash: 0000000270-3311900f2d1db8e31f69077492a87f9a4d7134b4571858097bc659c1f379254a [An inductive definition of beta-eta-equality. Nils Anders Danielsson **20110830144411 Ignore-this: bbaa0a693e65eedb66d40723920d658c + Along with a soundness proof. ] hash: 0000004883-32ab2111a69d0cd38eb05d79e97fae17c8d9a6970bd28b0317cad6a6d1a4dce0 [Updated code to reflect changes to Agda. Nils Anders Danielsson **20110915122331 Ignore-this: 13ac81d1dffee712f38d26532a6c9bdd ] hash: 0000003399-629c38c092a667fe475b8bcb45245e089fc22af85ba947fd2a2ae482cd055193 [Added README.DependentlyTyped.Extensional-type-theory. Nils Anders Danielsson **20110915140239 Ignore-this: ddadc598570bbe02a9715cc37a58e8b9 ] hash: 0000004474-3784056e866053aab7934e33b76bd8c47b6090d3d1ebc3082093afb52ae291e0