Commit 2022-05-09 11:26 c43486ec

View on Github →

feat(category_theory/limits): allow (co)limits over lower universes in algebraic categories (#13990) I'm concerned about the new universe annotations required in places. It was not so impossible to add them when proofs broke, but the proofs might have been hard to construct in the first place ....

Estimated changes

modified theorem Top.coinduced_of_is_colimit
modified def Top.colimit_cocone
modified theorem Top.colimit_is_open_iff
modified theorem Top.colimit_topology
modified theorem Top.induced_of_is_limit
modified def Top.limit_cone
modified def Top.limit_cone_infi
modified theorem Top.limit_topology
modified def Top.pi_fan
modified def Top.pi_fan_is_limit
modified def Top.pi_iso_pi
modified theorem Top.pi_iso_pi_hom_apply
modified theorem Top.pi_iso_pi_inv_π
modified theorem Top.pi_iso_pi_inv_π_apply
modified def Top.pi_π
modified def Top.sigma_cofan
modified def Top.sigma_iso_sigma
modified theorem Top.sigma_iso_sigma_hom_ι
modified def Top.sigma_ι