Owen Lynch on Nostr: nprofile1q…4rrqe Well for Lean it is the homotopy category which is relevant, ...
nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe (nprofile…rrqe) Well for Lean it is the homotopy category which is relevant, because what looks like a pullback in Lean syntax is only semantically a pullback in the homotopy category.