Support for U+2129 (Turned Greek Small Letter Iota)

[vsannier]

Description

I suggest adding iota.inv in the sym module for the Unicode character U+2129 (Turned Greek Small Letter Iota).

Use Case

This symbol has been used by Peano, Russell, Whitehead, Quine and many others to this day for the definite description operator. For example, sqrt(2) ≝ (℩x)(x²=2) (read “the square root of 2 is defined as the unique x such that…”).

See:

• iota expressions by Joel David Hamkins,
• Definition df-iota in the Intuitionistic Logic Explorer,
• The Notation in Principia Mathematica by Bernard Linsky,
• The Descriptive Operators by Claus-Peter Wirth,
• etc.

[MDLC01]

Thanks for providing information about how this character is used! Adding iota.inv to sym for U+2129 (as well as many other symbols) is planned. If you have more to add to the discussion, you can join the Symbols forge on Typst's Discord server.