From 3f977ffdec569474065cad950a439de4505a7af8 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Mon, 27 Jan 2025 16:40:35 -0800 Subject: [PATCH] Add ordinal exponentiation notes to iset.mm The comment of df-oexpi seems like a suitable place to say something about where we can find out more about constructive ordinal exponentiation. --- iset.mm | 12 +++++++++++- mmil.raw.html | 5 +++++ 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/iset.mm b/iset.mm index f7e836f62f..25bc742abd 100644 --- a/iset.mm +++ b/iset.mm @@ -61188,7 +61188,17 @@ defined for all sets (being defined for all ordinals might be enough if This definition is similar to a conventional definition of exponentiation except that it defines ` (/) ^oi A ` to be ` 1o ` for all ` A e. On ` , in order to avoid having different cases for whether the - base is ` (/) ` or not. (Contributed by Mario Carneiro, 4-Jul-2019.) $) + base is ` (/) ` or not. + + We do not yet have an extensive development of ordinal exponentiation. + For background on ordinal exponentiation without excluded middle, see + Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, and Chuangjie Xu + (2025), "Ordinal Exponentiation in Homotopy Type Theory", + arXiv:2501.14542 , ~ https://arxiv.org/abs/2501.14542 which is + formalized in the TypeTopology proof library at + ~ https://ordinal-exponentiation-hott.github.io/ . + + (Contributed by Mario Carneiro, 4-Jul-2019.) $) df-oexpi $a |- ^oi = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) ) $. $} diff --git a/mmil.raw.html b/mmil.raw.html index c7974ced00..b162645940 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -3718,6 +3718,11 @@ ~ om0 + + df-oexp + ~ df-oexpi + + oa0r none