Contexts x_1:A_1,...,x_n:A_n in simple type theory can be viewed as “flat”, since the variable declarations don’t depend on each other and can be permuted.

In dependent type theory, the general form of contexts is (x_1:A_1, x_2:A_2(x_1), ...,x_n:A_n(x_1,...,x_{n-1})) with a linear dependency chain between the variable declarations: However, the specific contexts occuring in practice are not always totally ordered. For example, in the context (x y:O, f:A(x,y)) the first two variables are not interdependent.

So maybe we should allow finite posets as shapes of contexts? It turns out to be better to use an even more general class of structures: finite direct categories, i.e. finite categories which have no nontrivial isomorphisms and endomorphisms.

FDCs were introduced by Makkai [1] as part of his notion of “First order logic with dependent sorts”, but the perspective on FDCs proposed in this talk is somewhat different since FDCs are not used to represent dependency structures of theories, but of contexts.

In the talk I will explain why FDCs seem to provide a good abstract notion of “shape” for contexts, that the category of FDCs and discrete fibrations forms a coclan, and how to derive a notion of dependent algebraic theory from these ideas which is very close to Chaitanya Leena Subramaniam’s “dependently typed theories”.

[1] https://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf