Background
Basic concepts
equivalences in/of -categories
Universal constructions
Local presentation
Theorems
Extra stuff, structure, properties
Models
For a morphism in an (infinity,1)-category is an -monomorphism equivalently if
in its n-image factorization
the first morphism is an equivalence in an (infinity,1)-category
it is an (n-2)-truncated morphism;
In homotopy type theory, a function is an -monomorphism if its -image factorization is via an equivalence in homotopy type theory.
More explicitly, given a natural number and types and , a function is a -monomorphism if for all terms the fiber of over has an homotopy level of .
A equivalence is a -monomorphism. -monomorphisms are typically just called monomorphisms or embeddings.
The type of all -monomorphisms with domain and codomain is defined as
The dual concept is that of n-epimorphism.
-monomorphism are precisely the equivalences.
Every morphism is an -monomorphism.
1-monomorphisms are often just called monomorphisms in an (∞,1)-category. The 1-monomorphisms into a fixed object are called the subobjects of that object.
A 1-monomorphism between 0-truncated objects is precisely an ordinary monomorphism in the underlying 1-topos.
Last revised on November 18, 2023 at 05:10:13. See the history of this page for a list of all contributions to it.