Grothendieck's Yoga of Six Operations and Wirthmüller Contexts
𝒞 ---- f ---> 𝒟
==============================
𝒫(𝒞) --[ f ↓! ⊣ ] -> 𝒫(𝒟) ≜ Lan (≡) (⊗) f ≅ λ φ. ∫↑ 𝓍. φ 𝓍 ⊗ (≡) (f 𝓍, -)
𝒫(𝒞) <-[ f ↑! ≃ f ↑* ] -- 𝒫(𝒟) ≜ - ∘ f ≅ λ φ. φ ∘ f
𝒫(𝒞) --[ ⊣ f ↓* ] -> 𝒫(𝒟) ≜ Ran (≡) (⋔) f ≅ λ φ. ∫↓ 𝓍. (≡) (-, f 𝓍) ⋔ φ 𝓍