An algebraic formulation of dependent type theory

[Egbert Rijke]

Dear all,

Yesterday I gave a talk during the HoTT workshop in Oxford. In it, I gave an algebraic description of dependent type theory and defined the corresponding algebras in a category with finite limits, called E-systems. E-systems are like B-systems, with the main difference being that B-systems have a stratification which I replaced with a theory of extension. This has both a context extension and a family extension. The theory also permits internal E-systems, which I did define but didn't discuss in the talk, and it potentially allows for infinite contexts.

The slides are attached.

With kind regards,

Egbert