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

Definition

Given a natural number n:n:\mathbb{N} and types AA and BB, a function f:ABf:A \to B is a nn-monic function if for all terms b:Bb:B the fiber of ff over bb has an homotopy level of nn.

isMonic(n,f) b:BhasHLevel(n,fiber(f,b))isMonic(n, f) \coloneqq \prod_{b:B} hasHLevel(n, fiber(f, b))

A equivalence is a 00-monic function. 11-monic functions are typically just called monic functions or inclusions.

The type of all nn-monic functions with domain AA and codomain BB is defined as

monic(n,A,B): f:ABisMonic(n,f)monic(n, A, B): \sum_{f:A \to B} isMonic(n, f)

Given types AA and BB, AA is called a subtype of BB, and BB is called a supertype of AA, if monic(1,A,B)monic(1, A, B) is inhabited. We define the proposition of subtype inclusion as

AB[monic(1,A,B)]A \subseteq B \coloneqq \left[monic(1, A, B)\right]

where [T]\left[T\right] is the propositional truncation of TT. If AA and BB are sets, then AA is a subset of BB and BB is a superset of AA.

The type of all subtypes of BB in a universe is defined as

Sub 𝒰(B) A:𝒰𝒯 𝒰(A)BSub_\mathcal{U}(B) \coloneqq \sum_{A:\mathcal{U}} \mathcal{T}_\mathcal{U}(A) \subseteq B

See also

Revision on June 15, 2022 at 22:56:16 by Anonymous?. See the history of this page for a list of all contributions to it.