Closed mzeuner closed 2 months ago
This PR proves that lifting functor from sets in a universe to sets in the successor universe is fully faithful and preserves (small) limits. It is a less opaque rewrite of the accidental https://github.com/agda/cubical/pull/1122.
This PR proves that lifting functor from sets in a universe to sets in the successor universe is fully faithful and preserves (small) limits. It is a less opaque rewrite of the accidental https://github.com/agda/cubical/pull/1122.