• Joined on 2023年08月11日
jaycech3n pushed to main at jaycech3n/in-hott 2026年07月09日 17:49:26 +02:00
372c3c93b5 interim
6c329d5a3f some yoneda
Compare 2 commits »
jaycech3n pushed to main at jaycech3n/ars 2026年07月09日 17:43:14 +02:00
4a4643a9d0 update
jaycech3n pushed to main at jaycech3n/ars 2026年07月09日 17:37:17 +02:00
d8b8057046 update
jaycech3n pushed to main at jaycech3n/ars 2026年07月08日 13:08:26 +02:00
4d41bbf12e update
6590268f8f update
Compare 2 commits »
jaycech3n pushed to main at jaycech3n/in-hott 2026年07月03日 18:44:42 +02:00
bbfa624af6 yoneda
jaycech3n pushed to main at jaycech3n/in-hott 2026年06月29日 23:51:17 +02:00
3b290c8d10 pre-experimental change commit
Compare 2 commits »
jaycech3n pushed to main at jaycech3n/in-hott 2026年06月25日 18:17:04 +02:00
96ea903cbf yoneda stuff
jaycech3n pushed to main at jaycech3n/in-hott 2026年06月25日 14:52:26 +02:00
bab789b734 tidy up
jaycech3n pushed to main at jaycech3n/in-hott 2026年06月25日 14:00:43 +02:00
f98e64e828 Functor wild categories.
jaycech3n pushed to main at jaycech3n/in-hott 2026年06月24日 20:54:06 +02:00
e2e5564c59 more commuting squares
Compare 2 commits »
jaycech3n pushed to main at jaycech3n/in-hott 2026年06月23日 18:36:42 +02:00
17d97787f4 we're on our way
162c8a23e7 working on wild natural transformations and commuting squares: interim commit just before upgrading the path solver to normalize whiskering
Compare 2 commits »
jaycech3n pushed to main at jaycech3n/in-hott 2026年06月22日 00:32:44 +02:00
6e813940e3 associativity of horizontal pasting for 2-coherent semicats
9651d0f5fd interim en route to proof
Compare 2 commits »
jaycech3n pushed to main at jaycech3n/in-hott 2026年06月19日 01:31:56 +02:00
b87affd482 clean up Yoneda Id
Compare 5 commits »
jaycech3n pushed to main at jaycech3n/in-hott 2026年06月15日 17:45:22 +02:00
60908d0885 using the postulated TC monad operations directly appears to be substantially less resource-intensive
5d78006742 solvers sprucing up
7240143e58 remove unnecessary stuff
Compare 4 commits »
jaycech3n opened issue 1lab/mikan#133 2026年06月10日 18:38:17 +02:00
Typechecking anonymous parametrized module is much slower than expected
jaycech3n pushed to main at jaycech3n/in-hott 2026年06月09日 00:21:58 +02:00
1d4ae58d25 revamped path category solver is x10s as fast
c1c0bbf3c9 tidy up
896bfffb72 cleanup
Compare 3 commits »
jaycech3n pushed to main at jaycech3n/in-hott 2026年06月06日 13:51:05 +02:00
1a2a54945e more efficient groupoid solver works
jaycech3n pushed to main at jaycech3n/in-hott 2026年06月04日 20:04:02 +02:00
9f3a915077 much faster groupoid solver in the works
jaycech3n pushed to main at jaycech3n/in-hott 2026年06月04日 15:16:47 +02:00
00433bdbed reflected term equality
fd70d518c9 1. Reorganize: PathCategories --> PathGroupoids, tests in separate modules. 2. GroupoidSolver cleanup; I think it's slow because (a) instance search for TrackAdjInvPairs is slow (b) quoting the...
Compare 3 commits »
jaycech3n pushed to main at jaycech3n/in-hott 2026年05月18日 15:25:27 +02:00
05d90532e5 1. Reorganize: PathCategories --> PathGroupoids, tests in separate modules. 2. GroupoidSolver cleanup; I think it's slow because (a) instance search for TrackAdjInvPairs is slow (b) quoting the...
63b62c4d97 groupoid solver functionality is there now, I think. Slow, but works
Compare 2 commits »