Schreiber layers of foundations

• natural deduction logical framework for dependent types and including a predicative type of types hierarchy (at this stage or later)

  • add dependent product type formation rule $\to$ pure type system

    • add rules for introducing inductive types $\to$ calculus of inductive constructions

      • specify the rules for the specific inductive types: empty type, dependent sum type, identity type $\to$ intensional dependent type theory

        • add uniqueness of equality-axiom $\to$ extensional dependent type theory

      • restrict attention to types that are propositions $\to$ intuitionistic first-order logic

      • add the axiom of excluded middle $\to$ classical first order logic

      • add ZF-axioms $\to$ classical set theory

      • add axiom of choice $\to$ ZFC

      • add large cardinal axioms

      • consider setoid types $\to$ predicative set theory

        • add univalence-axiom and rules for introducing higher inductive types $\to$ homotopy type theory

      • reflect to h-props $\to$ intuitionistic first-order logic

      • add axiom of excluded middle $\to$ first-order logic

      • reflect to h-sets $\to$ intuitionistic structural set theory

      • add axiom of excluded middle $\to$ structural set theory

      • reflect to h-level 3 $\to$ groupoid theory

      • reflect to h-level $n+2$ $\to$ n-groupoid theory

      • add cohesion-axiom $\to$ cohesive homotopy type theory

      1. consider higher geometric quantization $\to$ quantum theory

      2. add interval-axiom $\to$ directed homotopy type theory

      1)+2) $\to$ FQFT ??