[[!redirects monic]] [[!redirects monomorphism]] [[!redirects n-monic]] [[!redirects n-monomorphism]] [[!redirects n-monic function]] [[!redirects subtype]] [[!redirects supertype]] [[!redirects subset]] [[!redirects superset]] ## Definition ## Given a natural number $n:\mathbb{N}$ and types $A$ and $B$, a function $f:A \to B$ is a __$n$-monic function__ if for all terms $b:B$ the [[fiber]] of $f$ over $b$ has an [[homotopy level]] of $n$. $$isMonic(n, f) \coloneqq \prod_{b:B} hasHLevel(n, fiber(f, b))$$ A [[equivalence]] is a $0$-monic function. $1$-monic functions are typically just called __monic functions__. The type of all $n$-monic functions with domain $A$ and codomain $B$ is defined as $$monic(n, A, B): \sum_{f:A \to B} isMonic(n, f)$$ For every natural number $n:\mathbb{N}$, $monic(n, A, B)$ has a homotopy level of $n$. In particular, the type of all monic functions with domain $A$ and codomain $B$, defined as $$A \subseteq B \coloneqq monic(1, A, B)$$ is a [[proposition]]. $A$ is called a __subtype__ of $B$, and $B$ is called a __supertype__ of $A$. If $A$ and $B$ are [[set]]s, then $A$ is a __subset__ of $B$ and $B$ is a __superset__ of $A$. ## See also ## * [[fiber]] * [[epic function]] * [[effective epic function]] * [[lower type]] * [[upper type]]