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

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$.

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

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

is a proposition. $A$ is called a subtype of $B$, and $B$ is called a supertype of $A$. If $A$ and $B$ are sets, 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
• partial function