Dear All - Here a question related to categorical logic (or categorical proof theory) of a very different type. I would like to put it here because it is an illustration of another part of the field and also because it is technically difficult and interesting. It is well known that certain systems of propositional logic have a natural structure of free category for certain classes of categories with structure. For example, we have a structure of free Symmetric Monoidal Closed Category on the Intuitionistic Multiplicative Linear Logic. In this structure formulas are objects and equivalence classes of derivations of the sequents A -> B are morphisms. Free SMCC (in presence of "tensor unit" I) is not "fully coherent": there are non-commutative diagrams. For example, one has the Mac Lane's example A*** -> B*** (called "triple dual diagram"). In terms of IMLL there exist two non-equivalent derivations of ((A-oI)-oI)-o I -> ((A-oI)-oI)-o I w.r.t. the equivalence of free SMCC on the derivations of IMLL. One derivation is identity, another derivation is obtained in obvious way using the derivability of ((A-oI)-oI)-o I -> A-o I. Let us denote these derivations 1 and f respectively. (For the sequent ((A-oI)-oI)-o I -> ((A-oI)-oI)-o I every derivation is equivalent to 1 or to f.) The "triple dual conjecture" says that if we declare f\equiv 1 then all the derivations with the same final sequent in IMLL will become equivalent. I.e. the stronger categorical structure than SMCC (obtained by adding this new axiom for equivalence/ commutativity of diagrams) will be "fully coherent". If it is true we would have an interesting new variety of categories (subvariety of SMCCs) in the sense of Universal Algebra. Proof-theoretically, the study of this conjecture requires to study the equivalence relations on derivations of IMLL between the relation of free SMCC and the relation that identifies all derivations with the same final sequent. In my paper S. Soloviev. On the conditions of full coherence in closed categories. Journal of Pure and Applied Algebra, 69:301-329, 1990. it was shown that - if the "triple dual diagram" is commutative w.r.t. some equivalence relation ~ (containing the relation of free SMCC) - and the following additional condition holds: [a-oI/a] h ~ [a-oI/a] g => h~g for any two derivations of the same sequent, then all the derivations of the same sequent in IMLL become equivalent. The additional condition is a) difficult to verify b) has the form different form the equational form ("commutativity of a diagram") required from the point of view of Universal Algebra approach. All the attempts to prove "pure" triple dual conjecture (by myself and others) did not yet succeed. One may mention that it is known that some intermediate equivalence relations between the relation of free SMCC and the "total" relation of derivations do exist: L. Mehats, S. Soloviev. Coherence in SMCCs and equivalences on deriva- tions in IMLL with unit. Annals of Pure and Applied Logic, v.147, 3, p. 127-179, august 2007. but all known intermediate relations are contained in the relation generated by commutativity of triple dual diagram. My ph.d. student Antoine El Khoury has checked also that the commutativity of triple dual diagram (equivalence of 1 and f) implies equivalence of derivations of the balanced sequents with 1, 2 or 3 variables (commutativity of corresponding diagrams in SMCC). Remark. Obviosly, the commutativity of triple dual diagram implies A*** isomorphe to A*. Best regards to all Sergei Soloviev [For admin and other information see: http://www.mta.ca/~cat-dist/ ]