[[!redirects monic]] [[!redirects monomorphism]] [[!redirects n-monic]] [[!redirects n-monomorphism]] [[!redirects n-monic function]] [[!redirects inclusion]] [[!redirects subtype]] [[!redirects supertype]] [[!redirects subset]] [[!redirects superset]] [[!redirects type of subtypes]] ## 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__ or __inclusions__. 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)$$ Given types $A$ and $B$, $A$ is called a __subtype__ 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 $$A \subseteq B \coloneqq \left[monic(1, A, B)\right]$$ where $\left[T\right]$ is the propositional truncation of $T$. If $A$ and $B$ are [[set]]s, then $A$ is a __subset__ of $B$ and $B$ is a __superset__ of $A$. The type of all subtypes of $B$ in a universe is defined as $$Sub_\mathcal{U}(B) \coloneqq \sum_{A:\mathcal{U}} \mathcal{T}_\mathcal{U}(A) \subseteq B$$ ## See also ## * [[fiber]] * [[epic function]] * [[effective epic function]] * [[lower type]] * [[upper type]] * [[partial function]]