nLab n-monomorphism




For nn \in \mathbb{N} a morphism f:XYf \colon X \to Y in an (infinity,1)-category is an nn-monomorphism equivalently if

In homotopy type theory

In homotopy type theory, a function f:XYf \colon X \to Y is an nn-monomorphism if its nn-image factorization is via an equivalence in homotopy type theory.

More explicitly, given a natural number n:n:\mathbb{N} and types AA and BB, a function f:ABf:A \to B is a nn-monomorphism if for all terms b:Bb:B the fiber of ff over bb has an homotopy level of nn.

isMonic(n,f) b:BhasHLevel(n,fiber(f,b))isMonic(n, f) \coloneqq \prod_{b:B} hasHLevel(n, fiber(f, b))

A equivalence is a 00-monomorphism. 11-monomorphisms are typically just called monomorphisms or embeddings.

The type of all nn-monomorphisms with domain AA and codomain BB is defined as

Monos(n,A,B): f:ABisMonic(n,f)Monos(n, A, B): \sum_{f:A \to B} isMonic(n, f)

Dual concept

The dual concept is that of n-epimorphism.


Last revised on June 17, 2022 at 21:56:42. See the history of this page for a list of all contributions to it.