Skip to content

Latest commit

 

History

72 Commits

Folders and files

NameName
Last commit message
Last commit date
 
 
 
 
 
 
 
 

Repository files navigation

yoneda-game (work in progress)

The ∞-Yoneda Game — an interactive Rzk game following Emily Riehl's geodesic to the Yoneda lemma, built on the rzk-game engine.

Status: work in progress. Nine sections are in place, grouped into three chapters (homotopy type theory, synthetic ∞-categories, and naturality); the remainder of the geodesic to the Yoneda lemma is added over later updates.

How it works

The game is just data: a game/game.yaml table of contents and game/levels/*.rzk.md files (Rzk source in fenced prelude / template / solution blocks, plus Markdown prose). There is no Haskell toolchain here — rzk-game-action fetches the prebuilt engine and bundler from a pinned rzk-game release, bundles game/ into game.json, assembles the static site, and .github/workflows/deploy.yml publishes it to GitHub Pages.

Authoring locally

Pin engine-version in deploy.yml to a released tag for reproducible builds. To iterate on content off-CI, run the bundler from a rzk-game checkout over this repo's game/.

About

Proving the ∞-categorical Yoneda lemma as an Rzk formalization game.

Resources

Stars

1 star

Watchers

0 watching

Forks

Releases

Packages

Contributors