Jon Sterling on Nostr: nprofile1q…uu2p5 I suppose you mean the infinity-localisation, rather than the ...

nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyrvd3vd6zkwj3m8gddvs7rs6wmdhg55jz3l5w4paq07jp4dax4vk6guu2p5 (nprofile…u2p5) I suppose you mean the infinity-localisation, rather than the homotopy category… but in this case, I agree that it is important for understanding the semantics of HoTT, but I am not so sure that it is important for understanding the semantics of Lean.