Commit 2023-11-16 20:59 86d828e0

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.