[Agda] Poor man's way to latex Agda source

Eduardo Ochs eduardoochs at gmail.com
Wed Jul 7 06:04:19 CEST 2021

Hello list,

how do I latex small snippets of Agda code?

Ok, let me explain... I am a beginner with Agda and I am alternating
between reading the tutorials and trying to understand the
agda-categories library:


I've been working on ways to visualize some statements and proofs in
Category Theory and on ways to translate between different notations,
and I would like to be able to add to a diagram like this one


the information on how to translate each of my terms to Agda, using
exactly the terminology of the agda-categories library whenever

My guess is that it should be possible to write a "poor man's way to
typeset Agda source", like this thing here, that requires the user to
add lots of backslashes by hand:

  % \co: a low-level way to typeset code; a poor man's "\verb"

_and_ I guess that some people here may have written hacks like this,
which is why I am asking... the tricky part is how to handle the
unicode characters.

By the way, I use lualatex most of the time and pdflatex when I need,
and I've spent too much time learning how to use tricks like these

  \catcode`↗=13 \def↗{\nearrow} % lualatex
  \DeclareUnicodeCharacter{2198}{\searrow} % pdflatex

and how to fix them when they break. =/

  Thanks in advance!
    Eduardo Ochs

More information about the Agda mailing list