Homotopy Type Theory monic function > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

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 fiber of a function $f:A \to B$ over $b: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?
• lower poset?
• upper poset?