| 64c8600 | Roly Perera | 05 October 2016, 21:43:13 UTC | Update README. | 05 October 2016, 21:43:13 UTC |
| 211d9e4 | Roly Perera | 05 October 2016, 21:37:16 UTC | Update README. | 05 October 2016, 21:37:16 UTC |
| cb9d850 | Roly Perera | 11 September 2016, 12:44:52 UTC | Tweak layout. | 11 September 2016, 12:44:52 UTC |
| 119bcc7 | Roly Perera | 09 September 2016, 17:11:00 UTC | Slightly cleaner proof of cofinality for │ᵥ′ case; avoids subst. | 09 September 2016, 17:11:00 UTC |
| 9aaffbe | Roly Perera | 03 August 2016, 03:49:24 UTC | WIP | 03 August 2016, 03:49:24 UTC |
| 5ee7783 | Roly Perera | 01 July 2016, 08:30:51 UTC | Reinstate (id *) in nu-sync rule. | 01 July 2016, 08:30:51 UTC |
| fb2ec60 | Roly Perera | 01 July 2016, 08:27:55 UTC | │ᵥ′ case is a bit nasty...not quite sure how this will pan out for the pentagon proof... | 01 July 2016, 08:27:55 UTC |
| 95d8f02 | Roly Perera | 01 July 2016, 08:11:48 UTC | Fixing up cofinality proof again, aargh. | 01 July 2016, 08:11:48 UTC |
| 49b21f1 | Roly Perera | 01 July 2016, 08:07:35 UTC | Reinstating (id *) in nu-sync rule. | 01 July 2016, 08:07:35 UTC |
| 0441cac | Roly Perera | 30 June 2016, 13:23:36 UTC | Move pop-swap; drop id-comm. | 30 June 2016, 13:23:36 UTC |
| c81880f | Roly Perera | 28 June 2016, 09:20:07 UTC | Renaming instance for names is just confusing, inline. | 28 June 2016, 09:20:07 UTC |
| 4b8498a | Roly Perera | 28 June 2016, 09:13:36 UTC | Renaming instance for names is just confusing, inline. | 28 June 2016, 09:13:36 UTC |
| be12d0c | Roly Perera | 28 June 2016, 09:10:52 UTC | Renaming instance for names is just confusing, inline. | 28 June 2016, 09:10:52 UTC |
| f3a7666 | Roly Perera | 12 June 2016, 06:36:11 UTC | Eliminate unnecessary 'rewrite' from cofinality proof for ᵇ│ᵥ case. | 12 June 2016, 06:36:11 UTC |
| f2b5c66 | Roly Perera | 06 June 2016, 17:13:34 UTC | Version with id renaming applied in extrusion rendezvous case. | 06 June 2016, 17:13:34 UTC |
| 98eaac4 | Roly Perera | 06 June 2016, 16:44:21 UTC | Fixing up example. | 06 June 2016, 16:44:21 UTC |
| 4eabb13 | Roly Perera | 06 June 2016, 16:40:29 UTC | Transition.Concur.Ren no longer needed (relic of two-dimensional residuals). | 06 June 2016, 16:40:29 UTC |
| f49ee6b | Roly Perera | 06 June 2016, 15:51:55 UTC | 6/7 | 06 June 2016, 15:51:55 UTC |
| 4e135fc | Roly Perera | 06 June 2016, 15:33:16 UTC | 5/7 | 06 June 2016, 15:33:16 UTC |
| fc80074 | Roly Perera | 06 June 2016, 15:26:24 UTC | 4/7 | 06 June 2016, 15:26:24 UTC |
| d988d88 | Roly Perera | 06 June 2016, 14:19:54 UTC | 3/7 | 06 June 2016, 14:19:54 UTC |
| c2abacf | Roly Perera | 06 June 2016, 14:15:10 UTC | 2/7 | 06 June 2016, 14:15:10 UTC |
| 5f1706a | Roly Perera | 06 June 2016, 14:11:17 UTC | Ok, bit better... | 06 June 2016, 14:11:17 UTC |
| d10a950 | Roly Perera | 06 June 2016, 14:09:49 UTC | Urgh, proofs get nasty because Agda doesn't understand identity or functorality... | 06 June 2016, 14:09:49 UTC |
| a509864 | Roly Perera | 06 June 2016, 13:09:37 UTC | Now 7 cofinality proof-cases to fix. | 06 June 2016, 13:09:37 UTC |
| 4d5fdfb | Roly Perera | 06 June 2016, 13:05:32 UTC | 9/9. Only needed rewrite in 2 cases. | 06 June 2016, 13:05:32 UTC |
| f81e5fe | Roly Perera | 06 June 2016, 13:01:57 UTC | 8/9. | 06 June 2016, 13:01:57 UTC |
| f4bdabd | Roly Perera | 06 June 2016, 13:00:15 UTC | 6/9. | 06 June 2016, 13:00:15 UTC |
| 5221173 | Roly Perera | 06 June 2016, 12:57:35 UTC | 5/9. | 06 June 2016, 12:57:35 UTC |
| e439dba | Roly Perera | 06 June 2016, 12:55:03 UTC | 4/9. | 06 June 2016, 12:55:03 UTC |
| 6075b6f | Roly Perera | 06 June 2016, 12:53:22 UTC | 3/9. | 06 June 2016, 12:53:22 UTC |
| 6df2901 | Roly Perera | 06 June 2016, 12:35:44 UTC | 9 residuation rules need changing... | 06 June 2016, 12:35:44 UTC |
| c4ae784 | Roly Perera | 06 June 2016, 12:31:04 UTC | Experiment with explicit id substitution in the extrusion rendezvous rule. Seems to be the generality required to support the slicing behaviour we want... | 06 June 2016, 12:31:04 UTC |
| abf77d0 | Roly Perera | 05 June 2016, 10:03:44 UTC | case/subcase. | 05 June 2016, 10:03:44 UTC |
| fdf1870 | Roly Perera | 04 June 2016, 17:56:34 UTC | Onto │ᵥ′. 16 top-level cases before I've even made the recursive calls :) | 04 June 2016, 17:56:34 UTC |
| 8454c6b | Roly Perera | 04 June 2016, 09:20:13 UTC | Drop any cases of concurrency which are redundant because of symmetry. | 04 June 2016, 09:20:13 UTC |
| 80a2573 | Roly Perera | 04 June 2016, 09:12:39 UTC | Drop any cases of concurrency which are redundant because of symmetry. | 04 June 2016, 09:12:39 UTC |
| 545e13e | Roly Perera | 03 June 2016, 15:41:41 UTC | 15 or so cases to go. | 03 June 2016, 15:41:41 UTC |
| 62701a3 | Roly Perera | 02 June 2016, 10:30:42 UTC | source/target -> src/tgt | 02 June 2016, 10:30:42 UTC |
| e534484 | Roly Perera | 02 June 2016, 10:28:19 UTC | Finally, get rid of the annoying S/S' overloaded field names. | 02 June 2016, 10:28:19 UTC |
| 6a5ff3b | Roly Perera | 02 June 2016, 10:24:54 UTC | Finally, get rid of the annoying S/S' overloaded field names. | 02 June 2016, 10:24:54 UTC |
| cda2940 | Roly Perera | 02 June 2016, 10:22:54 UTC | source/target -> src/tgt | 02 June 2016, 10:22:54 UTC |
| 69bc469 | Roly Perera | 27 May 2016, 10:37:00 UTC | Explain better. | 27 May 2016, 10:37:00 UTC |
| f96bc4b | Roly Perera | 23 May 2016, 12:40:26 UTC | Restore old 'out' ,etc. | 23 May 2016, 12:40:26 UTC |
| 1c20798 | Roly Perera | 21 May 2016, 14:57:10 UTC | Sync up γ.! | 21 May 2016, 14:57:10 UTC |
| 5133a26 | Roly Perera | 19 May 2016, 12:31:24 UTC | Design notes on cofinality relation. | 19 May 2016, 12:31:24 UTC |
| 3102717 | Roly Perera | 19 May 2016, 12:28:54 UTC | Design notes on cofinality relation. | 19 May 2016, 12:28:54 UTC |
| 24c638b | Roly Perera | 19 May 2016, 12:02:27 UTC | Nope, that doesn't work. | 19 May 2016, 12:02:27 UTC |
| c21e50f | Roly Perera | 19 May 2016, 11:48:43 UTC | Experiment. | 19 May 2016, 11:48:43 UTC |
| 605e72f | Roly Perera | 09 May 2016, 14:03:51 UTC | Skeleton of iso. | 09 May 2016, 14:03:51 UTC |
| 351e652 | Roly Perera | 09 May 2016, 13:47:19 UTC | Lift ᴿ+ to lattice setting. | 09 May 2016, 13:47:19 UTC |
| 0140840 | Roly Perera | 09 May 2016, 11:55:12 UTC | Generalise to +-preserves-involutivity. | 09 May 2016, 11:55:12 UTC |
| c1fdd5d | Roly Perera | 09 May 2016, 11:36:54 UTC | Generalise to +-preserves-involutivity. | 09 May 2016, 11:36:54 UTC |
| 337214d | Roly Perera | 09 May 2016, 11:34:22 UTC | Generalise swap-involutive to shift under an arbitrary context. | 09 May 2016, 11:34:22 UTC |
| 5420c87 | Roly Perera | 13 April 2016, 00:50:56 UTC | Sync README. | 13 April 2016, 00:50:56 UTC |
| 0d15d46 | Roly Perera | 28 March 2016, 19:32:35 UTC | Had a couple of subst-related posulates in the GC instance for bound braids; should be able to get rid of those. | 28 March 2016, 19:32:35 UTC |
| cfaeccb | Roly Perera | 28 March 2016, 00:06:17 UTC | First pass over lattice impl for new (functional) notion of renaming. | 28 March 2016, 00:06:17 UTC |
| 78eb25f | Roly Perera | 27 March 2016, 14:32:47 UTC | Import equality testing from Data.Fin. | 27 March 2016, 14:32:47 UTC |
| e81be27 | Roly Perera | 03 February 2016, 21:41:52 UTC | Use project-specific naming convention for 'shared modules' module. | 03 February 2016, 21:41:52 UTC |
| 575b5aa | Roly Perera | 04 January 2016, 21:08:33 UTC | Not true that concurrent extrusion-synchronisations are necessarily of different binders. | 04 January 2016, 21:08:33 UTC |
| 0086631 | Roly Perera | 04 January 2016, 15:35:16 UTC | Hmm, my comment on ⋉ was quite out-of-date; this relation isn't just the reflexive closure of ⋉̂, but also permits the braid to be duplicated across the branches of a parallel. | 04 January 2016, 15:35:16 UTC |
| 6a3e587 | Roly Perera | 04 January 2016, 15:33:49 UTC | Hmm, my comment on ⋉ was quite out-of-date; this relation isn't just the reflexive closure of ⋉̂, but also permits the braid to be duplicated across the branches of a parallel. | 04 January 2016, 15:33:49 UTC |
| 6155307 | Roly Perera | 04 January 2016, 15:09:32 UTC | Sync up names of braiding/cofinality relations with LFMTP slides. Will use the same for the paper. | 04 January 2016, 15:09:32 UTC |
| e7ecb73 | Roly Perera | 04 January 2016, 15:05:09 UTC | 'Bound' braid (and its reflexive closure) should have similar notation; use the one from the LFMTP slides. | 04 January 2016, 15:05:09 UTC |
| eaaae79 | Roly Perera | 04 January 2016, 15:03:01 UTC | 'Bound' braid (and its reflexive closure) should have similar notation; use the one from the LFMTP slides. | 04 January 2016, 15:03:01 UTC |
| 1c18357 | Roly Perera | 04 January 2016, 14:59:54 UTC | 'Bound' braid (and its reflexive closure) should have similar notation; use the one from the LFMTP slides. | 04 January 2016, 14:59:54 UTC |
| 9cd35cc | Roly Perera | 04 January 2016, 14:51:07 UTC | 'Bound' braid (and its reflexive closure) should have similar notation; use the one from the LFMTP slides. | 04 January 2016, 14:51:07 UTC |
| 3823852 | Roly Perera | 04 January 2016, 13:49:04 UTC | Clarify that there are 5 (modulo symmetry) kinds of concurrent action. Also concurrent extrusion-rendezvous are necessarily of different binders. | 04 January 2016, 13:49:04 UTC |
| bae539e | Roly Perera | 04 January 2016, 13:45:57 UTC | Residuals of concurrent actions no longer required. | 04 January 2016, 13:45:57 UTC |
| 71fd55b | Roly Perera | 03 January 2016, 22:04:29 UTC | precise-cofinality merge will be 0.2 release. Migrate release notes from paper to agda repo. | 03 January 2016, 22:04:29 UTC |
| 03aa059 | Roly Perera | 03 January 2016, 21:50:53 UTC | Resolve merge conflicts. | 03 January 2016, 21:50:53 UTC |
| 1a8b34f | Roly Perera | 03 January 2016, 21:35:25 UTC | 'Everything' module (called ProofRelevantPi, so as not to conflict with categories.Everything). | 03 January 2016, 21:35:25 UTC |
| 8594104 | Roly Perera | 03 January 2016, 21:26:43 UTC | Todo on 'Everything' module. Strikeout tasks relating to higher-dimensional concurrency. | 03 January 2016, 21:26:43 UTC |
| 26896f8 | Roly Perera | 03 January 2016, 21:21:19 UTC | Example isn't much cop, but clearer what to do now, and at least it's compiling (with the addition of a few postulates). | 03 January 2016, 21:21:19 UTC |
| 011bfc3 | Roly Perera | 03 January 2016, 20:52:03 UTC | Example was based on two-dimensional residuals. But I don't need to be able to compute those, I think the point is that I can construct those by hand. | 03 January 2016, 20:52:03 UTC |
| 0f590a6 | Roly Perera | 03 January 2016, 20:47:43 UTC | Release candidate for precise-cofinality branch. (Leaving ≃-sym unproven, as it wasn't proven before anyway. | 03 January 2016, 20:47:43 UTC |
| cad8eb8 | Roly Perera | 03 January 2016, 20:39:56 UTC | Reflexivity is still trivial. | 03 January 2016, 20:39:56 UTC |
| bb00cd3 | Roly Perera | 03 January 2016, 20:39:15 UTC | First pass over new causal equivalence definition. | 03 January 2016, 20:39:15 UTC |
| 56cb97c | Roly Perera | 03 January 2016, 20:38:50 UTC | Well, ⋈-to-⋉ seems to fix that. (Need to revisit notation.) | 03 January 2016, 20:38:50 UTC |
| 5d3ecdb | Roly Perera | 03 January 2016, 20:35:23 UTC | Fix anomaly where seemed to be requiring the tail of a transposition proof to equate two traces which are not only coinitial but also cofinal and with the same actions :-/ | 03 January 2016, 20:35:23 UTC |
| 6c2605a | Roly Perera | 03 January 2016, 20:21:09 UTC | Hmm, this case seems to cause problems because of the use of ⋈... | 03 January 2016, 20:21:09 UTC |
| 4649a3c | Roly Perera | 03 January 2016, 20:18:02 UTC | Just missing causal equivalence constructor for the ᵛ∇ᵛ case. | 03 January 2016, 20:18:02 UTC |
| b3bc82c | Roly Perera | 03 January 2016, 20:16:33 UTC | Hmm, gonna need a new causal equivalence constructor for the ᵛ∇ᵛ case. | 03 January 2016, 20:16:33 UTC |
| cfd2917 | Roly Perera | 03 January 2016, 17:18:20 UTC | Back to syncing up causal equivalence. | 03 January 2016, 17:18:20 UTC |
| 2cf7cb1 | Roly Perera | 03 January 2016, 17:15:22 UTC | Done with 'cofinality of cofinality residual' proof. | 03 January 2016, 17:15:22 UTC |
| f0c837a | Roly Perera | 03 January 2016, 17:11:52 UTC | But reinstate ≅-cong-swap as a global for reuse in the other case. | 03 January 2016, 17:11:52 UTC |
| 8d07099 | Roly Perera | 03 January 2016, 17:09:23 UTC | Inline 'blah' local first... | 03 January 2016, 17:09:23 UTC |
| 28a8e72 | Roly Perera | 03 January 2016, 17:06:38 UTC | Inline experiment. Now for remaining case. | 03 January 2016, 17:06:38 UTC |
| b519984 | Roly Perera | 03 January 2016, 16:59:23 UTC | Make ≅-cong✴₂′ helper local. | 03 January 2016, 16:59:23 UTC |
| a274dc6 | Roly Perera | 03 January 2016, 16:53:02 UTC | Inline functional argument. | 03 January 2016, 16:53:02 UTC |
| 2b9f111 | Roly Perera | 03 January 2016, 16:49:37 UTC | Implicit gamma. | 03 January 2016, 16:49:37 UTC |
| 2a0b91a | Roly Perera | 03 January 2016, 16:43:04 UTC | Success, just need to consolidate. | 03 January 2016, 16:43:04 UTC |
| 22e9c27 | Roly Perera | 03 January 2016, 16:38:32 UTC | Possible progress. | 03 January 2016, 16:38:32 UTC |
| d920a20 | Roly Perera | 03 January 2016, 16:24:44 UTC | Can we make it about a Proc in a fixed context? | 03 January 2016, 16:24:44 UTC |
| 761e985 | Roly Perera | 03 January 2016, 16:22:41 UTC | Let's fully specialise first of all... | 03 January 2016, 16:22:41 UTC |
| 0863fd7 | Roly Perera | 03 January 2016, 16:16:22 UTC | Start hacking ≅-cong✴₂ to making it a closer fit to my problem... | 03 January 2016, 16:16:22 UTC |
| 548a0e2 | Roly Perera | 03 January 2016, 16:09:10 UTC | Minor progress on heterogeneous congruence problem... | 03 January 2016, 16:09:10 UTC |
| bcd06be | Roly Perera | 03 January 2016, 16:03:10 UTC | Experiment with isolated version of remaining problem case.. | 03 January 2016, 16:03:10 UTC |
| d86244c | Roly Perera | 03 January 2016, 15:59:28 UTC | Other ᵛ∇ᵛ case. | 03 January 2016, 15:59:28 UTC |
| 469f610 | Roly Perera | 03 January 2016, 15:57:50 UTC | First ᵛ∇ᵛ case. | 03 January 2016, 15:57:50 UTC |
