leonv

leonv synced commits to main at leonv/bsc-leon-vatthauer from mirror 2023-11-22 23:19:41 +01:00

3e4ecb3dfb work on proofs

96aa6b8994 Merge branch 'main' of git8.cs.fau.de:theses/bsc-leon-vatthauer

aaa48e4240 update index

Compare 3 commits »

leonv synced commits to main at leonv/bsc-leon-vatthauer from mirror 2023-11-22 15:09:19 +01:00

2317c6b30d minor

bb2e7c5061 Work on commutativity

bfb437ea36 fix makefile

fa5c81f587 ♻️ Major refactor, K is defined by free elgot algebras now

Compare 4 commits »

leonv synced commits to main at leonv/bsc-leon-vatthauer from mirror 2023-11-21 22:49:31 +01:00

eabc93af77 align proofs

leonv synced commits to main at leonv/bsc-leon-vatthauer from mirror 2023-11-20 14:09:18 +01:00

b74ecf373c align proofs

df288fccec ✨ Proof that K is initial strong pre-Elgot

d3712d4abd Add category of strong pre elgot monads

d762e280ad fix imports

Compare 4 commits »

leonv synced commits to main at leonv/bsc-leon-vatthauer from mirror 2023-11-18 13:09:18 +01:00

1f4e5460d7 show that K is strong pre-Elgot

7b39c02b12 🎨 Some more cleanup

50fee48b17 🎨 Cleanup and fix constraints.

Compare 3 commits »

leonv synced commits to main at leonv/bsc-leon-vatthauer from mirror 2023-11-15 19:49:16 +01:00

55dcf598fc Show that K is initial pre-Elgot

60f60ce3bf Work on initial pre-Elgot

08cf9b6f61 Merge branch 'main' of git8.cs.fau.de:theses/bsc-leon-vatthauer

0e89d52460 minor

bac3d12e52 Add category of pre-Elgot monads

Compare 6 commits »

leonv synced commits to main at leonv/bsc-leon-vatthauer from mirror 2023-11-15 11:39:20 +01:00

a877cd3f25 Proof that KX is freeElgot (still assuming compositionality)

leonv synced commits to main at leonv/bsc-leon-vatthauer from mirror 2023-11-15 03:29:20 +01:00

13450c1d23 Show that K is PreElgot

leonv synced commits to main at leonv/bsc-leon-vatthauer from mirror 2023-11-14 19:19:17 +01:00

5641cb3dd7 minor

leonv synced commits to main at leonv/bsc-leon-vatthauer from mirror 2023-11-13 18:49:18 +01:00

c11ad1998c Progress on commutativity

leonv synced commits to main at leonv/bsc-leon-vatthauer from mirror 2023-11-13 10:39:18 +01:00

fb0d6f2799 🎨 rewrite index

a747658f8b 🎨 moved unused files to /src/Misc

Compare 2 commits »

leonv synced commits to main at leonv/bsc-leon-vatthauer from mirror 2023-11-11 17:49:18 +01:00

4d052891cd minor

21c98bab4f 🚧 Case-statements and small progress on restriction category

Compare 2 commits »

leonv synced commits to main at leonv/bsc-leon-vatthauer from mirror 2023-11-09 16:49:16 +01:00

a3973a0b38 Add "delay monad in agda" slides

leonv synced commits to main at leonv/bsc-leon-vatthauer from mirror 2023-11-07 23:59:20 +01:00

b6016084ac Work on kleene

leonv synced commits to main at leonv/bsc-leon-vatthauer from mirror 2023-11-07 15:49:17 +01:00

91ccbbf0c3 Work on kleene

leonv synced commits to main at leonv/bsc-leon-vatthauer from mirror 2023-11-06 23:29:19 +01:00

bfd597591c 🚧 added proof by induction, started work on kleenes fixpoint theorem

5bdc57f064 Finished small proof

Compare 2 commits »

leonv synced commits to main at leonv/bsc-leon-vatthauer from mirror 2023-11-06 15:19:16 +01:00

91ca1b5813 Work on kleene fixpoint

leonv synced commits to main at leonv/bsc-leon-vatthauer from mirror 2023-11-05 14:49:18 +01:00

317702c0f6 Started showing that K is preelgot

leonv synced commits to main at leonv/bsc-leon-vatthauer from mirror 2023-11-04 14:19:17 +01:00

28cee7138e ✨ Show equational lifting law, added proof principle

leonv synced commits to main at leonv/bsc-leon-vatthauer from mirror 2023-11-03 21:59:16 +01:00

7f336282ed work on new proof principle