Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
From that discussion on temporal logic, I was thinking about the comparison of ’henceforth’ with necessarily, and why doing base change and dependent product seemed different for Time1⇉Time0 and Worlds→*. I concluded that we can reformulate the latter as pullback PairsAccessibleWorlds⇉Worlds and the comparison is much closer.
So then we seem to have greater flexibility with the latter in the sense that I can’t do the projection onto classes trick with time, Time0→??. Equivalence relations may be treated either way, but not in general.
But then when it comes to representation theory, wouldn’t the analogy with Worlds go:
But I’m not going to want to base change from * in the latter case, just because there is a disanalogy in that unlike Worlds→* it’s not *→BG, but BG→* that I care about.
Can we not have an epi Worlds→Time0, and then induce the groupoid with objects Worlds from Time1⇉Time0?
1 to 2 of 2