Let be a function limit space with a tight apartness relation and let be a subtype of . Let us define the subtype of pairs of elements apart from the diagonal as
Given a partial binary function , the currying of results in the dependent functions
A function is a limit of approaching the diagonal if for all the limit of the dependent function approaching is . We can define a predicate that the has a limit approaching the diagonal as
The type of all functions in that have a limit approaching the diagonal is defined as
As a result, there exists a function
which returns the limit of a partial binary function approaching the diagonal.