Refactor results from Poly in this file
The important sorrys remaining are
- I have defined the Beck-Chevalley natural transformations, but not shown that they are isomorphisms. Links
MorphismProperty.Over.map /left adjoint to pb/sigma and pushward/right adjoint to pb/pi
MorphismProperty.Over.map /left adjoint to pb/sigma preserves pullbacks. Here
Refactor results from Poly in this file
The important
sorrys remaining areMorphismProperty.Over.map/left adjoint to pb/sigma and pushward/right adjoint to pb/piMorphismProperty.Over.map/left adjoint to pb/sigma preserves pullbacks. Here