Strictification conjecture for linear fibrational double categories

A linear fibrational double category (LFDC) is a categorical structure with the substructural type-theoretic features described in the source, including type-level weakening, function types, and products. Strictification conjecture. Every LFDC with type-level weakening, function types, products, and the other indicated structure is equivalent to a strict LFDC. This would extend the applicability of the LFDC type theory from strict LFDCs to all LFDCs; the conjecture is presented as a goal for the future semantic development of the theory, and no resolution is given here.