Post #2103982
2026-02-12 14:06 UTC
@ncf @edwinb Maybe the wording is a bit weird though, it should maybe say
“interpreted as (Γ → φ)”
because otherwise it sounds like there is a particular unspecified map of type Γ → φ..
Replies (1)
-
@ncf@types.pl 2026-02-12 14:09
@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".