Homotopy Type Theory limit of a net > history (Rev #4, changes)

Skip the Navigation Links | Home Page | All Pages | Latest Revisions | Authors |

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

Contents

Definition

In premetric spaces

Let TT be a directed type, and let SS be a TT-premetric space. Given a directed type II, a limit of a net x:I→Sx: I \to S is a term l:Sl:S with

λ:∏ ϵ:T‖∑ N:I∏ i:I(i≥N)→(x i∼ ϵl)‖\lambda: \prod_{\epsilon:T} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (x_i \sim_{\epsilon} l) \Vert

Cauchy approximations

Let T A T A be a directed abelian type group and with a pointcodirected type1:A1:A , where a the directed type operation⊕\oplusstrict order is associative. A limit of aT< T \lt - , a termCauchy approximationζ:0<1\zeta: 0 \lt 1 and a family of dependent termsx:T→Sx: T \to S is a term l:Sl:S with

x a: T A → , S b:A⊢ c α( x a,b):∏ δ:T(∏ η:T0x δ<∼ δ⊕ηal)×(0<b)→(0<a+b) x:T a:A, \to b:A S \vdash c(x):\prod_{\delta:T} \alpha(a, \prod_{\eta:T} b):(0 x_\delta \lt \sim_{\delta a) \oplus \times \eta} (0 l \lt b) \to (0 \lt a + b)

Let A +≔∑ a:A(0<a)A_{+} \coloneqq \sum_{a:A} (0 \lt a) be the positive cone? of AA.

A limit of a A +A_{+}-Cauchy approximation x:A +→Sx: A_{+} \to S is a term l:Sl:S with
x:A +→S⊢c(x):∏ δ:A +∏ η:A +x δ∼ δ⊕ηlx:A_{+} \to S \vdash c(x):\prod_{\delta:A_{+}} \prod_{\eta:A_{+}} x_\delta \sim_{\delta \oplus \eta} l

In convergence spaces

…

Sequences

A limit of a sequence is a limit of a net that happens to be a sequence.

See also

Revision on March 12, 2022 at 21:33:15 by Anonymous?. See the history of this page for a list of all contributions to it.

DiscussNext revision (13 more)Previous revision (3 more)Current version of pageHide changesHistory (16 revisions)Rollback Source