Skip to content

jonajosejg/grothendieck

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

1 Commit
 
 
 
 

Repository files navigation

agda-grothendieck-yoga

Grothendieck's Yoga of Six Operations and WirthmΓΌller Contexts

       π’ž ---- f ---> π’Ÿ
==============================
𝒫(π’ž) --[ f ↓! ⊣      ] -> 𝒫(π’Ÿ) β‰œ Lan (≑) (βŠ—) f β‰… Ξ» Ο†. βˆ«β†‘ 𝓍. Ο† 𝓍 βŠ— (≑) (f 𝓍, -)
𝒫(π’ž) <-[ f ↑! ≃ f ↑* ] -- 𝒫(π’Ÿ) β‰œ         - ∘ f β‰… Ξ» Ο†. Ο† ∘ f
𝒫(π’ž) --[      ⊣ f ↓* ] -> 𝒫(π’Ÿ) β‰œ Ran (≑) (β‹”) f β‰… Ξ» Ο†. βˆ«β†“ 𝓍. (≑) (-, f 𝓍) β‹” Ο† 𝓍

About

Yoga of Six Operations w / Wirthmuller Contexts

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages