embedding of types in nLab

Contents

Idea

The analogue in dependent type theory of the concept of injection in set theory, embedding of topological spaces in topology, and embedding in category theory.

This is similar to equivalence of types, which are the analogues in dependent type theory of the concept of bijection in set theory, homeomorphism in topology, and isomorphism in category theory.

Definition

Given types AA and BB, a function f:A→Bf:A \to B is an embedding if one of the following equivalent conditions holds of ff:

• for all x:Ax:A and y:Ay:A, application of the function ff to identifications between xx and yy is an equivalence of types;

isEmbedding(f)≔∏ x:A∏ y:AisEquiv(ap f(x,y))\mathrm{isEmbedding}(f) \coloneqq \prod_{x:A} \prod_{y:A} \mathrm{isEquiv}(\mathrm{ap}_f(x, y))

• for all y:By:B, the fiber of ff at yy is a mere proposition

isEmbedding(f)≔∏ y:BisProp(∑ x:Af(x)= By)\mathrm{isEmbedding}(f) \coloneqq \prod_{y:B} \mathrm{isProp}\left(\sum_{x:A}f(x) =_B y\right)

Properties

Relation to subtypes

Given a type of propositions Prop\mathrm{Prop} and a material subtype P:A→PropP:A \to \mathrm{Prop}, the corresponding structural subtype of AA is defined by

∑ x:Ax∈P\sum_{x:A} x \in P

and the embedding is given by the first projection function

π 1:(∑ x:Ax∈P)→A\pi_1:\left(\sum_{x:A} x \in P\right) \to A

with the witness that π 1\pi_1 is an embedding given by the fact that the membership relation x∈Px \in P is a proposition for all elements x:Ax:A and material subtypes P:A→PropP:A \to \mathrm{Prop}.

• embedding type

• injection, embedding of topological spaces, embedding of smooth manifolds, embedding

• equivalence of types

• subtype, predicate

References

For embeddings in dependent type theory, see section 11.4 of:

• Egbert Rijke, Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (arXiv:2212.11082)