cubical icon indicating copy to clipboard operation
cubical copied to clipboard

Published 20 hours ago • verified publisher icon agda

Properties of the lifting functor

Open mzeuner opened this issue 10 months ago • 0 comments

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.

mzeuner avatar Apr 24 '24 11:04 mzeuner