Tangle-lagda replaces tr-agda with a raco subcommand. You write a .lagda.scrbl whose Agda code lives between @agda|{ and }|, then go two directions.

mirror extracts a .agda for Agda:

raco tangle-lagda mirror src/foo.lagda.scrbl _tmp/mirror/foo.agda

weave folds the highlighted HTML back into a renderable card:

raco tangle-lagda weave src/foo.lagda.scrbl _tmp/agda-html/foo.html content/gen/foo.scrbl

Prose and markers become blank lines, so the mirror is line-for-line aligned with the source: Agda highlights line n, weave drops it back onto line n. The card below is the real output of that pipeline, woven from src/Peano.lagda.scrbl:

module demo where

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

_+_ : Nat → Nat → Nat
zero  + n = n
suc m + n = suc (m + n)