Post #968748

The extended version of our LICS'25 paper, titled Constructive Ordinal Exponentiation, is now on arXiv. It has two new sections (Section 6 and 8) on ordinal arithmetic. Everything is formalized in Agda and merged into @MartinEscardo's TypeTopology repository. https://arxiv.org/abs/2501.14542v5 This joint work with @fnf, @Nicolai_Kraus and Chuangjie Xu. #TypeTheory #logic #Agda