set of contexts $T_A$ – understood as tests –, and a term $t$ is considered typable with the type $A$ when $t\in T_A^\bot$, i.e. $\forall E(\cdot)\in T_A, t\perp E(\cdot)$. We refer the reader to, e.g., Riba’s work[@riba2007strong] for more details.

In this aspect of reconstructing linear logic, several geometry of interaction models were defined using operators algebras [@girard1989geometry; @girard1988geometry; @girard2011geometry], unification algebras [@girard1995geometry], graphs [@seiller2012interaction; @seiller2016interaction] and graphings [@seiller2017interaction; @seiller2019interaction; @seiller2016interaction2]. Although all these models did define rich models, that were in particular used to study computational complexity [@baillot2001elementary; @aubert2016characterizing; @aubert2016logarithmic; @seiller2018interaction; @seiller2020probabilistic], they failed with respect to two different aspects. Firstly, the objects used to interpret even the most basic proofs were most of the time infinite objects and even when they were not, types were defined through an infinite number of tests. Secondly, the obtained models did interpret soundly the fragments of linear logic considered, but no completeness results exist[^1].

Recently, Girard published a series of articles [@girard2013three; @girard2017transcendental; @girard2016transcendental; @girard2016transcendental3] sketching the main lines of a new kind of model that would have the qualities of geometry of interaction models, but improve on them at least concerning the first failure mentioned above. Those articles are interesting and 