Commit 2026-02-15 14:33 cf6c6cbc

View on Github →

chore(CategoryTheory/Sites): generalize universes for Sieve.functor (#35188) Add Sieve.uliftFunctor, which is a variant of Sieve.functor with a lift in the universe level of the goal. Add variants of existing lemmas accordingly. Also modify the simp lemmas of uliftYoneda to more useful ones.

Estimated changes