path: root/pkgs/development/coq-modules/domains/darcs_context

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.
]