image inclusion

[marcbezem]

Why is the unit map in 2.27.1 called "image inclusion"? It is rather the $p$ of the image factorization in 2.26.4, and not the $i$. The latter is an injection (n-truncated in general), whereas $p$ is surjective (n-connected in general).

[UlrikBuchholtz]

I don't think we define anywhere what an “inclusion” is! In particular, we should not restrict its use to injections. Here are some other examples of inclusions in the book:

• the wedge inclusion A ∨ B → A × B, special case on p. 92
• direct sum inclusion at the level of classifying types BG → BG × BH, p. 98

Perhaps we'd also like to have a “point inclusion” pt : 1 → BG?

For HITs, it's also natural to say that any non-recursive point constructor is a kind of inclusion, since the whole HIT adds stuff on top of this. For example, are the point constructors of a pushout not inclusions of a kind?

We could decide to restrict “inclusion” to mean “injection”, but then we lose many of the above. Something to discuss Thursday?

[bidundas]

In set theory an inclusion is a special type of injection (the canonical injection of a subset).

So, if X:A->U is a type family and a:A some (I?) might be willing to call the canonical map X(a) -> \Sum_{b:A}X(b) 'the inclusion' (generalizing from the subset classifier) though it may not be an injection in the current language and is evil in that it depends on the particular presentation

It’s then a descriptive term: it specifies what map I’m talking about, it’s not a property of the map (cf also Ulrik’s examples).

For families of propositions I wouldn’t hesitate. Perhaps there are other instances..

Bjorn

On Jan 10, 2023, at 13:10, Ulrik Buchholtz @.***> wrote:

I don't think we define anywhere what an “inclusion” is! In particular, we should not restrict its use to injections. Here are some other examples of inclusions in the book:

• the wedge inclusion A ∨ B → A × B, special case on p. 92 • direct sum inclusion at the level of classifying types BG → BG × BH, p. 98 Perhaps we'd also like to have a “point inclusion” pt : 1 → BG?

For HITs, it's also natural to say that any non-recursive point constructor is a kind of inclusion, since the whole HIT adds stuff on top of this. For example, are the point constructors of a pushout not inclusions of a kind?

We could decide to restrict “inclusion” to mean “injection”, but then we lose many of the above. Something to discuss Thursday?

— Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you are subscribed to this thread.

[marcbezem]

Good to discuss this, here and possibly on Thursday. I'm not at all against the terminology, since it was defined right after. It would be good to say something more about it as there are 33 occurrences of "inclusion" in the book, from 2.18.6 on. Note that in "a point inclusion" one stresses what is included, and in "image inclusion" it is ambiguous: for f: A->B, the image inclusion includes for each a in A the image of a under f in the image of f (nothing wrong with that). There might be quite some diversity in these 33 occurrences.

[UlrikBuchholtz]

Fixed in 0d86a5a