Grothendieck's Yoga of Six Operations and WirthmΓΌller Contexts
π ---- f ---> π
==============================
π«(π) --[ f β! β£ ] -> π«(π) β Lan (β‘) (β) f β
Ξ» Ο. β«β π. Ο π β (β‘) (f π, -)
π«(π) <-[ f β! β f β* ] -- π«(π) β - β f β
Ξ» Ο. Ο β f
π«(π) --[ β£ f β* ] -> π«(π) β Ran (β‘) (β) f β
Ξ» Ο. β«β π. (β‘) (-, f π) β Ο π