theory of presheaf type

**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 geometric theory $T$ is **of presheaf type** if its classifying topos is equivalent to a presheaf topos.

A theory is of presheaf type if and only if its category of models in Set is a finitely accessible category, and if and only if it is sketchable.

- Tibor Beke,
*Theories of presheaf type*(pdf)

Revised on October 31, 2012 02:49:50
by Urs Schreiber
(82.169.65.155)