plfa
Embedding is a split monomorphism rather than an injection
In chapter Isomorphism, section Embedding, there is the following definition of an embedding of A into B.
record _≲_ (A B : Set) : Set where
field
to : A → B
from : B → A
from∘to : ∀ (x : A) → from (to x) ≡ x
Meanwhile, a standard definition of an injection from A to B would look like:
record _↪_ (A B : Set) : Set where
field
to : A → B
inj : ∀ {x y : A} → to x ≡ to y → x ≡ y
Lorenzo Lipparini points out, on Agda Zulip, that ⊥ ↪ ⊤ is inhabited, while ⊥ ≲ ⊤ is not. Given that “embedding” is usually taken to be synonymous with “injection”, the definition _≲_ is surprising. Precisely, while _↪_ is equivalent to a monomorphism, _≲_ corresponds to a split monomorphism when “there exists” is read as Σ. A split monomorphism is not a concept I have come across before, and it is likely unfamiliar to readers.
Perhaps the minimal change would be to talk about surjections/epimorphisms rather than injections/monomorphisms. Split epimorphisms (i.e, split monomorphisms in the opposite category) are unproblematic in Martin-Löf type theory because the type-theoretic principle of choice makes them equivalent to epimorphisms (again crucially reading “there exists” as Σ). The definition would be flipped to give:
record _≳_ (A B : Set) : Set where
field
to : A → B
from : B → A
to∘from : ∀ (y : B) → to (from y) ≡ y
I called it an embedding because one often refers to embedding/projection pairs, which is exactly what to and from form.
The point that ⊥ ↪ ⊤ is inhabited, while ⊥ ≲ ⊤ is not is a good one, and perhaps should be added to the text. Would you like to file a pull request to do that?
I'd rather not use the terminology epimorphism/split epimorphism/monomorphism in the text, as it may needlessly scare some readers.
@wadler Maybe we should add the phrase "embedding/projection pair" to the text explicitly? As well as the warning that embedding often refers to an injection, and this is a stronger notion?
Makes sense. (I would do it if "make test" was running, but since it isn't it seems a bit dangerous.)