How does one get certain unicode characters to compile with .lagda files. For instance, when I add certain unicode characters manually to the tex file, like \phi, \forall, etc. but when I add < or == it yields the below error. Should I change font packages? Are there any repositories with example .lagda files, relevantly installed font packages, and commands so that I can get it to work out of the box for say, anything written in the standard library? I'm following the exact instructions for ad hoc workarounds on
https://agda.readthedocs.io/en/v2.6.1.1/tools/generating-latex.html
Here is the relevant clipping from my main.tex
\usepackage{unicode-math}
\setmathfont{XITS Math}
\usepackage{newunicodechar}
\newunicodechar{λ}{\ensuremath{\mathnormal\lambda}}
\newunicodechar{ℓ}{\ensuremath{\mathnormal\ell}}
\newunicodechar{η}{\ensuremath{\mathnormal\eta}}
\newunicodechar{∀}{\ensuremath{\mathnormal\forall}}
\newunicodechar{ϕ}{\ensuremath{\mathnormal\phi}}
%% \newunicodechar{⟨}{\ensuremath{\mathnormal\<}}
%% \newunicodechar{⟩}{\ensuremath{\mathnormal\>}}
\newunicodechar{≡}{\ensuremath{\mathnormal\==}} %error when uncommented
and the error
$ ./compile.sh
Latexmk: This is Latexmk, John Collins, 26 Dec. 2019, version: 4.67.
Latexmk: applying rule 'xelatex'...
Rule 'xelatex': File changes, etc:
Changed files, or newly in use since previous run(s):
'latex/Cubical/Algebra/Group/Morphism.aux'
------------
Run number 1 of rule 'xelatex'
------------
------------
Running 'xelatex -no-pdf -recorder "main.tex"'
------------
This is XeTeX, Version 3.14159265-2.6-0.999991 (TeX Live 2019/Debian) (preloaded format=xelatex)
restricted \write18 enabled.
entering extended mode
(./main.tex
LaTeX2e <2020-02-02> patch level 2
L3 programming layer <2020-02-14>
(/usr/share/texlive/texmf-dist/tex/latex/base/article.cls
Document Class: article 2019/12/20 v1.4l Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/size10.clo))
(/usr/share/texlive/texmf-dist/tex/latex/base/inputenc.sty) (./latex/agda.sty
LaTeX Warning: You have requested package `latex/agda',
but the package provides `agda'.
(/usr/share/texlive/texmf-dist/tex/generic/iftex/ifxetex.sty
(/usr/share/texlive/texmf-dist/tex/generic/iftex/iftex.sty))
(/usr/share/texlive/texmf-dist/tex/generic/iftex/ifluatex.sty)
(/usr/share/texlive/texmf-dist/tex/latex/xifthen/xifthen.sty
(/usr/share/texlive/texmf-dist/tex/latex/tools/calc.sty)
(/usr/share/texlive/texmf-dist/tex/latex/base/ifthen.sty)
(/usr/share/texlive/texmf-dist/tex/latex/ifmtarg/ifmtarg.sty))
(/usr/share/texlive/texmf-dist/tex/latex/xcolor/xcolor.sty
(/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/color.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/graphics-def/xetex.def))
(/usr/share/texlive/texmf-dist/tex/latex/polytable/polytable.sty
(/usr/share/texlive/texmf-dist/tex/latex/lazylist/lazylist.sty)
(/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty))
(/usr/share/texlive/texmf-dist/tex/latex/etoolbox/etoolbox.sty)
(/usr/share/texlive/texmf-dist/tex/latex/environ/environ.sty
(/usr/share/texlive/texmf-dist/tex/latex/trimspaces/trimspaces.sty))
(/usr/share/texlive/texmf-dist/tex/latex/l3packages/xparse/xparse.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-xdvipdfmx.def)))
(/usr/share/texlive/texmf-dist/tex/latex/xkeyval/xkeyval.sty
(/usr/share/texlive/texmf-dist/tex/generic/xkeyval/xkeyval.tex
(/usr/share/texlive/texmf-dist/tex/generic/xkeyval/xkvutils.tex
(/usr/share/texlive/texmf-dist/tex/generic/xkeyval/keyval.tex)))))
(/usr/share/texlive/texmf-dist/tex/latex/unicode-math/unicode-math.sty
(/usr/share/texlive/texmf-dist/tex/latex/unicode-math/unicode-math-xetex.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3packages/l3keys2e/l3keys2e.sty)
(/usr/share/texlive/texmf-dist/tex/latex/fontspec/fontspec.sty
(/usr/share/texlive/texmf-dist/tex/latex/fontspec/fontspec-xetex.sty
(/usr/share/texlive/texmf-dist/tex/latex/base/fontenc.sty)
(/usr/share/texlive/texmf-dist/tex/latex/fontspec/fontspec.cfg)))
(/usr/share/texlive/texmf-dist/tex/latex/base/fix-cm.sty
(/usr/share/texlive/texmf-dist/tex/latex/base/ts1enc.def))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the `?' option.
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))
(/usr/share/texlive/texmf-dist/tex/latex/unicode-math/unicode-math-table.tex)))
(/usr/share/texlive/texmf-dist/tex/latex/newunicodechar/newunicodechar.sty)
(./main.aux (./latex/Cubical/Algebra/Group/Morphism.aux)) [1]
(./latex/Cubical/Algebra/Group/Morphism.tex
! Extra }, or forgotten $.
\PT@scanend ->\PT@post@preamble \egroup
l.594 \end{code}
?