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
Cartesian logic or finite limit logic is the internal logic of finitely complete categories (which the Elephant calls cartesian categories).
…
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 logic was introduced in the early seventies by John Isbell, Peter Freyd and Michel Coste (cf. Johnstone 1979). A standard source is Johnstone (2002).
Jiří Adámek, Jiří Rosický, Locally presentable and accessible categories , Cambridge UP 1994.
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)
Last revised on June 8, 2017 at 06:27:32. See the history of this page for a list of all contributions to it.