Context: [additional facts about limits on cuts robdockins@fastmail.fm**20140818025955 Ignore-this: 6f9c952db425df6ae9d2a14139a8a3d1 ] [work on limits robdockins@fastmail.fm**20140817221707 Ignore-this: 9811e0cd669b48f3beb7a56d47cbe3c3 ] [finish proving that Q field ops commute with injq robdockins@fastmail.fm**20140817060600 Ignore-this: a1f6c62b39983e6f6f01d28aca5f8534 ] [split up realdom.v and perform associated code motion robdockins@fastmail.fm**20140817030034 Ignore-this: 24c74cd459d2ab15dcd3d83ba06f7081 ] [recip is canonical and converges robdockins@fastmail.fm**20140725211947 Ignore-this: c100dbd94114cca9576b2a3f46c9ddc7 ] [improve the proof that 1 is a unit for multiplication robdockins@fastmail.fm**20140724150124 Ignore-this: c5ec976f8a9858a7ba1f704b4e84d02e ] [complete proof the interval multiplication converges; other minor stuff robdockins@fastmail.fm**20140724015132 Ignore-this: bc717baa4c8f9ec31b821c5cfae5b499 ] [further progress in realdom.v robdockins@fastmail.fm**20140723004023 Ignore-this: f33e18d22ae69c9b6209e28151d18017 ] [unmessify rational_intervals patch robdockins@fastmail.fm**20140721123718 Ignore-this: 4a125b192a9964a508a1063845e9f160 ] [messy updates to rational_intervals.v robdockins@fastmail.fm**20140721015810 Ignore-this: 858dac9c55426167c6f397a71ef3fda5 ] [implicit arguments for "fixes" robdockins@fastmail.fm**20140721015739 Ignore-this: 229ecdd48265fc855319141e399bc522 ] [metadata robdockins@fastmail.fm**20140714201441 Ignore-this: aa16faaf09c1c404bdc6eaf0d0c39912 ] [further beautification robdockins@fastmail.fm**20140714200516 Ignore-this: 47d74c51d9fe130a5ac12706b1ddb1d4 ] [start working on the recripricol function robdockins@fastmail.fm**20140714180055 Ignore-this: c7f93cea17f46daa78a1ea14e86dfcaf ] [tweaks to the lambda models robdockins@fastmail.fm**20140714180031 Ignore-this: 219788fe70f42f0f6e60176cab464f19 ] [beauty edits in st_lam* robdockins@fastmail.fm**20140714180006 Ignore-this: a40aa7ae00ed27595ee04073918bd028 ] [move stuff to rational_intervals.v / define real_mult and prove some properties robdockins@fastmail.fm**20140712053232 Ignore-this: 398c5c03aac9ff37526d4d7c9e1a82c0 ] [finish correctness proof for interval multiplication robdockins@fastmail.fm**20140711191547 Ignore-this: c9ab138a0ca43fe0b133b208419bbcc4 ] [break out facts about rational intervals robdockins@fastmail.fm**20140711012320 Ignore-this: b7fe6e9377629a89b5debe3019ae1aa ] [updates to ideal completion robdockins@fastmail.fm**20140707053800 Ignore-this: 90d1efbd0e5833d8c83f0df056d7a74c ] [a pile of additional properties in realdom.v robdockins@fastmail.fm**20140707053519 Ignore-this: 7edba1e72a1856f297ef11e698ed989f ] [some properties of converging prereals robdockins@fastmail.fm**20140706041401 Ignore-this: 273bfbb245302becd7ff402831827ffb ] [make realdom compile robdockins@fastmail.fm**20140630015439 Ignore-this: 8bfc8eaeed4a1596450b0bb9ddef9aaa ] [renaming robdockins@fastmail.fm**20140630011639 Ignore-this: a287e083af095790cbf2b48df7a58739 ] [reorganize some code robdockins@fastmail.fm**20140630011446 Ignore-this: f1375b9e7ad822cb92f0c83d4001eddd ] [build the retract for realdom robdockins@fastmail.fm**20140630001245 Ignore-this: 4eb9da621588417d1b7b2fc980c7bf70 ] [fill out lemmas about cPLT robdockins@fastmail.fm**20140630001140 Ignore-this: add9e45c14621e3d6328684098bf8461 ] [more facts about cPLT robdockins@fastmail.fm**20140628073731 Ignore-this: 101a131ed114902924a1707eff7ebc70 ] [continuous domains as retracts of bifinite domains robdockins@fastmail.fm**20140628035522 Ignore-this: 5e7c61d49cf8424412b0d94f5fcb5ee6 ] [start implementing arithmetic operations in RealDom robdockins@fastmail.fm**20140620003249 Ignore-this: c28479b8a933cba263765bdddb112264 ] [define the domain of rational intervals robdockins@fastmail.fm**20140619040809 Ignore-this: 6cbe1a9cc690e5a9d77f37ee299154b this domain is useful for describing the semantics of exact real arithmetic. ] [show that every effective CUSL is Plotkin robdockins@fastmail.fm**20140619034433 Ignore-this: d529a4b1d6d698f79572caa805072394 ] [fix notation for octothorpe robdockins@fastmail.fm**20140614222130 Ignore-this: 3dc815825f11ceaf4f4f53e4668e6382 ] [fix for coq 8.4pl4 robdockins@fastmail.fm**20140614222049 Ignore-this: 9745904845aaf54e5569df982fc93d65 ] [move swelling lemma into finsets robdockins@fastmail.fm**20140504080535 Ignore-this: ffa560e9aa4e4f8b15a55c1f9b1da72e ] [documentation improvements and code motion robdockins@fastmail.fm**20140504070008 Ignore-this: da7847f82403990342732a8ce226315c ] [replace the old finprod robdockins@fastmail.fm**20140504005534 Ignore-this: 606cf44422f68d66c8d2d90049e67b93 ] [remove the old finprod robdockins@fastmail.fm**20140504005137 Ignore-this: 38bd54e16c87d27bbede08496c37bfba ] [update st_lam_fix to use the new finprod robdockins@fastmail.fm**20140504003627 Ignore-this: 95d0a66e99ccead89bdfef09a1c8c109 ] [update st_lam to use the new termmodel robdockins@fastmail.fm**20140503230854 Ignore-this: c3d6b2155674b414c5c2e14b85b13760 ] [new version of finprod with a better term model robdockins@fastmail.fm**20140503222035 Ignore-this: db63e3a063bdb6f2f579644c7b63bd1b ] [a few more (hopefully final) lemmas about union robdockins@fastmail.fm**20140422223924 Ignore-this: 7b95c75abef9b0d45863b5e33d1c5a37 ] [finish proofs about union robdockins@fastmail.fm**20140422065034 Ignore-this: 2929c3cdb013c028a48022b0293b2f18 ] [powerdomain progress robdockins@fastmail.fm**20140421064325 Ignore-this: 592f9c6046f05a27897b460edb2efe10 Show that powerdomains are endofunctors on PLT. Further, they are monads with the 'singleton' and 'join' operations. Also make some progress on the additive portion of the theory, dealing with emptyset and union. ] [tweak makefile robdockins@fastmail.fm**20140420031337 Ignore-this: d5954b26f731bfed3d79cefacab322fb ] [show that semvalue is the weakest condition allowing beta-reduction of strict functions robdockins@fastmail.fm**20140420020447 Ignore-this: 16a7ed23f04879f1fb324bdac8a2ffaf ] [some additional operations relating to the PLT adjunction robdockins@fastmail.fm**20140420020351 Ignore-this: db8eec6e3f74cce3acb67d2b660b104e ] [finish building power domain fmap robdockins@fastmail.fm**20140420020217 Ignore-this: 556e1cb87576de36cb26f8add3a1b163 ] [fix up st_lam.v robdockins@fastmail.fm**20140329015058 Ignore-this: 1c31d674b759fbd0cc74fb3125579f96 ] [push some proofs into finprod robdockins@fastmail.fm**20140329000401 Ignore-this: 49070fdd951e49473e60d3cd0ec431c6 ] [documentation and aesthetic changeds robdockins@fastmail.fm**20140327043141 Ignore-this: be27b24b78ea6af722a307117e59f5b3 ] [finish the st_lam_fix example robdockins@fastmail.fm**20140322011153 Ignore-this: e702f564b6eab2f8c11ab16bcb62504b ] [clarafications re: countable choice; remove unfinished example from build order robdockins@fastmail.fm**20140321212852 Ignore-this: 2a9d5c79c05ba088e1815feab99a5f6c ] [break the "fixes" operator into a separate file and prove some facts about it robdockins@fastmail.fm**20140318013247 Ignore-this: 80c506cef0719a974a049a1f5870f676 ] [minor fix to skiy.v robdockins@fastmail.fm**20140317054057 Ignore-this: ffef6fcaf5fa7f8cea80d2808caf4f4c ] [add the fixpoint operator; admit proofs robdockins@fastmail.fm**20140317044648 Ignore-this: 97ca18e980cdf46a9b40c8252badef14 ] [remove the evaluation case for variables robdockins@fastmail.fm**20140317032932 Ignore-this: e46d634e735e5b21a18518a48777168d ] [start on STLC with fixpoints -- but without fixpoints for now robdockins@fastmail.fm**20140317031953 Ignore-this: 3458bc18c73d967bef58418bc73e06cb ] [add the eliminator for booleans to st_lam; other additional utility lemmas robdockins@fastmail.fm**20140317031753 Ignore-this: 369dd375755cbd9ae5e3c969f3ef6ec ] [some minor code motion robdockins@fastmail.fm**20140228064927 Ignore-this: 804828472ddb0c5fafc72460fce8387b ] [plug final holes in st_lam and add to build order robdockins@fastmail.fm**20140228044729 Ignore-this: 3edc7f36bfa97775ba33ffa27c80df59 ] [reduce st_lam.v to facts I believe about fresh variables robdockins@fastmail.fm**20140228010832 Ignore-this: bde3e73291ddd32337d6fb999e4b1c02 ] [fix breakages robdockins@fastmail.fm**20140226073930 Ignore-this: 9be54f5255f8ed9d53a79260e9bdf565 ] [more work on lambdas robdockins@fastmail.fm**20140226043753 Ignore-this: 7f7452670221e2643067a3c7cc180998 ] [use new finprod implementation robdockins@fastmail.fm**20140226043700 Ignore-this: c9e05df5fcfd31254ed7318fe693490c ] [remove old finprod robdockins@fastmail.fm**20140226043642 Ignore-this: 2705703a2c782da21a152fbb27c8a972 ] [rearrange the interfact to finprod robdockins@fastmail.fm**20140226043541 Ignore-this: c44d7c478948f42b188eb8d06469abbf ] [fill remaining holes in finprod2 robdockins@fastmail.fm**20140225205242 Ignore-this: 1eeb9b8beef92790c28918292f2a9cf4 ] [rework some stuff dealing with semidecidable predicates robdockins@fastmail.fm**20140225092149 Ignore-this: 32b5ccb2927e08979ea92b9ef67c40f4 ] [lots of work on alpha-congrunce in lambdas robdockins@fastmail.fm**20140225035601 Ignore-this: fbbec9dac4cb328ff4e0b25df646e0c7 ] [terminate is universal in PLT robdockins@fastmail.fm**20140225035538 Ignore-this: abc6cd1a60578c435bf9ca596d8d0922 ] [new attack on nominal finite products robdockins@fastmail.fm**20140225035516 Ignore-this: 3875e713acc6aa5193696612f3ede76d ] [push forward a little on lambdas robdockins@fastmail.fm**20140221095249 Ignore-this: c690a1b03075702e3fd84aac7e268211 ] [update finprod for various changes robdockins@fastmail.fm**20140221095230 Ignore-this: a6d787930ed356ae2b0a003af1f4d44 ] [better discrete cases lemma robdockins@fastmail.fm**20140219051301 Ignore-this: f0ec88e8207257e7657ced933cf687e7 ] [start working on simply-typed lambdas robdockins@fastmail.fm**20140219051238 Ignore-this: 69bea345376ea39cd1addc0849a43077 ] [more messing about with advanced category theory stuff robdockins@fastmail.fm**20140211095003 Ignore-this: 9cd3c9d961349e8797f109f716c5f678 ] [minor rearrangements and code motion robdockins@fastmail.fm**20140211041724 Ignore-this: 642ad6f1395fde7ecd81e5a905fd5428 ] [some basic bicategory theory robdockins@fastmail.fm**20140210083634 Ignore-this: f47a898fa045a397d3ee70e1512b8baa ] [even more notation futzing robdockins@fastmail.fm**20140209072416 Ignore-this: d2061652cb3e80f6994f567a9e677b32 ] [additional notational futzing robdockins@fastmail.fm**20140209043308 Ignore-this: ac42cbbc94df227e6d5e70b96ae65fd3 ] [futz around with notations, various other cleanup activities robdockins@fastmail.fm**20140209005551 Ignore-this: 3f41a52650aadd956ac490b62e59c1c3 ] [complete adequacy for SKI+Y robdockins@fastmail.fm**20140206050414 Ignore-this: f730587ac7a42f3e35740976a1439f2e ] [minor changes in cpo robdockins@fastmail.fm**20140206014745 Ignore-this: 95244704faf1e6c336d62dc7912f9022 ] [push through most of SKI+Y adequacy robdockins@fastmail.fm**20140205214805 Ignore-this: dc998ef45f2e919e9373bfa21a5ef8c7 ] [major simplification of the adequacy proof for SKI robdockins@fastmail.fm**20140205185605 Ignore-this: f1f0dc46274db05f3393038dfe2775e2 ] [push forward on SKI+Y robdockins@fastmail.fm**20140205044216 Ignore-this: daf255aa940b42c1c68ba947a356370d ] [continue futzing with the LR statement robdockins@fastmail.fm**20140203055601 Ignore-this: f5ef9f06d3b1a11d76317b52cec691ab ] [start pushing on adequacy for SKI+Y robdockins@fastmail.fm**20140202085948 Ignore-this: 956844809340fad0c13c19e9fa729b5c ] [mostly finish soundness for SKI+Y robdockins@fastmail.fm**20140202060633 Ignore-this: 4c75fd9eeefa1d6dad6866662abea0fd ] [start working on a CCL example robdockins@fastmail.fm**20140202020748 Ignore-this: 44c5d7854cc19b0f90414c2be6b3df68 ] [make id(A) a parsing-only notation robdockins@fastmail.fm**20140202020724 Ignore-this: 68f51f754c0b89e2e815da47b901e4b1 ] [the PLT adjunction is strong monodial robdockins@fastmail.fm**20140202020637 Ignore-this: 7b29b9a6a5e8efa07440c528ec12d7bd ] [fix my broken version of lfp and fixup proofs robdockins@fastmail.fm**20140202020615 Ignore-this: 3ac283481318622cbf38378e815a4f09 ] [more work on SKI + Y robdockins@fastmail.fm**20140202020516 Ignore-this: d1f63e2ef610c6f93d03806c5426cfa5 ] [start work on SKI + Y robdockins@fastmail.fm**20140201085039 Ignore-this: fb7a405830cf90526cddd8ce37f4da40 ] [doc corrections robdockins@fastmail.fm**20140130015908 Ignore-this: bca4c04267bfdac8cb202651a0960d92 ] [lots of additional inline documentation robdockins@fastmail.fm**20140129234834 Ignore-this: ab2c59add5514f44a898de1f0eece98b ] [powerdomains form continuous functors in EMBED robdockins@fastmail.fm**20140126234115 Ignore-this: d2ee08902f0bdb52efd7f7ce2c594469 ] [complete the powerdomain constructions; build some operations robdockins@fastmail.fm**20140125225202 Ignore-this: 9c8f2632df05e84fc3794a338ff8720d ] [construct the basic powerdomains--still some holes left robdockins@fastmail.fm**20140125064541 Ignore-this: c3206d2e1e925096b3e9ff49afacef2f ] [generalize the lfp construction to a generic chain_sup operation robdockins@fastmail.fm**20140124183103 Ignore-this: 4cc2c1011b9f79365dcb7c76784fbfa6 ] [update makefile robdockins@fastmail.fm**20140124073734 Ignore-this: a0b7db8383262caa314c21b99e146222 ] [new file for recursive lambda domains robdockins@fastmail.fm**20140124070023 Ignore-this: 300c02b4da83b6ebd734aa2ccb21cd2d ] [more lemmas about antistrict homs robdockins@fastmail.fm**20140124065953 Ignore-this: 483c7b350dc3cab59c8ff50e1ac73b8c ] [fix breakage related to implicit arguments robdockins@fastmail.fm**20140124065805 Ignore-this: 561693d3280851299c6a49a2a34546b3 ] [notation tweaks in cpo.v robdockins@fastmail.fm**20140124053800 Ignore-this: 83e92d8c14568448074a940ceafbe2c9 ] [add if/then/else to the SKI system robdockins@fastmail.fm**20140124023630 Ignore-this: 37a9737932a05393a6338380226ca346 ] [case analysis for finite types robdockins@fastmail.fm**20140124012505 Ignore-this: 6ec1076b2a74f5832501a105a28a6dba ] [finish adequacy proof for SKI robdockins@fastmail.fm**20140123211322 Ignore-this: 1fe3e626e33431c27e2aa186b3bf91d2 ] [additional lemmas about domains robdockins@fastmail.fm**20140123090037 Ignore-this: fcad2dd816f805b8b5e7d1be3df60db8 ] [most of a proof of adequacy for SKI robdockins@fastmail.fm**20140123085839 Ignore-this: d1595c02a6387297018e7f316a3e751 ] [more work on finite products robdockins@fastmail.fm**20140121061158 Ignore-this: c2f8212e041478104dd4c81c225b42d5 ] [begin work on a more flexible "finprod" domain robdockins@fastmail.fm**20140119021653 Ignore-this: 249718a2c31964733171b21c84d2effb ] [mess with implicit arguments in categories.v robdockins@fastmail.fm**20140113041450 Ignore-this: 314cad9207f706e949bd686aaa5c5e1b ] [products for CPO, uniformity of lfp robdockins@fastmail.fm**20140113041421 Ignore-this: e533abe995e634c732a35e71d66ddb6a ] [define the LFP in pointed CPOs, prove the Scott induction principle robdockins@fastmail.fm**20140112231843 Ignore-this: 2014174b1c6914bef376d614f34d073f ] [build the forgetful functor from EMBED to PLT robdockins@fastmail.fm**20140110014909 Ignore-this: 1dacbfc0383e48f4ab35fe0a5fd11cec ] [notation changes, prove sum_cases and curry preserve order and equality robdockins@fastmail.fm**20140110014820 Ignore-this: d1c6a1d0346a9eba14f3529ac30b5e2f ] [prove addl facts about pairs, tweak implicit arguments robdockins@fastmail.fm**20140110010319 Ignore-this: 9f0af8abc268b2b22d8b5450d6a4136 ] [make 'ob' a coercion robdockins@fastmail.fm**20140110010204 Ignore-this: 467c0b0a8b086a7f44bf98875a4380d6 ] [copyright notices robdockins@fastmail.fm**20140106232333 Ignore-this: f59bafa0ec99e259bd9b4319f2cdbc67 ] [add ord_dec coercion robdockins@fastmail.fm**20140104052750 Ignore-this: 4ed1cacfd27979f0fe518862be5ac27c ] [define the model for CBV lambda calculus robdockins@fastmail.fm**20140104050626 Ignore-this: 88ca796d4697bfebb044d3fae27d6129 ] [proof a fixpoint lemma for unpointed domains robdockins@fastmail.fm**20140103231818 Ignore-this: 4939eb02d09b6a4eecf145c887c64393 ] [prove that the adjoint functors between PLT and PPLT extend to continuous functors in EMBED robdockins@fastmail.fm**20140103000915 Ignore-this: 54da0101f581731ebe512ed514e0603e ] [notation changes for PLT robdockins@fastmail.fm**20140102234446 Ignore-this: ad1f82f22d1bf0e057f11c3508a81716 ] [move embeddings into their own file; pull TPLT and PPLT into profinite.v robdockins@fastmail.fm**20140102234424 Ignore-this: 3704996af47ae32415ba3e539d67cf5c ] [Show that PLT is cocartesian; rearrange proof that EMBED(true) is terminated robdockins@fastmail.fm**20140102213805 Ignore-this: 3470df6910e7a3e4bda478c0c6ecea62 ] [remove unnecessary "inh" hypothesis in the definition of Plotkin order; fixup the fallout robdockins@fastmail.fm**20140102213646 Ignore-this: b6a5ad59296f938b377d71852120d48b ] [move proofs that empty and unit preorders are effective plotkin robdockins@fastmail.fm**20140102205530 Ignore-this: 7324843510fd938d356aa82003c9ec68 ] [make epi/mono/iso morphisms into categories robdockins@fastmail.fm**20131228082442 Ignore-this: ee75a2b6eb1f3d6fa47f17d6734e5015 ] [define the cocartesian and distributive categories robdockins@fastmail.fm**20131226001612 Ignore-this: 11e9d8a88bef42bcb800b31d85d28d16 ] [remove uses of maximally implict arguments robdockins@fastmail.fm**20131226001536 Ignore-this: c0d93a5398aea58cbcc4fbbca3b59b17 ] [fixpoints and binary sums for NOMINAL robdockins@fastmail.fm**20131121092931 Ignore-this: 8a660dfe2ab16a8208ae559dcf2b7ed0 ] [modify bilimit.v to use the general construction from cont_functors.v robdockins@fastmail.fm**20131120075848 Ignore-this: 17ea36107ade1646eab5c99aec3561a9 ] [generic fixpoint construction for categories with initial objects and directed colimits robdockins@fastmail.fm**20131119092522 Ignore-this: 25674dff855a1cecdb4ee919f8bf3a5d ] [remove some irritating unit parameters, fix doc typos robdockins@fastmail.fm**20131118093204 Ignore-this: 38342d58567d8a13471620d5b7c2b7d4 ] [improvements to categories; complete some constructions in nominal robdockins@fastmail.fm**20131118085737 Ignore-this: e58cb49a01d0210dabdb021250910adb ] [build fixes robdockins@fastmail.fm**20131113004305 Ignore-this: 5abffcd1d6b44f816749c5e0cfd5b6e9 ] [Documentation additions robdockins@fastmail.fm**20131113004254 Ignore-this: 79a913d3a8652866f3fdc64891f6304d ] [lots of inline documentation additions robdockins@fastmail.fm**20131112192736 Ignore-this: 6aa38112c10ceed3bf43e35dbda98312 ] [update makefiles robdockins@fastmail.fm**20131112192706 Ignore-this: d834beaa532cdf994cfa0a0b5a562e4f ] [continuous functors for binary sum and products robdockins@fastmail.fm**20131112192605 Ignore-this: 61520e6e315df909465a02f854816366 ] [add the category of nominal types robdockins@fastmail.fm**20131112192520 Ignore-this: f0351c5eb0bdacdfe192a6863d9c0bc6 ] [split the proof that expF is a continuous functor into a separate file; rearrange some defintions robdockins@fastmail.fm**20130924013328 Ignore-this: 4eacee37bb6474d1bdfffe416b98b4c1 ] [rearrange definitions of continuous functors. Prove enough plumbing to build the model: D = D->D robdockins@fastmail.fm**20130924002837 Ignore-this: a66f9e8833601e244048b70e8bfaab96 ] [show that the function space is a continuous functor; other junk robdockins@fastmail.fm**20130923060521 Ignore-this: d8f406450688c633ebc1fe1eb0343c91 ] [some name changes, other cosmetic fixes robdockins@fastmail.fm**20130909043234 Ignore-this: cdd24d1c96a34fb3573c1806153df9fb ] [additional cosmetic changes and rearrangements robdockins@fastmail.fm**20130909020137 Ignore-this: 77d28bc9452f6c93915194033118dab7 ] [reorganize profinite code robdockins@fastmail.fm**20130909011437 Ignore-this: 8511bf92ca6998ff8c69d5537624bdb8 ] [cosmetic changes robdockins@fastmail.fm**20130908183909 Ignore-this: e19039701e58fd26ca4eab79d7b49d14 ] [complete the bilimit construction, show how to take fixpoints of continuous functors robdockins@fastmail.fm**20130908175228 Ignore-this: 82feab8fdc0c944f13d91605c6a8e571 ] [find a MUCH easier path to a bilimit construction robdockins@fastmail.fm**20130907012151 Ignore-this: fcc72ad140b045ef37e4b03ad38a8fb0 ] [lots of progress, mostly on defining bilimits robdockins@fastmail.fm**20130905204959 Ignore-this: abf4bcf03a49fa009f9fb2200ee3abf2 ] [start working on the theory of finite preorders, which form a basis for plokin orders robdockins@fastmail.fm**20130812054451 Ignore-this: 5be36257a8fdf486bcc31f587d93c457 ] [parameterize plotkin orders, build category PPLT robdockins@fastmail.fm**20130811063623 Ignore-this: 3f273841bc72098acee0fd618627dbd5 ] [complete the details showing PLT is cartesian closed robdockins@fastmail.fm**20130809230336 Ignore-this: 13fd1b5a8172dd263cf655421f7584f7 ] [add files missed in the first import robdockins@fastmail.fm**20130809080742 Ignore-this: 6b59cce866a486d70559f7c80fe99053 ] [initial import of development robdockins@fastmail.fm**20130809080409 Ignore-this: 44cb5a0df2f1643d289f07dcd4227cbf First major steps toward a fully effective and usable formalized domain theory. We formalize the plotkin preorders and show that they form a cartesian closed category. ]