The module 26-descent is replaced with a collection of files written in the "new" style, defining descent data, morphisms and equivalences, and showing the descent property.
There is currently some duplication with the development in 26-id-pushout, where I tried to make the absolute minimum changes required for it to typecheck, since I'll be replacing the entire file in an upcoming PR.
The module
26-descentis replaced with a collection of files written in the "new" style, defining descent data, morphisms and equivalences, and showing the descent property.There is currently some duplication with the development in
26-id-pushout, where I tried to make the absolute minimum changes required for it to typecheck, since I'll be replacing the entire file in an upcoming PR.