It looks like you're new here. If you want to get involved, click one of these buttons!

- All Categories 2.2K
- Applied Category Theory Course 347
- Applied Category Theory Seminar 2
- Exercises 149
- Discussion Groups 48
- How to Use MathJax 15
- Chat 475
- Azimuth Code Project 108
- News and Information 145
- Azimuth Blog 148
- Azimuth Forum 29
- Azimuth Project 190
- - Strategy 109
- - Conventions and Policies 21
- - Questions 43
- Azimuth Wiki 708
- - Latest Changes 700
- - - Action 14
- - - Biodiversity 8
- - - Books 2
- - - Carbon 9
- - - Computational methods 38
- - - Climate 53
- - - Earth science 23
- - - Ecology 43
- - - Energy 29
- - - Experiments 30
- - - Geoengineering 0
- - - Mathematical methods 69
- - - Meta 9
- - - Methodology 16
- - - Natural resources 7
- - - Oceans 4
- - - Organizations 34
- - - People 6
- - - Publishing 4
- - - Reports 3
- - - Software 20
- - - Statistical methods 2
- - - Sustainability 4
- - - Things to do 2
- - - Visualisation 1
- General 39

Options

## Comments

Nice ! Where did you do your PhD?

We're seeing a tiny taste of Grothendieck's 6 operations already in our study of posets: in Lecture 9 we saw that any function \(f : X \to Y\) induces a functor \(f^* : P(Y) \to P(X) \) that has both a left adjoint \(f_{!} : P(X) \to P(Y) \) and a right adjoint \( f_{\ast} : P(X) \to P(Y) \). All of this is a watered-down version of what happens for topoi or model categories. To me it will be very exciting when more and more of these ideas find their way into

appliedmathematics.`Nice ! Where did you do your PhD? We're seeing a tiny taste of Grothendieck's 6 operations already in our study of posets: in [Lecture 9](https://forum.azimuthproject.org/discussion/1931/lecture-9-chapter-1-adjoints-and-the-logic-of-subsets/p1) we saw that any function \\(f : X \to Y\\) induces a functor \\(f^* : P(Y) \to P(X) \\) that has both a left adjoint \\(f_{!} : P(X) \to P(Y) \\) and a right adjoint \\( f_{\ast} : P(X) \to P(Y) \\). All of this is a watered-down version of what happens for topoi or model categories. To me it will be very exciting when more and more of these ideas find their way into _applied_ mathematics.`

excuse me for the later answer. I did my PhD at the University Osnabrück(Germany), supervised by Rainer Vogt. Yes, the idea of Grothendieck's 6 operations is to consider the left and right adjoint functors of the pullback-functor f* in the context of monoidal fibered categories

`excuse me for the later answer. I did my PhD at the University Osnabrück(Germany), supervised by Rainer Vogt. Yes, the idea of Grothendieck's 6 operations is to consider the left and right adjoint functors of the pullback-functor f* in the context of monoidal fibered categories`

Topoi can be used as semantics for type theories (e.g. the nLab article https://ncatlab.org/nlab/show/dependent+linear+type+theory about linear dependent type theory, which presumably corresponds to infinity topoi). In the homotopy type theory one notes the classical adjunction f_! -| f ^ * -| f_ * as \ Sigma_f -| f ^ * -| \ Prod_f, because the terms (dependent) sum and product behave so. In the logical interpretation of HoTT, \ Sigma is an existence quanter and \ prod an all-quantor (https://homotopytypetheory.org/book/). Now every additional structure can be encoded on an infinite topos X so that the logic contains more constructs but the topos is still a model. A typical question would be, to an infinite topos X, to ask, which logic T exactly has this topos (up to isomorphism) as model.

`Topoi can be used as semantics for type theories (e.g. the nLab article https://ncatlab.org/nlab/show/dependent+linear+type+theory about linear dependent type theory, which presumably corresponds to infinity topoi). In the homotopy type theory one notes the classical adjunction f_! -| f ^ * -| f_ * as \ Sigma_f -| f ^ * -| \ Prod_f, because the terms (dependent) sum and product behave so. In the logical interpretation of HoTT, \ Sigma is an existence quanter and \ prod an all-quantor (https://homotopytypetheory.org/book/). Now every additional structure can be encoded on an infinite topos X so that the logic contains more constructs but the topos is still a model. A typical question would be, to an infinite topos X, to ask, which logic T exactly has this topos (up to isomorphism) as model.`