Cite keml-diagrams.

]]>If we include simultaneous substitutions as a syntactic sort, then type theories can be formulated as GATs (or perhaps even multisorted ATs in the case of simple type theories). ]]>

Assume we have an operator

σ : {x : ∏_i s_i | P(x)}.

Then we can add a sort P* and a total operation outP* : P* -> ∏_i s_i and include P(outP*(p)) in the equational theory of the system. Then σ can be rewritten as

σ : {(x, p) : (∏_i s_i) x P* | outP*(p) = x}.

I guess we also want to express in the equational theory that if p, q : P*, then p = q. We probably also want to make sure that if P(x) then x = outP*(p) for some p, but I do not see how to do that, since P mentions non-total operations.

If this is indeed the idea, then I suggest to include this in the article. ]]>

Transferred material from cartesian theory > history.

]]>In another thread Mike said:

In particular, one selling point of intrinsic syntax seems to be its essentially-algebraic character

I don’t understand the details of the connection between essentially algebraic theories and type systems. Which type systems are essentially algebraic? Is it exactly those with intrinsic syntax? How do I rigorously tell when syntax is “intrinsic”, in an arbitrary metalanguage?

]]>Added a comment about Gabriel-Ulmer duality.

]]>Added “cartesian logic” as related topic.

“Cartesian theory” really ought to be redirected here, as the notions are equivalent. I am attempting to do that.

Steve Vickers

]]>- redirected “Cartesian theory” here
- added brief definition of cartesian theory.

Steve Vickers

]]>Clarification about partial Horn logic

]]>added references to *essentially algebraic theory*. Also equipped the text with a few more hyperlinks.