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

Showing changes from revision #6 to #7: Added | Removed | Changed

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 or inclusions.

The type of all $n$-monic functions with domain $A$ and codomain $B$ is defined as

For Given every types natural number$\mathrm{<span><del\; class="diffmod">\; n</del><ins\; class="diffmod">\; A</ins></span>}:\mathbb{N}$ n:\mathbb{N} A , and$\mathrm{monic}(n,A,B)$ monic(n, B A, B) , has a homotopy level of$\mathrm{<span><del\; class="diffmod">\; n</del><ins\; class="diffmod">\; A</ins></span>}$ n A . is called asubtype of $B$, and $B$ is called a supertype of $A$, if $monic(1, A, B)$ is inhabited. We define the proposition of subtype inclusion as