Colocal types #1089
Colocal types #1089
Conversation
|
Hi! I think we had this discussion with Tom before, when we should speak of the diagonal and when we should speak of the constant map. Eg: it is misleading to say that "the constant map is an equivalence" if it is merely meant that In this pull request I see some changes from "diagonal" back to "constant map". Is the above consideration taken into account here? |
| is an [equivalence](foundation-core.equivalences.md). This is dual to the notion | ||
| of an [`f`-local type](orthogonal-factorization-systems.local-types.md), which | ||
| is a type such that the | ||
| [precomposition map](foundation-core.precomposition-functions.md) | ||
|
|
||
| ```text | ||
| _∘ f : (Y → A) → (X → A) | ||
| ``` | ||
|
|
||
| is an equivalence. |
There was a problem hiding this comment.
I think this exposition deserves a bit more detail. For instance, we can't expect readers to be able to infer what kind of types are colocal merely from the sentence "This is dual to the notion of local". Things to include that would improve this prose would be answers to the following questions:
- What does it really mean for a type to be colocal at
f? - Does it generalize or is it related to already existing concepts?
- In what context is this definition relevant?
Defines what it means for a type to be colocal at a map, and shows a few basic properties of these.