Homotopy Type Theory limit of a binary function approaching a diagonal > history (Rev #1)

Contents

Definition

Let TT be a function limit space with a tight apartness relation #\# and let STS \subseteq T be a subtype of TT. Let us define the subtype Δ #(S)S×S\Delta_{\#}(S) \subseteq S \times S of pairs of elements apart from the diagonal as

Δ #(S) (x,y):S×Sx#y\Delta_{\#}(S) \coloneqq \sum_{(x,y):S \times S} x \# y

Given a partial binary function q:Δ #(S)Tq:\Delta_{\#}(S) \to T, the currying of qq results in the dependent functions

x:Sq(x):( y:Sx#y)Tx:S \vdash q(x): \left(\sum_{y:S} x \# y\right) \to T

A function g:STg:S \to T is a limit of qq approaching the diagonal if for all x:Sx:S the limit of the dependent function q(x)q(x) approaching xx is g(x)g(x). We can define a predicate that the qq has a limit approaching the diagonal as

hasLimitApproachingDiagonal(q)[ g:SF x:Slim yxq(x)(y)=g(x)]hasLimitApproachingDiagonal(q) \coloneqq \left[\sum_{g:S \to F} \prod_{x:S} \lim_{y \to x} q(x)(y) = g(x)\right]

The type of all functions in Δ #(S)F\Delta_{\#}(S) \to F that have a limit approaching the diagonal is defined as

DiagonalLimitFunc(S,T) q:Δ #(S)ThasLimitApproachingDiagonal(q)DiagonalLimitFunc(S, T) \coloneqq \sum_{q:\Delta_{\#}(S) \to T} hasLimitApproachingDiagonal(q)

As a result, there exists a function

lim (x,y)(x,x)()(x,y):DiagonalLimitFunc(S,T)(SF)\lim_{(x, y) \to (x, x)} (-)(x, y): DiagonalLimitFunc(S, T) \to (S \to F)

which returns the limit of a partial binary function q:DiagonalLimitFunc(S,T)(Δ #(S)T)q:DiagonalLimitFunc(S, T) \subseteq (\Delta_{\#}(S) \to T) approaching the diagonal.

See also

Revision on April 16, 2022 at 07:39:26 by Anonymous?. See the history of this page for a list of all contributions to it.