Logic, equality, and compactness #1264
Conversation
| **Terminology.** In the terminology of Martín Escardó, a type that has | ||
| ∀-decidability search is referred to as _weakly compact_, or _Π-compact_, or | ||
| _satisfying the weak principle of omniscience_. {{#cite TypeTopology}} |
There was a problem hiding this comment.
It would be useful here to mention also whether the terminology "∀-decidability" is our own name for the concept, or whether it is more widely used in other literature (I couldn't tell the answer from what has been written so far in this file). Same for all the related decidability searches.
There was a problem hiding this comment.
Right, yes. This is new terminology
| _exhaustively searchable_, _exhaustibly searchable_, _exhaustible_, | ||
| _omniscient_, _satisfying the principle of omniscience_, _compact_, or | ||
| _Σ-compact_. {{#cite Esc08}} {{#cite TypeTopology}} We reserve the term | ||
| _Σ-decidability searchable_ for types for which there (merely) |
There was a problem hiding this comment.
The phrase "Σ-decidability searchable" grammatically questionable, because it combines a noun "Σ-decidability" with an adjective "searchable" in the wrong order. Please find better terminology.
| has-Σ-decidability-search-Level : | ||
| {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2) | ||
| has-Σ-decidability-search-Level l2 X = | ||
| (P : decidable-family l2 X) → is-decidable (Σ X (family-decidable-family P)) |
There was a problem hiding this comment.
If I read this concept correctly, the scheme here is that for families of a certain kind, the total space is again of that kind. (This concept could also be interesting for localizations: local types such that the domain of every map with local fibers into it has a local domain.) So wouldn't it be better for the name to have that kind be postfixed to the name, rather than prefixed as an adjective?
For example, has-pair-search-decidable-family would seem more fitting with our naming scheme, or has-pairing-search-decidable-family. I'd read this name as follows: There is a function which, given a decidable family searches for a pair or reports that there is no such pair.
Another idea would be just to name this concept "has-Σ-decidability" without postfixing the word "search", because the concept is just about decidability of Σ-types. Or even "has-decidable-Σ".
There was a problem hiding this comment.
Indeed! I suppose for instance projectivity of a type is exactly "Π-inhabitedness".
There was a problem hiding this comment.
I tried implementing the terminology "having decidable Σ-types" in the most recent commit
|
Martín just explained to me that the "types with double negation dense equality have decidable sigmas" result is a special case of "types are compact iff their totally separated reflections are compact", so that should be remarked in the appropriate places before merging. |
A lot of results in logic and foundations.
Summary