notation recommendations

Stream: lean4

[Dean Young]

I have defined categorical completion [Cᵒᵖ,Set] in my category theory library and wanted to notate it with some variant of a circumflex/hat/carat. The notation also needs a Latex equivalent which works with the minted environment. Does anyone have a recommendation for what to do here?

[Eric Wieser]

Any unicode notation can be made to work with minted, so that's not really a constraint

[Dean Young]

What about the over and under characters?

[Eric Wieser]

You can tell LaTeX to render unicode characters in whatever way you please, so sure

[Alex Keizer]

I switched to XeLatex spefically for its unicode support, and it's been very easy to have it render unicode heavy Lean code nicely!

[Dean Young]

Hmm... I think I'll switch to Xelatex then.