Jon Sterling on Nostr: Allow me to once again advertise nprofile1q…8a7rw’s “Formalizing equivalences ...

Allow me to once again advertise nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyrgd7heng7z3cv2f6ddtm8zqxx3rxwh84wvk27nus3rl9qq9endsqr8a7rw (nprofile…a7rw)’s “Formalizing equivalences without tears”: https://arxiv.org/abs/2408.11501

I just used this technique to give a really simple proof that reflections in a Σ-closed subuniverse satisfy a *dependent* orthogonality law. In the critical step, there is a big diagram that commutes up to judgemental equality.

(Sorry for typos if some remain.)