Back

For example, consider the function ℚ⁺ → ℝ that sends a positive rational number to its square root.

This function can be extended to a function ℝ⁺ → ℝ that generalizes square roots of rationals to square roots of positive reals.

In this particular case, the function ℚ⁺ → ℝ is continuous, and the function ℝ⁺ → ℝ is its unique continuous extension.

‌2/

Another example is Euler's Γ function that generalizes factorials from positive integers to the complex numbers, excluding the non-positive integers.

In this particular case, there are many other such extensions.

Here one wants extensions that are continuous and satisfy the factorial equation (n+1)! = n! × (n+1), with n generalized from natural numbers to reals or complex numbers.

3/

In some cases, it is impossible to extend functions so that they have desirable properties. For example, the continuous function ℝ\{ 0 } → ℝ that sends x to 1/x is continuous, but there is no continuous extension ℝ → ℝ that would make sense of 1/0.

4/

However, we can add a point at infinity to ℝ, as a topological space, to get the projective real line ℝ∞, its one-point compactification, so that we can define 1/0 = ∞, to get a continuous extension.

5/

The function 1/(-) : ℝ\{0} → ℝ *can* be extended to a function ℝ → ℝ, e.g by stipulating that 1/0 is π, or any other arbitrary real number.

But no such an extension can be continuous, no matter what we choose the value of 1/0 to be.

6/

In constructive mathematics, it may be that all functions are continuous.

What do we mean by this? There *are* models in which all functions are continuous.

7/

The mother of discontinuity is the principle of excluded middle.

Without it, we cannot define a discontinuous function.

We used excluded middle above to define the function that defines the value of the function at 1/0 to be π.

Given the input x of 1/x, we check wether x is zero or not, using excluded middle. If it iis zero, we define 1/x to be π, and, otherwise, we define 1/x in the usual way.

8/

Why do we care about constructive mathematics? There are zillions of reasons, depending on the constructive mathematician we speak to. The purpose of this thread is not to discuss that.

But here I want to mention two reasons that matter to me and to lots of people working on HoTT/UF.

(9.1) HoTT/UF can be interpreted in any ∞-topos, so that any statement in HoTT/UF means something in that topos.

A definition, or construction or proof in HoTT/UF makes sense in any ∞-topos.

Except if we go non-constructive and assume excluded middle and choice.

Proofs and constructions that use excluded middle, in HoTT/UF, apply only to so-called *boolean* ∞-toposes. Very few ∞-toposes are boolean.

So a main reason to be "constructive" (that is, avoid excluded middle and choice) is to be more general, in the sense of accounting for all ∞-toposes, not just the boolean ones.

(9.2) HoTT/UF can be used to compute. For example, we can compute in HoTT/UF using cubical Agda.

Not everybody, in the mathematical community, is interested in ∞-toposes (but for example Peter Scholze is, among many other people).

Not everybody is interested in computing (but a lot of us here are).

If you are not interested in (9.1) or (9.2), you will probably wish to stop reading this thread, unless you are curious to see what is going on.

9/

Having motivated the extension problem and constructivity in HoTT/UF, we move to the subject matter of this thread.

The general situation is that we have a function X → Y, and we want to extend it to a function X' → Y, where X' enlarges X.

If we did have excluded middle available, in general, the extension problem would always be solvable for non-empty Y. Given f : X → Y, we can define f' : X' → Y by f'(x) = f (x) if x in in X, and f'(x) = some arbitrarily chosen point of Y otherwise.

(You may need some additional amount of choice for this, if the assumption is simply that Y is non-empty, but I don't want to discuss this now.)

10/

Definition. A type D is injective if for every embedding j : X → X' and any function f : X → D, we can find a function f' : X' → D that extends f along j, in the sense that f' ∘ j = f.

Discussion. In HoTT/UF we have two choices. We may merely require that f' exists, or that it be explicitly given. Depending on the choice, we arrive at the notions of "injective" and "algebraically injective" type respectively.

I have studied both. Here I will restrict myself to "algebraically injective" types, for simplicity, which I will refer to as "injective" for the sake of brevity. I hope this will cause no confusion.

I developed a lot of results for (algebraically) injective types in my github repository TypeTopology [1] and then published them in the article [2]

[1] https://www.cs.bham.ac.uk/~mhe/TypeTopology/InjectiveTypes.index.html

[2] https://doi.org/10.1017/S0960129520000225

What I want to do in this thread is to quickly review what I did in that paper and then list some new results about injectivity that I have developed in TypeTopology that haven't been published yet.

(This was a longer introduction than I intended!)

11/

In some sense, the main examples of injective types are universes.

Every universe 𝓤 is injective.

Products Πᵢ Dᵢ of injective types are injective.

In particular, for any type I, if D is injective then the "exponential power" (I → D) of D is injective.

Injective types are closed under retracts.

And any injective type is a retract of an exponential power of some universe.

So the injective types are precisely the retracts of exponential powers of universes.

Another source of examples is the "lifting monad" also known as the partial-map-classifier monad.

Given any type X, we can consider the type 𝓛 X of partial elements of X, which consists of triples (P , i , f) such that P is a type, i witnesses the fact that P is a subsingleton (type with at most one element), and f is a function P → X.

The injective spaces are precisely the types that can be equipped with an Eilenberg-Moore 𝓛-algebra structure.

I deliberately omitted universe levels in this discussion, for simplicity. For full details, see the Agda code or the published paper, where the above discussion is conducted much more carefully than I want to do here.

However, for people who care about (9.1) (∞-toposes) but not about (9.2) (computation), this doesn't make any difference. The reason is that ∞-toposes satisfy "propositional resizing", and under this assumption injectivity is universe-level independent. This is also discussed in the Agda code and the paper.

(At present, there is no known computational realization of propositional resizing in HoTT/UF.)

12/

I now move to the new, unpublished results that have been collected in TypeTopology, and refereed by Agda (for correctness, but not for originality or relevance or whatever else peer reviewing in mathematics requires).

The main results are about new examples of injective types.

I list them here:

(13.1) The type of ordinals is injective.

This is the original motivation for this work. I wanted to construct plenty of "searchable" or "compact" types, which I discussed in other threads. Injectivity is a main tool for that purpose.

But this wasn't included in the above publication.

(13.2) The types of iterative multisets and of iterative sets (in the sense of Aczel with its incarnation à la Gylterud) are injective.

(13.3) The following are also injective:

* The type of pointed types.
* The type of ∞-magmas.
* The type of pointed magmas.
* The type of monoids.

(13.4) And, moreover, I proved (13.3) by developing a couple of general injectivity theorems, that are a bit technical to discuss here, but that basically say that mathematical structures that are closed under products of the underlying sets, with the underlying operations defined pointwise, form injective types. The true theorems are a bit more general than that.

They imply (although I haven't formalized this conclusion in Agda) that e.g. the type groups, the type of posets, and many more things like that, are all injective.

13/

I suspect that the type of (univalent) 1-categories is also injective, although I only have sketches of ideas of why this would be so in my mind at this stage.

These facts and ideas, as I said, are unpublished, but they are available at TypeTopology with English prose discussions and Agda code.

https://www.cs.bham.ac.uk/~mhe/TypeTopology/InjectiveTypes.index.html

14/

Here is another application of injectivity. People wondered whether the type of ordinals satisfies desirable decidability conditions.

Can you decide, constructively, whether an ordinal is zero? Or a limit ordinal? Etc.

I proved in TypeTopology, in August 2022, that the type of ordinals has some non-trivial decidable property if and only if De Morgan Law (= the negation of every proposition is decidable) [1].

So the type of ordinals is indecomposable, like the type of Dedekind real numbers and other types of real numbers.

But this actually follows from the fact that the type of ordinals is injective [1].

If a type is injective, then the existence of a non-trivial decidable property implies that De Morgan Law holds.

There are very few De Morgan toposes in the current mathematical zoo of toposes.

And De Morgan Law is certainly not "computational".

By the above, also the types of magmas, monoids, groups, posets, etc. don't have non-trivial decidable properties unless De Morgan Law holds.

[1] https://www.cs.bham.ac.uk/~mhe/TypeTopology/Taboos.Decomposability.html

End for now, but I may include further discussion if anything comes to my mind.

15/

@nilesjohnson Yes, I know! What I was wondering is what the first use of injectivity, and the terminology "injective" for objets is. Are injective modules the first appearence? In the early 1970's Dana Scott characterized the continuous lattices as the injectiveT0 topological spaces over subspace embeddings. Injectivity, in one way or another, also makes appearences in homotopy theory.

@MartinEscardo oh, haha, I completely misunderstood what you meant about not knowing the source of the terminology!

@OscarCunningham @MartinEscardo - those spaces aren't injective if we use this modified definition:

"A space D is injective if for every embedding j : X → X' and any continuous map f : X → D, we can find a continuous map f' : X' → D that extends f along j, in the sense that f' ∘ j = f."

For example, let D = X be the sphere and j: X → X' be the usual embedding of the sphere in the ball. Let f : X → D be the identity map from the sphere to itself. Then there's no way to extend this to a continuous map from the ball to the sphere. This is a famous result of Brouwer, now a textbook application of homology groups.

But I'm not sure what definition of "embedding" Martin is using, and how it differs from the usual definition in topology. The usual definition in topology is not homotopy-invariant! And I doubt that any homotopy-invariant definition of "embedding" will let us embed the sphere in a ball, since the ball is homotopy equivalent to a point.

@johncarlosbaez @MartinEscardo @OscarCunningham "But I'm not sure what definition of 'embedding' Martin is using". I think it must be just the ∞-categorical notion of monomorphism, which in the ∞-category of spaces boils down to this: a map j : X → Y is a monomorphism if X is the disjoint union of some of the path components of Y and j is the inclusion. And I think a space is injective if and only if it has a point:

- If D is injective then considering ∅ → pt, you see D has a point.

- And if D has a point p, then every map X → D can be extended along an arbitrary monomorphism X → X' by sending the path components of X' outside X to p.

So, I think this notion of injective is not interesting for spaces. In fact, what I said goes through as soon as you have the law of excluded middle, so this notion of injective type is really only interesting constructively. If you want to think about it in some specific ∞-topos, try sheaves of spaces on S¹.

EDIT: Apparently I can't read: Martin already explained in the thread that under excluded middle injective = inhabited. Sorry for the repetition.

@MartinEscardo @johncarlosbaez @OscarCunningham Nor is it an embedding (= (-1)-truncated map), right? (The homotopy fiber over any point of 𝐑≃1 is all of 𝐐, which is not a proposition — or are you thinking of something else than topological spaces up to weak homotopy equivalence?)

@at @johncarlosbaez @OscarCunningham

Oh. OK. This needs to be clarified (again and again) and is a fair question.

When you define the Dedekind reals in HoTT/UF, you don't get the homotopy type of the real line (which is contractible).

You get a non-contractible 0-truncated type.

There is a long and interesting mathematical story to be told here, but I will save this for another thread in the future.

In connection with this, it is perhaps worth mentioning Mike Shulman's cohesive homotopy type theory.

https://ncatlab.org/nlab/show/cohesive+homotopy+type+theory

@isAdisplayName Thanks for paying attention. I think I've fixed it now. If not then complain again please.