Path Types & Transport

The most important chapter in this book. Paths are the foundation of everything Deppy does — they turn equality from a proposition into a structure.

What Is a Path?

In everyday mathematics a path is a continuous curve connecting two points. You can picture it: a line drawn from point A to point B on a surface. The line is evidence that A and B are connected.

In homotopy type theory we take this literally. An equality proof between two values a and b of type A is a path — a continuous map from the unit interval 𝕀 = [0, 1] into the space A, sending 0 to a and 1 to b.

A path is not a fact that two things are equal — it is a construction that witnesses their equality and records how they are related.

This distinction matters enormously. In classical logic, 3 + 4 = 7 and 2 + 5 = 7 are both just "true". In path-based equality, each has a different path — the computation 3 + 4 ↝ 7 is different evidence than 2 + 5 ↝ 7. The paths remember the computation.

PathType(A, x, y) — The Type of Paths

In Deppy the type of paths between x and y in type A is written:

PathType(A, x, y)

A term p : PathType(A, x, y) is evidence that x and y are equal in type A. The type A matters: two values can be equal in one type but not in another (just as two Python objects can be equal under one protocol but not another).

from deppy.core import PathType, Refl, Sym, Trans, Cong, Ap

# Reflexivity: every value is equal to itself
p1 : PathType(int, 42, 42) = Refl(42)

# A computed path: 3+4 = 7
p2 : PathType(int, 3 + 4, 7) = Refl(7)
# β-reduction makes 3+4 and 7 definitionally equal

Path Constructors

Deppy provides six fundamental constructors for building paths. Every path that Deppy ever constructs is ultimately built from these primitives.

Refl — Reflexivity

The simplest path: every value is equal to itself.

Refl(a) : PathType(A, a, a)

# "a = a because... it just is."
# As an interval function: λ i. a  (constant function)

Refl is the identity path. It is the zero-length loop at a point. Computationally, Refl(a) is the constant function that returns a regardless of the interval parameter.

Sym — Symmetry (Path Inverse)

If p : a = b, then Sym(p) : b = a. Equality is symmetric — you can walk a path backwards.

Sym(p) : PathType(A, b, a)

# As an interval function: λ i. p(1 - i)
# At i=0: p(1) = b.  At i=1: p(0) = a.  ✓

# Example
p   : PathType(int, 7, 3 + 4)  # 7 = 3+4
p_inv = Sym(p)                     # 3+4 = 7

Trans — Transitivity (Path Composition)

If p : a = b and q : b = c, then Trans(p, q) : a = c. You can chain paths end-to-end.

Trans(p, q) : PathType(A, a, c)

# Notation: p · q  (path composition)
# As an interval function: walk p for i ∈ [0, 0.5], then q for i ∈ [0.5, 1]

# Example: chain of equalities
p : PathType(int, 2+3, 5)    # 2+3 = 5
q : PathType(int, 5, 10//2)  # 5 = 10//2
r = Trans(p, q)                # 2+3 = 10//2

Cong — Congruence

If p : a = b and f is a function, then Cong(f, p) : f(a) = f(b). Functions preserve equality.

Cong(f, p) : PathType(B, f(a), f(b))

# As an interval function: λ i. f(p(i))
# Apply f pointwise along the path

# Example
p : PathType(int, 3, 3)         # 3 = 3 (Refl)
double = lambda x: x * 2
q = Cong(double, p)                # double(3) = double(3), i.e., 6 = 6

# More interesting example
p2 : PathType(int, 2+1, 3)       # 2+1 = 3
q2 = Cong(double, p2)              # double(2+1) = double(3), i.e., 6 = 6

Ap — Application to Paths

Ap is the dependent version of Cong. Given a dependent function f : Π(x:A). B(x) and a path p : a =A b, we get a path over p from f(a) to f(b).

Ap(f, p) : PathOver(B, p, f(a), f(b))

# PathOver is a "path that lies above another path"
# It accounts for the fact that f(a) : B(a) and f(b) : B(b)
# live in DIFFERENT types when B depends on the input.

# Example: a function from numbers to their string names
def name(n: int) -> str:
    names = {1: "one", 2: "two", 3: "three"}
    return names.get(n, str(n))

# Ap(name, refl(2)) : name(2) = name(2)

PathAbs & PathApp — Cubical Path Abstraction

In cubical type theory, paths are literally functions from the interval. PathAbs constructs a path by abstracting over the interval variable, and PathApp evaluates a path at a point.

# PathAbs: construct a path from a lambda over 𝕀
p = PathAbs("i", lambda i: interp(a, b, i))
# p : PathType(A, a, b)
# Boundary conditions: p(0) = interp(a, b, 0) = a
#                      p(1) = interp(a, b, 1) = b

# PathApp: evaluate a path at a specific interval point
PathApp(p, 0)    # → a
PathApp(p, 1)    # → b

# This is the key computational content:
# paths are not opaque tokens — they COMPUTE.

Path Composition in Detail

Path composition p · q (Trans) is the workhorse of equational reasoning. Here's how it works in Deppy:

# Given: p : a = b  and  q : b = c
# We want: a = c

# Algebraically:
composed = Trans(p, q)  # a = c

# As an interval function (cubical):
# composed(i) = { p(2i)       if i ≤ 0.5
#               { q(2i - 1)   if i ≥ 0.5

# Verification example: chain of equalities for a sorting proof
step1 : PathType(list[int], sort([3,1,2]), [1,2,3])  # sort([3,1,2]) = [1,2,3]
step2 : PathType(list[int], [1,2,3], sorted([3,1,2]))  # [1,2,3] = sorted([3,1,2])
combined = Trans(step1, step2)   # sort([3,1,2]) = sorted([3,1,2])

Path Algebra Laws

Paths satisfy groupoid laws (up to higher paths):

Transport — THE Key Operation

If paths are the nouns of HoTT, transport is the verb. Transport is what makes paths useful: it lets you carry data and proofs from one point to another along a path.

transport(P, p, x)
  # P : A → Type     — a type family (property) indexed by A
  # p : PathType(A, a, b)  — a path from a to b
  # x : P(a)         — a value/proof at the starting point
  # Result: P(b)     — the corresponding value/proof at the endpoint

In words: if P is some property that depends on a value in A, and you have a proof that P holds at point a, and you have a path from a to b, then transport gives you a proof that P holds at point b.

Transport Example: Sorting

# We've verified that insertion_sort produces a sorted list
proof_isort : Sorted(insertion_sort(xs))

# We have a path: insertion_sort and merge_sort produce the same output
# (proved via function extensionality — see below)
p_equiv : PathType(
    list[int],
    insertion_sort(xs),
    merge_sort(xs)
)

# Transport the "Sorted" property along the path
proof_msort : Sorted(merge_sort(xs)) = transport(
    Sorted,      # the property to transport
    p_equiv,     # the path to transport along
    proof_isort  # the proof at the starting point
)

# merge_sort is verified! We reused the insertion_sort proof.

Transport Example: List ↔ Tuple

# Property: "all elements are positive"
AllPositive = lambda container: all(x > 0 for x in container)

# Proof that my_list has all positive elements
my_list = [1, 2, 3]
proof_list : AllPositive(my_list) = ... # verified by Z3

# Path between list and tuple (as Iterables, they're equivalent)
p : PathType(Iterable[int], my_list, (1, 2, 3))
p = duck_path(Iterable[int], my_list, (1, 2, 3))

# Transport: AllPositive(my_list) → AllPositive((1, 2, 3))
proof_tuple = transport(AllPositive, p, proof_list)

# The tuple is verified without re-checking every element!

When Transport Fails

Transport can only carry a property P along a path p : a =A b if P is invariant under the equivalence that p represents. If P depends on structure that the path does not preserve, transport fails — and this failure is a type error, caught at verification time.

# This will FAIL:
HasAppendMethod = lambda container: hasattr(container, "append")

proof_list_has_append : HasAppendMethod(my_list)  # ✓ lists have .append()

# Try to transport to tuple...
proof_tuple_has_append = transport(HasAppendMethod, p, proof_list_has_append)
# ❌ TYPE ERROR: HasAppendMethod is not invariant under the Iterable path.
# The path p only preserves Iterable operations (__iter__, __next__).
# .append() is not part of Iterable, so it can't be transported.

Function Extensionality (FunExt)

Function extensionality is the principle that two functions are equal if they produce equal outputs on all inputs:

FunExt: If ∀ x. f(x) = g(x), then f = g.

This sounds obvious, but it is not provable in many type theories (including vanilla Martin-Löf type theory). In cubical HoTT it is a theorem, and in Deppy it is a fundamental building block.

from deppy.core import funext

# Two implementations of doubling
f = lambda x: x + x
g = lambda x: x * 2

# Pointwise proof: for every x, f(x) = g(x)
pointwise : Π(x:int). PathType(int, x + x, x * 2)
pointwise = lambda x: z3_prove(x + x == x * 2)

# FunExt lifts pointwise equality to function equality
p : PathType(int -> int, f, g) = funext(pointwise)

# Now f and g are EQUAL as functions.
# Any proof about f can be transported to g.

FunExt for Higher-Order Python

Function extensionality is especially powerful for Python's rich ecosystem of higher-order functions:

# Prove that map(f, xs) = [f(x) for x in xs] for all f, xs

map_version = lambda f, xs: list(map(f, xs))
comp_version = lambda f, xs: [f(x) for x in xs]

# Pointwise: for any specific f and xs, they produce the same list
pointwise_proof = lambda f, xs: list_map_comprehension_equiv(f, xs)

# FunExt (applied twice — once for f, once for xs):
p = funext(lambda f: funext(lambda xs: pointwise_proof(f, xs)))

# Result: map_version = comp_version  as functions
# Any property verified for map(f, xs) transfers to comprehension

Univalence — The Crown Jewel

Univalence is the most powerful principle in homotopy type theory. It says:

Univalence: If A ≃ B (A and B are equivalent types — there's a structure-preserving bijection between them), then A = B in the universe of types.

This is a profound statement. It says that equivalent types are identical. Two types that have the same structure are not merely "isomorphic" — they are equal, and any property of one is automatically a property of the other.

from deppy.core import univalence, Equiv

# Equivalence: dict ≃ OrderedDict for read operations
# (Both support __getitem__, __contains__, keys(), values(), items())

read_equiv : Equiv(ReadableMapping[str, int],
                   dict[str, int],
                   OrderedDict[str, int])

# Univalence: equivalence → equality
p : PathType(Type,
    dict[str, int],
    OrderedDict[str, int]
) = univalence(read_equiv)

# Now ANY property of dict (for read operations) transfers to OrderedDict
# and vice versa — automatically, via transport along p.

Univalence in Practice

Univalence lets Deppy perform powerful proof transfer between types. The most common applications:

Worked Examples

Example 1: Two Sorting Algorithms Are Equivalent

from deppy import guarantee
from deppy.core import PathType, funext, transport

@guarantee("output is a sorted permutation of input")
def insertion_sort(xs: list[int]) -> list[int]:
    result = list(xs)
    for i in range(1, len(result)):
        key = result[i]
        j = i - 1
        while j >= 0 and result[j] > key:
            result[j + 1] = result[j]
            j -= 1
        result[j + 1] = key
    return result

@guarantee("output is a sorted permutation of input")
def merge_sort(xs: list[int]) -> list[int]:
    if len(xs) <= 1:
        return list(xs)
    mid = len(xs) // 2
    left = merge_sort(xs[:mid])
    right = merge_sort(xs[mid:])
    return merge(left, right)

Example 2: Lambda Equivalence via FunExt

# Two lambda expressions
f = lambda xs: sorted(set(xs))
g = lambda xs: list(dict.fromkeys(sorted(xs)))

# Both remove duplicates and sort.  Are they equal?

# Pointwise: for any list xs, sorted(set(xs)) = list(dict.fromkeys(sorted(xs)))
# Z3 can verify this for finite domains; oracle for general case
pw = lambda xs: verify_set_fromkeys_equiv(xs)

# FunExt gives us the path
p : PathType(
    list[int] -> list[int],
    f, g
) = funext(pw)

# If f is verified correct, g is correct via transport
proof_g = transport(Correct, p, proof_f)

Example 3: Transport Across Container Types

# Verified: sum of a list of positive ints is positive
@guarantee("result > 0 when all elements > 0 and len(xs) > 0")
def positive_sum(xs: list[int]) -> int:
    return sum(xs)

# We want to use this with a tuple too.
# Construct a path: list and tuple are equivalent as Iterables
p = duck_path(Iterable[int], [1,2,3], (1,2,3))

# Transport the property
# "positive_sum is correct" → "positive_sum is correct on this tuple"
# (Here positive_sum uses only Iterable operations: iteration via sum())
proof_tuple = transport(PositiveSumCorrect, p, proof_list)

J-Elimination (Path Induction)

J-elimination (also called path induction) is the fundamental elimination principle for path types. It says: to prove something about all paths, it suffices to prove it for the reflexivity path refl(a).

# J-elimination principle:
#
# Given:
#   C : Π(x:A). Π(y:A). (x =_A y) → Type    — a motive
#   d : Π(a:A). C(a, a, refl(a))              — base case for refl
#
# Then for any x, y : A and p : x =_A y:
#   J(C, d, x, y, p) : C(x, y, p)

# In Python terms: to prove a property about all equalities,
# just prove it for the "obvious" equality (refl).

# Example: prove that Sym(Sym(p)) = p for any path p
# It suffices to show Sym(Sym(refl(a))) = refl(a)
# But Sym(refl(a)) = refl(a), so Sym(Sym(refl(a))) = Sym(refl(a)) = refl(a) ✓

Summary: The Path Toolkit

def f(d: dict) -> list: return sorted(d.keys())
def g(d: dict) -> list: return sorted(list(d))