# metric spaces (blogs) — RSS Amplifier Recent posts from the 2 feeds in the RSS Amplifier directory that cover metric spaces. Page: Feed: --- ## [QTCat: Queer and Trans People in Category Theory](https://semantic-domain.blogspot.com/2026/06/qtcat-queer-and-trans-people-in.html) _2026-06-08 · Neel Krishnaswami · Semantic Domain_ I just saw a poster for the QTCat workshop, which is a workshop for queer and trans people in category theory, which is being held this August 12-14, 2026 in Hamburg. Unfortunately, registration has closed, but I still wanted to post about it because they are going to livestream their talks, and it's got a pretty fascinating lineup of invited speakers: Jules Hedges , Theo Johnson-Freyd , Ioannis… ## [Bidirectional Typechecking That Does Not Stop](https://semantic-domain.blogspot.com/2026/05/bidirectional-typechecking-that-does.html) _2026-05-13 · Neel Krishnaswami · Semantic Domain_ I’ve been implementing a new language, and one of the things I have been doing is implementing a language server for the first time. Interestingly, this has changed how I will write bidirectional typecheckers from now on! A bidirectional type system is a set of (syntax-directed) rules with a mode assignment, telling you which bits of the rules are inputs, and which bits are outputs. This lets you… ## [IsarMathLib 1.35.0: Update to Isabelle 2025-1, Uniformities and pseudometrics](https://slawekk.wordpress.com/2025/12/20/isarmathlib-1-35-0-update-to-isabelle-2025-1-uniformities-and-pseudometrics/) _2025-12-20 · slawekk · Formalized Mathematics_ In this release I updated IsarMathLib to the new Isabelle 2025-1. On the mathematics side I continued the story of defining uniformities with collections of psedudometrics. As they say in General Topology Chapter IX §1 no. 4: The significance of defining a uniformity by means of a family of pseudometrics lies in the fact that \[…\] ## [IsarMathLib 1.34.0: Z-modules and complete lattice of uniformities](https://slawekk.wordpress.com/2025/08/24/isarmathlib-1-34-0-z-modules-and-complete-lattice-of-uniformities/) _2025-08-24 · slawekk · Formalized Mathematics_ In this release I edited a theory file about actions of integers on abelian groups (-modules) contributed by Daniel de la Concepción Sáez a couple of years ago so that it is written in Isar dialect supported by the isarmathlib.org site and finished the proof that collection of uniformities on a fixed set, ordered by \[…\] ## [IsarMathLib 1.33.0: ultrafilters, ultraproducts, hypernaturals, order on uniformities](https://slawekk.wordpress.com/2025/05/18/isarmathlib-1-33-0-ultrafilters-ultraproducts-hypernaturals-order-on-unformities/) _2025-05-18 · slawekk · Formalized Mathematics_ This release is mostly about recent contributions by Daniel de la Concepción Sáez. There are three theory files added on ultrafilters, ultraproducts, internal sets and hypernatural numbers (i.e. nonnegative hyperintegers). On my side I formalized some material about the order structure on the collection of uniformities on a given set . Such uniformities are collections \[…\] ## [IsarMathLib 1.32.0: Update to Isabelle2025 and Uniformity from collection of pseudometrics](https://slawekk.wordpress.com/2025/03/19/isarmathlib-1-32-0-update-to-isabelle2025-and-uniformity-from-collection-of-pseudometrics/) _2025-03-19 · slawekk · Formalized Mathematics_ As in the title I updated IsarMathLib to Isabelle2025 released March 13th. There is quite a lot of new formalized mathematics in this release, scattered over many subjects. One new theory that stands out a bit is about uniformities defined by collections of pseudometrics. In one of previous posts I wrote about how a single \[…\] ## [Finally...](https://semantic-domain.blogspot.com/2025/01/finally.html) _2025-01-02 · Neel Krishnaswami · Semantic Domain_ ...it's Rocq, and no longer Coq! ## [How to Read Papers](https://semantic-domain.blogspot.com/2024/12/how-to-read-papers.html) _2024-12-16 · Neel Krishnaswami · Semantic Domain_ One of the key skills for any academic researcher is reading other peoples' papers. The trouble is that our peers write papers faster than we can read them, and to fully understand a paper takes a long time, because each paper summarizes months to years of effort. So you cannot fully read all the relevant literature, even if you did nothing but reading. This means you need to have a way to…