More logic #1387
More logic #1387
Conversation
|
|
||
| The | ||
| {{#concept "double negation image" Disambiguation="of a map" Agda=double-negation-im}} | ||
| of `f : A → B` is the essentially unique type that factorizes `f` as a |
There was a problem hiding this comment.
You write about an essentially unique type, but I see no reference to uniqueness (or universal properties) in this file. Honestly this paragraph is pretty cryptic, and I find it hard to believe it's at all understandable to many people outside Martín's sphere of influence 😅. Would you mind rephrasing it, and at least drawing a diagram?
There was a problem hiding this comment.
I expanded a bunch on the idea section, let me know if it is satisfactory now or if I included something new that is confusing.
| {l1 l2 l3 : Level} {A : UU l1} | ||
| where | ||
|
|
||
| is-decidable-comp-decidable-family-decidable-subtype' : |
There was a problem hiding this comment.
I don't think this and the following definition are related to subtypes specifically?
|
|
||
| **Remark.** It is an established fact that both the property of satisfying | ||
| double negation elimination, and the property of having decidable negation, are | ||
| strictly weaker conditions than being decidable. Therefore, this result |
There was a problem hiding this comment.
I don't understand how this proves independence. Also could you include a source for the "established fact"?
| has-prop-double-negation-elim-has-double-negation-elim H = unit-trunc-Prop ∘ H | ||
| ``` | ||
|
|
||
| ### Propositional double negation elimination for merely decidable types |
There was a problem hiding this comment.
Heading says "merely decidable", formalization says is-inhabited-or-empty
|
|
||
| ## Idea | ||
|
|
||
| A [map](foundation-core.function-types.md) is said to be |
There was a problem hiding this comment.
"Propositionally decidable maps/types" don't actually appear to ever be mentioned in prose outside of their files? You usually use "merely decidable", wouldn't it then be better to name the concept that? Especially since the corresponding definition is is-inhabited-or-empty(-map)?, not is-propositionally-decidable(-map)?
There was a problem hiding this comment.
While I can't recall my rationale for this terminology anymore, notice that there are multiple concepts one might refer to as "merely decidable":
║ is-decidable-map f ║₋₁(x : A) → ║ is-decidable (fiber f x) ║₋₁(x : A) → is-inhabited-or-empty (fiber f x)
while the last two are equivalent, the first one is a stronger assumption which is implied by choice. I don't know if perhaps I reserved "merely decidable map" for the first one, I'll have to think about it
| ### Decidable maps are propositionally decidable | ||
|
|
||
| ```agda | ||
| is-inhabited-or-empty-map-is-decidable-map : |
There was a problem hiding this comment.
Is this definition intentionally non-abstract, in contrast with the other functions?
There was a problem hiding this comment.
Probably yes. Cf my other comment on unfolding
src/logic/propositionally-double-negation-eliminating-maps.lagda.md
Outdated
Show resolved
Hide resolved
…da.md Co-authored-by: Vojtěch Štěpančík <[email protected]>
Co-authored-by: Vojtěch Štěpančík <[email protected]>
Co-authored-by: Vojtěch Štěpančík <[email protected]>
Co-authored-by: Vojtěch Štěpančík <[email protected]>
Pulls logic additions from #1264.