natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
A theory in cartesian logic.
…
finitely complete category, cartesian functor, cartesian logic, cartesian theory
regular category, regular functor, regular logic, regular theory, regular coverage, regular topos
coherent category, coherent functor, coherent logic, coherent theory, coherent coverage, coherent topos
geometric category, geometric functor, geometric logic, geometric theory
Cartesian theories were introduced under different names in the early seventies by John Isbell, Peter Freyd and Michel Coste (cf. Johnstone 1979). A standard source is Johnstone (2002).
Peter Freyd, Cartesian Logic , Theor. Comp. Sci. 278 (2002) pp.3-21.
Peter Johnstone, A Syntactic Approach to Diers’ Localizable Categories , pp.466-478 in Springer LNM 753 Heidelberg 1979.
Peter Johnstone, Sketches of an Elephant II , Oxford UP 2002. (Around D1.3.4 p.833)