| foundations | constructive, univalent |
| gh | https://github.com/jcreedcmu |
We're excited to share the Lean FRO Year 3 Roadmap today! This roadmap builds on work completed in the first two years of Lean FRO operations and will guide all #LeanLang development through July 2026. Read the full document at https://lean-lang.org/fro/ for details on our seven key priority areas.
the annoying thing is there really is no obvious clean way to say everything I want in 2d... the thing I'm calling β * α (which "is" the "horizontal composition" of 2-cells sorta, but only sorta) is, as an object, the honest-to-goodness pushout of α and β over B, but it's also a funny weak pushout of hf and kg over A ⊕ C.
Need to invest in some VR goggles I guess to do this properly in 3d...
So I just started working for the Lean FRO (https://lean-lang.org/fro/); if you are interested in
- math;
- dependently typed programming languages;
- and specifically building tooling to make doing mechanized math in lean more accessible, approachable, and generally awesome
then we should talk! I'm going to be hiring for a team whose goal is that. Boosts welcome, and feel free to dm me with contact info or email jason@lean-fro.org
ideas I considered and rejected:
a bare "script" I find unsatisfying because it's already so overloaded with other meanings
"index" I don't like because it's too tied to a certain *function* of the typographical operation. Squaring a variable is a superscript 2, but is not an index.
It's nice that we have "affix" as a hypernym when we want to say "either a prefix or a suffix".
I lack any knowledge of a good word for "either a subscript or superscript".
Proposal: "offscript"
+ reasonably short and snappy
+ it has the morpheme "script" in it, maintaining a close mouthfeel relationship to its hyponyms
+ "off" describes offsetting the baseline in some direction, either up or down
+ it vaguely suggests "going off-script" which I find amusing
Lean