Commit 2023-11-16 20:59 86d828e0
View on Github →feat(Condensed): adjunctions between categories of condensed objects (#8210)
Creates the file Condensed/Adjunctions
. For now there is only the free-forgetful adjunction for condensed sets/abelian groups, but there are others on the to-do list.