Category Theory

This example is a larger proof library, organized as a guided tour. Each file builds on the previous one: proof combinators, arithmetic lemmas, algebraic structures, functors, and a Yoneda-style round trip.

The public api exposes extracted Nix functions. The hoas attrset keeps the typed HOAS terms available for users who want to inspect or extend the proofs.

Arithmetic proof layer

The first layer derives equality combinators from J, defines addition by Nat elimination, and proves the standard addition laws. Computational facts are extracted as ordinary Nix functions.

cat = import ./examples/category-theory { inherit fx; };

cat.api.add 3 5 == 8
cat.tests.addComm

Algebra and functors

The algebra files package the arithmetic proofs as a monoid and a one-object category. The functor file reuses the same doubling map as both a monoid homomorphism and an endofunctor.

cat.tests.natAddMonoid
cat.tests.natCategory
cat.tests.doubleFunctor

Yoneda round trips

The final file states the evaluate/lift pair for a small types-as-groupoids presentation and checks both round-trip laws.

cat.tests.yonedaEval
cat.tests.yonedaLift
cat.tests.evalLift
cat.tests.liftEval