1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
|
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.
]
|