Equality & Path Types

The conceptual heart of Deppy — identity types, path types, and the bridge between homotopy type theory and Python verification.

Identity Types

In ordinary Python, == is a runtime boolean test. In dependent type theory, equality is a type: the proposition "x equals y" is itself a type, and a proof that x == y is a term inhabiting that type.

from __future__ import annotations
from deppy.types import PathType, Refl, Sym, Trans, Cong
from deppy.types import Ap, Transport, J, FunExt, Univalence
from deppy import guarantee, check
from typing import TypeVar

A = TypeVar('A')
B = TypeVar('B')

# PathType(A, x, y) is the type of proofs that x = y in type A
# Read: "a path from x to y in the space A"

Reflexivity — Every Point Has a Path to Itself

# Refl(x) : PathType(A, x, x)
# "x equals x" — the trivial path (constant loop)

def equality_is_reflexive(x: A) -> PathType[A, x, x]:
    return Refl(x)
# Deppy verifies: Refl(x) inhabits PathType(A, x, x)  ✅

Symmetry — Paths Are Reversible

# If p : PathType(A, x, y), then Sym(p) : PathType(A, y, x)
# "If x = y, then y = x"

@guarantee("symmetry of equality")
def equality_is_symmetric(
    p: PathType[A, x, y]
) -> PathType[A, y, x]:
    return Sym(p)

Transitivity — Paths Compose

# If p : PathType(A, x, y) and q : PathType(A, y, z),
# then Trans(p, q) : PathType(A, x, z)
# "If x = y and y = z, then x = z"

@guarantee("transitivity of equality")
def equality_is_transitive(
    p: PathType[A, x, y],
    q: PathType[A, y, z],
) -> PathType[A, x, z]:
    return Trans(p, q)

Congruence — Functions Respect Equality

# If f : A → B and p : PathType(A, x, y),
# then Ap(f, p) : PathType(B, f(x), f(y))
# "If x = y, then f(x) = f(y)" for any function f

@guarantee("functions preserve equality")
def congruence(
    f: Callable[[A], B],
    p: PathType[A, x, y],
) -> PathType[B, f(x), f(y)]:
    return Ap(f, p)

# Also available as Cong(f, x, y) for convenience:
# Cong(f, p) is the same as Ap(f, p)

J-Elimination — The Induction Principle for Equality

The J rule (path induction) is the fundamental elimination principle for identity types. It says: to prove a property for all paths, it suffices to prove it for reflexivity.

# J(C, d, p) where:
#   C : (x : A) → (y : A) → PathType(A, x, y) → Type
#   d : (x : A) → C(x, x, Refl(x))
#   p : PathType(A, a, b)
# produces: C(a, b, p)

@guarantee("path induction: reduce any path proof to the refl case")
def j_example(
    x: A,
    y: A,
    p: PathType[A, x, y],
) -> PathType[A, y, x]:
    """Derive symmetry from J."""
    # C(x, y, p) = PathType(A, y, x)
    # d(x) = Refl(x) : PathType(A, x, x)
    return J(
        motive=lambda x, y, _: PathType[A, y, x],
        base=lambda x: Refl(x),
        path=p
    )

Transport — Moving Data Along Paths

If you have a proof that x = y and a value of type P(x), you can transport it to get a value of type P(y).

# Transport(P, p, px) where:
#   P : A → Type    (a type family)
#   p : PathType(A, x, y)
#   px : P(x)
# produces: P(y)

@guarantee("transport along an equality proof")
def transport_example(
    v: Vec[int, n],
    p: PathType[Nat, n, m],  # proof that n = m
) -> Vec[int, m]:
    """If n = m, a Vec of length n is also a Vec of length m."""
    return Transport(
        family=lambda k: Vec[int, k],
        path=p,
        value=v
    )

Function Extensionality

Two functions are equal if they agree on all inputs. This is not automatic in standard type theory — it's an axiom (or a theorem in cubical type theory).

# FunExt(h) where:
#   h : (x : A) → PathType(B, f(x), g(x))
# produces: PathType(A → B, f, g)

@guarantee("pointwise equal functions are equal")
def funext_example(
    f: Callable[[int], int],
    g: Callable[[int], int],
    h: Callable[[int], PathType[int, "f(x)", "g(x)"]],
) -> PathType[Callable[[int], int], f, g]:
    return FunExt(h)

# Example: (λx. x + 0) = (λx. x)
def plus_zero_is_identity():
    f = lambda x: x + 0
    g = lambda x: x
    # Z3 proves ∀x. x + 0 == x
    pointwise = lambda x: Refl(x)  # Z3 discharges this
    return FunExt(pointwise)
# Result: PathType(int → int, (λx. x+0), (λx. x))  ✅

Univalence — Equivalence Is Equality

The univalence axiom is the crown jewel of homotopy type theory. It states: two types that are equivalent (have inverse functions between them) are equal as types.

# If f : A → B is an equivalence (has an inverse g with
# g ∘ f ~ id and f ∘ g ~ id), then:
# Univalence(f, g, ...) : PathType(Type, A, B)

@guarantee("equivalent types are equal")
def univalence_example():
    """
    bool ≃ Literal[0, 1]
    They are equivalent: True↔1, False↔0.
    Therefore, by univalence, they are EQUAL as types.
    """
    to_int   = lambda b: 1 if b else 0
    from_int = lambda n: n == 1

    # Prove round-trip: from_int(to_int(b)) == b for all b
    # Prove round-trip: to_int(from_int(n)) == n for n ∈ {0,1}
    return Univalence(
        forward=to_int,
        backward=from_int,
        # Deppy + Z3 verify the round-trip properties
    )

Path Types in Practice: Python Object Equality

Why does this matter for Python? Because Python has many notions of equality:

Deppy unifies these: is implies == implies behavioural equivalence, each giving a path type at a different level. Univalence lets you transport proofs between duck-type-compatible classes automatically.

# Two classes with the same interface are equivalent
class ArrayStack:
    def push(self, x: int) -> None: ...
    def pop(self) -> int: ...

class LinkedStack:
    def push(self, x: int) -> None: ...
    def pop(self) -> int: ...

# Deppy can prove: ArrayStack ≃ LinkedStack
# Via univalence: PathType(Type, ArrayStack, LinkedStack)
# Any theorem proved about ArrayStack transfers to LinkedStack!

Summary of Path Operations

Exercises