# 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.

```nix
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.

```nix
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.

```nix
cat.tests.yonedaEval
cat.tests.yonedaLift
cat.tests.evalLift
cat.tests.liftEval
```