7. Deduction structures from extension structures [0031]

If $C$ is a category equipped with an involutive monad $(\boldsymbol{P},I)$ (for example if $C$ is an algebraic universe), each $\boldsymbol P$-algebra $(E,\theta)$ (and in particular every free algebra $PZ$) carries an extension structure $\text{Ex}$: for each $f : I\to E$ and $h : I\to J$ we can define an extension of $f$ along $h$ as follows:

$$ \text{Ex}_h f \quad = \quad J\xto{\eta_J} PJ \xto{h^*} PI \xto{Pf} PE \xto{\theta} E $$
[0039] Translator’s Note 7·a.

Extension structures are defined by Guitart in a short note called Extenseurs, cf. (Guitart, 1980). (TODO: translate it).

If $C$ is a topos or the category of fuzzy sets, $\text{Ex}$ satisfies the axioms of an extension structu.

If $E$ has an extension structure, it also has a deduction structure, namely we can define

$$ (f : I\to E)\vdash(g : J\to E) $$

if and only if there exists a diagram where $\text{Ex}_u f$ and $\text{Ex}_w(k\circ v)=g$.