Commit 2023-11-04 17:09 e11f1695

feat: descend a continuous map along a quotient map (#8090) This was done for profinite sets in LTE. We give a homeomorphism from the quotient of a quotient map to its codomain, and prove that a continuous map which is constant on the fibres of a quotient map can be descended along the quotient map.