Post #2103983
2026-02-12 14:09 UTC
@constantine @edwinb Yes, I think that's what threw me off. The sort itself is interpreted as a subterminal presheaf (so a functor Con → Ω) whose elements at Γ are maps Γ → φ. I wonder if you mean anything precise by "relativises".
Replies (1)
-
@constantine@types.pl 2026-02-12 14:27
@ncf Makes sense, I will edit that, thanks. By relativises I basically mean the ‘contextualisation’ procedure, which in the basic case takes a Tarski universe and turns it into a CwF (but there are a few variations of it that are given in @rafaelbocquet ‘s thesis, one of which is the correspondence between SOGAT and GAT models)