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 $Time_1 \rightrightarrows Time_0$ and $Worlds \to \ast$. I concluded that we can reformulate the latter as pullback $PairsAccessibleWorlds \rightrightarrows 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, $Time_0 \to ??$. 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 $\ast$ in the latter case, just because there is a disanalogy in that unlike $Worlds \to \ast$ it’s not $\ast \to B G$, but $B G \to \ast$ that I care about.
Can we not have an epi $Worlds \to Time_0$, and then induce the groupoid with objects $Worlds$ from $Time_1\rightrightarrows Time_0$?
1 to 2 of 2