Homotopy Type Theory monic function > history (Rev #1)

Definition

Given a natural number $n:\mathbb{N}$, a function $f:A \to B$ is a $n$-monic function if for all terms $b:B$ the homotopy fiber of a function $f:A \to B$ over $b:B$ has an homotopy level of $n$.

A homotopy equivalence is a $0$-monic function. $1$-monic functions are typically just called monic functions.

See also

• homotopy fiber
• epic function?