Fibrations & Fiber Bundles

Model class hierarchies, generic types, and module structures as fibrations — then verify properties per-fiber and conclude globally.

What Is a Fibration?

A fibration is a map p : E → B from a total space E to a base space B, where the key property is that paths in B can be lifted to paths in E.

Think of it like a multi-story building. The base space B is the floor plan. The total space E is the entire building (all floors stacked together). The fibration map p projects a room to its position on the floor plan. The fiber above a point b ∈ B is the column of rooms above that position — one room on each floor.

In type theory: a fibration is a type family P : B → Type. The base is B. The fiber over b : B is P(b). The total space is the dependent sum Σ(b:B). P(b).

The Python Connection

Python's type system is full of fibration structures:

• Class hierarchies: The base is the abstract class. The fibers are the concrete subclasses. The total space is the union of all instances.
• Generic types: list[T] is a type family indexed by T. The base is the set of all types. The fiber over int is list[int].
• Module hierarchies: A package is a fibration. The base is the package namespace. Each module is a fiber.

Formal Definition in Deppy

from deppy.hott import Fibration, TotalSpace, Section
from deppy.core.kernel import Fiber

# A fibration is a type family P indexed by a base type B
# P : B → Type

# Example: class hierarchy as fibration.
# Build the fibration directly from the abstract base class —
# Deppy walks ``__subclasses__()`` to populate the total space.
shape_fibration = Fibration.from_metaclass(Shape)
# shape_fibration.subclasses == [Circle, Rectangle, Triangle]
# shape_fibration.base_space  == Shape

Key Components

Class Hierarchies as Fibrations

The most natural fibration in Python is a class hierarchy. An abstract base class (ABC) defines a base space, and each concrete subclass is a fiber.

from abc import ABC, abstractmethod

class Serializable(ABC):
    @abstractmethod
    def serialize(self) -> bytes: ...

    @abstractmethod
    def deserialize(cls, data: bytes) -> "Serializable": ...

# Five concrete implementations (five fibers)
class JsonDoc(Serializable):
    def serialize(self) -> bytes:
        return json.dumps(self.data).encode()
    def deserialize(cls, data: bytes) -> "JsonDoc":
        return JsonDoc(json.loads(data))

class CsvRow(Serializable): ...
class ProtobufMsg(Serializable): ...
class MsgpackObj(Serializable): ...
class XmlElement(Serializable): ...

# Fibration structure
# Base:  B = {JsonDoc, CsvRow, ProtobufMsg, MsgpackObj, XmlElement}
# Fiber: P(JsonDoc) = set of all JsonDoc instances
#        P(CsvRow)  = set of all CsvRow instances
#        etc.
# Total space: Σ(T:B). P(T) = all Serializable instances
# Section: serialize : Π(T:B). P(T) → bytes

Fiber-by-Fiber Verification

The key benefit of the fibration viewpoint is fiber-by-fiber verification. Instead of proving that serialize works for all possible Serializable objects at once, we prove it per-fiber — once for JsonDoc, once for CsvRow, etc.

# Contract: deserialize(serialize(x)) = x for all Serializable x

# Instead of one hard proof for all Serializable:
# ∀ x:Serializable. deserialize(serialize(x)) = x

# We prove per-fiber:
# ∀ x:JsonDoc.     deserialize(serialize(x)) = x  ✓  (fiber 1)
# ∀ x:CsvRow.      deserialize(serialize(x)) = x  ✓  (fiber 2)
# ∀ x:ProtobufMsg. deserialize(serialize(x)) = x  ✓  (fiber 3)
# ∀ x:MsgpackObj.  deserialize(serialize(x)) = x  ✓  (fiber 4)
# ∀ x:XmlElement.  deserialize(serialize(x)) = x  ✓  (fiber 5)

# Fibration structure guarantees: fiber proofs → global proof

Parametric Polymorphism as Fibration

Python's Generic[T] types form a fibration where the base is the set of all types, and the fiber over each type T is the set of Generic[T] instances at that type.

from typing import Generic, TypeVar
T = TypeVar('T')

class Stack(Generic[T]):
    def __init__(self):
        self._items: list[T] = []

    def push(self, item: T) -> None:
        self._items.append(item)

    def pop(self) -> T:
        return self._items.pop()

    def is_empty(self) -> bool:
        return len(self._items) == 0

# Fibration structure:
# Base:  B = Type (all Python types)
# Fiber: P(int) = Stack[int], P(str) = Stack[str], ...
# Section: push : Π(T:Type). Stack[T] × T → Stack[T]

Verifying Generics Per-Fiber

# Contract: pop() after push(x) returns x
@guarantee("pop after push returns the pushed item")
def push_pop_roundtrip(stack: Stack[T], item: T) -> bool:
    stack.push(item)
    return stack.pop() == item

# Deppy verifies per-fiber:
# 1. For T = int:  push(42); pop() → 42      ✓
# 2. For T = str:  push("hi"); pop() → "hi"  ✓
# 3. For T = list: push([1]); pop() → [1]    ✓
#
# But we don't need to check ALL types — parametricity!
# The generic code doesn't inspect T, so if it works for one T,
# it works for all T.  This is a "free theorem" from parametricity.

Path Lifting

The homotopy lifting property is the defining property of fibrations. It says: if you have a path in the base space, you can lift it to a path in the total space.

# Path in the base: int ≃ float (as numeric types)
base_path : PathType(NumericType, int, float)

# Lifting: this path lifts to a path between Stack[int] and Stack[float]
lifted_path : PathType(StackType, Stack[int], Stack[float])

# Now any proof about Stack[int] transports to Stack[float]!
# transport(StackCorrect, lifted_path, proof_int) : StackCorrect(Stack[float])

In Python terms: if two types are equivalent (via a path), then generic containers over those types are also equivalent. Proofs about Stack[int] transport to Stack[float] via the lifted path.

Application to Python Inheritance

Path lifting gives us the Liskov Substitution Principle as a theorem, not an axiom. If Dog is a subtype of Animal, there is a path from Dog to Animal in the type universe. This path lifts to paths between containers of dogs and containers of animals.

# Subtyping as path in type universe
sub_path : PathType(Type, Dog, Animal)

# Lifts to container types (covariant case)
lifted : PathType(Type, list[Dog], list[Animal])

# A function verified for list[Animal] works for list[Dog]
# via transport along the lifted path
proof_dogs = transport(AllFed, Sym(lifted), proof_animals)

# BUT: contravariant case
# For Callable[[Animal], None], the path goes the OTHER way:
contra_lifted : PathType(Type,
    Callable[[Animal], None],
    Callable[[Dog], None]
)
# A function accepting Animals can be used where Dog-acceptor is expected
# (but NOT vice versa — direction matters!)

Module Hierarchies as Fibrations

A Python package is naturally a fibration:

# Package structure as fibration
#
# mypackage/           ← Total space E
# ├── __init__.py      ← Base space B (package namespace)
# ├── models.py        ← Fiber P("models")
# ├── views.py         ← Fiber P("views")
# ├── controllers.py   ← Fiber P("controllers")
# └── utils.py         ← Fiber P("utils")
#
# Fibration map: each function/class → its containing module
# Section: an import that works across all modules

This is useful for verifying cross-module properties. For example: "every public function in every module has a docstring" can be verified per-fiber (per-module) and concluded globally via the fibration structure.

Full Example: Abstract Base Class with 5 Implementations

from abc import ABC, abstractmethod
from deppy import guarantee

class Collection(ABC):
    @abstractmethod
    def add(self, item) -> None: ...

    @abstractmethod
    def contains(self, item) -> bool: ...

    @abstractmethod
    def size(self) -> int: ...

    @guarantee("after add(x), contains(x) is True and size increases by 1")
    def add_contract(self, item):
        """Contract that all subclasses must satisfy."""
        old_size = self.size()
        self.add(item)
        assert self.contains(item)
        assert self.size() == old_size + 1

# Five implementations (five fibers)
class ListCollection(Collection):
    def __init__(self): self._data = []
    def add(self, item): self._data.append(item)
    def contains(self, item): return item in self._data
    def size(self): return len(self._data)

class SetCollection(Collection):
    def __init__(self): self._data = set()
    def add(self, item): self._data.add(item)
    def contains(self, item): return item in self._data
    def size(self): return len(self._data)

class DictCollection(Collection):
    def __init__(self): self._data = {}
    def add(self, item): self._data[item] = True
    def contains(self, item): return item in self._data
    def size(self): return len(self._data)

class DequeCollection(Collection):
    def __init__(self): self._data = deque()
    def add(self, item): self._data.append(item)
    def contains(self, item): return item in self._data
    def size(self): return len(self._data)

class SortedCollection(Collection):
    def __init__(self): self._data = []
    def add(self, item): bisect.insort(self._data, item)
    def contains(self, item):
        i = bisect.bisect_left(self._data, item)
        return i < len(self._data) and self._data[i] == item
    def size(self): return len(self._data)

Total Spaces and Dependent Pairs

The total space of a fibration is the type of dependent pairs:

# Σ(b:B). P(b)  — the total space
# An element is a pair (b, x) where b:B and x:P(b)

# For the Collection example:
# Σ(T:CollectionType). T
# An element is ("ListCollection", some_list_collection_instance)

# In Python, this is essentially:
def process_any_collection(c: Collection) -> int:
    # c is an element of the total space
    # It has a type tag (which fiber it's from) and a value
    return c.size()

# The type of c is Σ(T:CollectionType). T
# Deppy can pattern-match on the first component (the fiber)
# to dispatch verification to the right fiber proof.

Sections: Functions That Work Across All Fibers

A section of a fibration is a dependent function s : Π(b:B). P(b) — it picks one element from each fiber. In Python terms, a section is a method that works for every subclass.

# Section: a function that works for any Collection subclass
def add_twice(c: Collection, item) -> None:
    c.add(item)
    c.add(item)

# This is a section of the fibration
# add_twice : Π(T:CollectionType). T → item → None
# It must work for every fiber (every concrete Collection)

# Verification: prove per-fiber, conclude globally
# For ListCollection: add_twice adds two copies → size += 2  ✓
# For DequeCollection: same  ✓
# For SetCollection: add_twice might add only one (duplicate!) → check!

Connection to Parametricity and Free Theorems

Parametricity is the idea that a polymorphic function must behave "uniformly" across all type instantiations. In HoTT, this is captured by the fact that a section of a fibration must be natural — it commutes with path lifting.

# Free theorem for a function f : list[T] → list[T]
# If f is parametric (doesn't inspect T), then for any
# function g : A → B:
#
#   map(g, f(xs)) = f(map(g, xs))
#
# This is a "free theorem" — it follows from the TYPE alone,
# without looking at the implementation.

# In fibration terms:
# f is a section of the fibration list : Type → Type
# g induces a path between fibers list[A] and list[B]
# Naturality says: f commutes with this path

# Deppy checks parametricity automatically:
# 1. Analyze function body — does it use isinstance(T)?
# 2. If no type inspection → parametric → free theorems apply
# 3. If yes → not parametric → must verify per-fiber

Fiber Induction

Fiber induction is the elimination principle for fibrations. To prove a property of the total space, it suffices to prove it for each fiber:

# Fiber induction principle:
# Given:
#   P : (Σ(b:B). F(b)) → Type    — a property of the total space
#   d : Π(b:B). Π(x:F(b)). P(b, x)  — proof for each fiber
# Then:
#   Π(e:Σ(b:B). F(b)). P(e)       — proof for the total space

# In Python:
# To prove something about "any Collection":
# 1. Prove it for ListCollection
# 2. Prove it for SetCollection
# 3. Prove it for DictCollection
# 4. Prove it for DequeCollection
# 5. Prove it for SortedCollection
# Then: it holds for any Collection.

Summary