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?
| false ≤ false | ||
| false ≤ true | ||
| true ≤ true | ||
| true ≰ false. |
There was a problem hiding this comment.
Why would a non-inequality be a generator of an inductive relation? And since the relation is not literally given by the inequalities, wouldn't it be better to write what it actually is defined as, and then note an alternative way of looking at it? I think I noticed this trend of the prose and Agda matching only up to (sometimes unproven) equivalence
| leq-right-or-bool {x} {true} p = star | ||
| leq-right-or-bool {false} {false} p = star | ||
|
|
||
| leq-or-bool'' : |
There was a problem hiding this comment.
These should have better names, but I'm currently too tired to come up with any
There was a problem hiding this comment.
It is one direction of the universal property of or, so something like is-lower-bound-or-bool should work
There was a problem hiding this comment.
sorry, upper bound*
Pulls logic additions from #1264.