Let $\mathbb{A_0,A_1}$ be logics.

A flow type, or double functor, is a matrix functor $[\![\mathbb{A}]\!]: \mathbb{A_0\to A_1}$

2.png

with invertible matrix transformations

3-comp.png

3-unit.png

which cohere with the associators and unitors.

4-assoc.png

4-lunit.png

4-runit.png