Comparing hierarchies of types in models of linear logic

International audienceWe show that two models M1 and M2 of linear logic collapse to the same extensional hierarchy of types, when (1) their monoidal categories C and D are related by a pair of monoidal functors F: C -> D and G: D-> C and transformations Id => GF and Id => FG, and (2) their exponentials are related by distributive laws ! F => F ! and ! G => G ! commuting to the promotion rule. The key ingredient of the proof is a notion of back-and-forth translation between the hierarchies of types induced by M1 and M2. We apply this result to compare (1) the qualitative and the quantitative hierarchies induced by the coherence (or hypercoherence) space model, (2) several paradigms of games semantics: error-free vs. error-aware, alternated vs. non-alternated, backtracking vs. repetitive, uniform vs. non-uniform