Commit graph

298 commits

Author SHA1 Message Date
5641cb3dd7
minor 2023-11-14 19:04:50 +01:00
c11ad1998c
Progress on commutativity 2023-11-13 16:24:28 +01:00
fb0d6f2799
🎨 rewrite index 2023-11-13 10:31:10 +01:00
a747658f8b
🎨 moved unused files to /src/Misc 2023-11-13 09:45:15 +01:00
4d052891cd
minor 2023-11-11 15:44:16 +01:00
21c98bab4f
🚧 Case-statements and small progress on restriction category 2023-11-11 14:56:03 +01:00
a3973a0b38 Add "delay monad in agda" slides 2023-11-09 11:41:35 +00:00
b6016084ac
Work on kleene 2023-11-07 19:29:58 +01:00
91ccbbf0c3
Work on kleene 2023-11-07 13:53:13 +01:00
bfd597591c
🚧 added proof by induction, started work on kleenes fixpoint theorem 2023-11-06 19:30:21 +01:00
5bdc57f064
Finished small proof 2023-11-06 15:26:18 +01:00
91ca1b5813
Work on kleene fixpoint 2023-11-06 12:59:43 +01:00
317702c0f6
Started showing that K is preelgot 2023-11-05 14:09:54 +01:00
28cee7138e
Show equational lifting law, added proof principle 2023-11-04 09:52:36 +01:00
7f336282ed
work on new proof principle 2023-11-03 17:33:44 +01:00
446d55f1f5
Merge branch 'main' of git8.cs.fau.de:theses/bsc-leon-vatthauer 2023-11-01 20:06:30 +01:00
6bb5bd519e
introduce equational lifting 2023-11-01 20:06:20 +01:00
de565d00c7
Started working on motivation 2023-10-31 17:11:38 +01:00
61573d159c
Work on commutativity 2023-10-31 14:16:47 +01:00
e8d8377c79
Worked on commutativity 2023-10-29 10:54:09 +01:00
f92fbc76ed
🚧 Work on commutativity of K 2023-10-28 17:37:01 +02:00
07dffa087c
🎨 Tidy up proof that K is strong, add explanations 2023-10-28 13:59:23 +02:00
d61a4c8bfa Added usage notes 2023-10-28 10:44:52 +00:00
55e3e91d18
❄ added nix devshell 2023-10-28 12:34:15 +02:00
bf4af5ad9c
Working on small lemma 2023-10-25 18:19:09 +02:00
7e7ff5268f
minor 2023-10-25 18:18:58 +02:00
9dfd4145a2
Finished strength of K 2023-10-25 18:18:30 +02:00
a71045161a
Align proofs 2023-10-22 15:07:39 +02:00
544b604ce8
Finished proof that delay is commutative 2023-10-17 21:58:43 +02:00
16608a236f
🚧 Work on commutativity 2023-10-17 15:21:30 +02:00
cfd5bf4968
🚧 Great progress on commutativity proof of delay monad 2023-10-16 18:08:34 +02:00
14c41b3666
Added missing proof principle 2023-10-16 11:07:30 +02:00
9ff33adfda
🚧 Work on commutativity 2023-10-15 17:55:42 +02:00
65d971eb68
🎨 Tidying up proofs, added small lemma 2023-10-15 14:40:01 +02:00
47035c1e52
Added index with some nice text 2023-10-12 21:39:36 +02:00
c166f40576
🚧 Small progress, stuck on multiple fronts 2023-10-12 18:11:28 +02:00
09732380ec
🚧 Working on stable algebras, currently showing that K is strong 2023-10-09 16:45:55 +02:00
b7cc991d11
🚧 prepare for meeting 2023-10-09 12:11:21 +02:00
b325ecc6c3
🚧 Working on stable algebras 2023-10-05 16:22:05 +02:00
b6da0a4242
Finished 1=>2 of theorem 35 2023-10-05 14:31:12 +02:00
b6a89dbdc8
️ Finished many helper lemmas and a small proof 2023-10-05 12:48:06 +02:00
0b71566f54
️ Proof that rho is natural in X 2023-10-04 23:45:29 +02:00
22306ddb27
️ Proof that quotiented D is a functor 2023-10-04 22:44:48 +02:00
7e9653c41e
🔀 Merge branch 'main' of git8.cs.fau.de:theses/bsc-leon-vatthauer 2023-10-03 19:44:22 +02:00
0165423fcf
🚧 Started working on quotienting the delay monad 2023-10-03 19:44:08 +02:00
0cf7c2e866 Update README.md 2023-10-03 17:01:18 +00:00
e5157c0bc5
Finished proving strength of delay monad 2023-10-03 18:55:46 +02:00
3fad80110d
Still working on delay strength, finished strength-assoc 2023-09-30 17:33:47 +02:00
571ed10fec
Stuck on mu-eta strength, started assoc 2023-09-29 17:28:54 +02:00
59492a9502
Progress on strength for delay monad 2023-09-27 20:06:46 +02:00