74 commits

Author	SHA1	Message	Date
Leon Vatthauer	6d254586e1	minor	2024-03-16 10:09:31 +01:00
Leon Vatthauer	75d6990bd5	Finishing touches on partiality chapter	2024-03-15 17:35:39 +01:00
Leon Vatthauer	98cdfffdb9	minor	2024-03-12 16:18:07 +01:00
Leon Vatthauer	5f836b4d89	minor	2024-03-11 18:15:55 +01:00
Leon Vatthauer	64f76f92f7	minor	2024-03-10 20:59:35 +01:00
Leon Vatthauer	7986abb134	improve proofs	2024-03-04 17:09:22 +01:00
Leon Vatthauer	a1046d16e1	minor	2024-02-22 18:04:17 +01:00
Leon Vatthauer	a3f077bd8d	Final refactor	2024-02-20 15:09:58 +01:00
Leon Vatthauer	c2e6966610	Continue work on refactor, almost finished	2024-02-19 18:07:46 +01:00
Leon Vatthauer	adf99ef3e0	major refactor to finish up	2024-02-18 18:15:15 +01:00
Leon Vatthauer	e4af840dc2	some more refactor	2024-02-15 21:51:54 +01:00
Leon Vatthauer	98837f659c	some refactoring, change ambient category	2024-02-15 21:29:54 +01:00
Leon Vatthauer	8caee3929a	sync	2024-02-15 16:03:26 +01:00
Leon Vatthauer	031df0312d	sync todays work	2024-02-14 16:59:30 +01:00
Leon Vatthauer	896dc3d296	update index	2024-02-14 12:03:57 +01:00
Leon Vatthauer	8b435ffad5	remove html that was added by accident	2024-02-11 13:02:04 +01:00
Leon Vatthauer	2bf4655eae	update index	2024-02-09 17:53:52 +01:00
Leon Vatthauer	ac39b97ce2	Added READMEs	2024-02-09 13:49:08 +01:00
Leon Vatthauer	24a1bbee0e	Proof that maybe is equational lifting	2024-02-08 16:16:21 +01:00
Leon Vatthauer	d6c13a88e4	minor	2024-02-06 18:23:12 +01:00
Leon Vatthauer	4d82edeab9	small refactor	2024-02-06 11:37:52 +01:00
Leon Vatthauer	161ceabcda	Finish proof that D~~ is instance of K on setoids. Did some refactor on StableFreeElgotAlgebras, proved that left-stable and right-stable imply each other	2024-02-05 18:13:44 +01:00
Leon Vatthauer	17c023c944	refactor for exponential algebras	2024-02-04 18:49:12 +01:00
Leon Vatthauer	38c29332fc	merge elgot branch (unfinished)	2024-02-04 18:00:40 +01:00
Leon Vatthauer	1f4c0da823	tidy up	2024-02-04 17:58:30 +01:00
Leon Vatthauer	bb49f23814	Finish proof that quotient of D is freealgebra	2024-02-04 17:55:22 +01:00
Leon Vatthauer	68588c6b82	update flake	2024-02-04 17:54:49 +01:00
Leon Vatthauer	32feee45e5	Finished preservation proof	2024-02-03 14:33:10 +01:00
Leon Vatthauer	b31d3e2540	stuck on final proof for stability	2024-02-02 17:59:59 +01:00
Leon Vatthauer	2e28faeda6	build on recent PR to agda-categories	2024-02-02 16:03:47 +01:00
Leon Vatthauer	75e61fcc33	minor	2024-02-02 12:45:17 +01:00
Leon Vatthauer	d90381d11a	minor progress	2024-02-01 14:00:54 +01:00
Leon Vatthauer	86e45d7b71	minor	2024-02-01 12:51:13 +01:00
Leon Vatthauer	d3b63f632d	progress on exponentials	2024-02-01 12:14:57 +01:00
Leon Vatthauer	85195b13d0	refactor elgot algebras	2024-02-01 10:29:03 +01:00
Leon Vatthauer	aea11ac62f	merge	2024-01-30 13:44:08 +01:00
Leon Vatthauer	78260e3f91	refactor to support newest agda-categories release	2024-01-29 18:15:06 +01:00
Leon Vatthauer	8241082f3f	updated agda-cat	2024-01-29 15:42:18 +01:00
Leon Vatthauer	2dc6420a35	sync	2024-01-29 15:38:50 +01:00
Leon Vatthauer	f0923f1007	finished congruence proof	2024-01-29 12:52:25 +01:00
Leon Vatthauer	11dd7f8f23	sync	2024-01-28 15:07:38 +01:00
Leon Vatthauer	7568f60833	Refactor to update library versions	2024-01-25 13:30:41 +01:00
Leon Vatthauer	6ba246ee53	updated library versions	2024-01-24 15:22:54 +01:00
Leon Vatthauer	577b095325	sync	2024-01-16 10:07:01 +01:00
Leon Vatthauer	5557dd1d6a	changed definition	2024-01-14 13:00:56 +01:00
Leon Vatthauer	291b33abbe	some renaming and new definitions	2024-01-14 12:20:49 +01:00
Leon Vatthauer	2cc26eeb9a	cleanup and add uniformity proof	2024-01-13 19:39:16 +01:00
Leon Vatthauer	202d130d33	Finish subproof	2024-01-10 17:46:55 +01:00
Leon Vatthauer	a6fd66ef29	sync	2024-01-09 16:02:09 +01:00
Leon Vatthauer	9beebd009d	Some progress	2024-01-09 13:34:53 +01:00