Native Type Theory
Article
Formal Antecedent
Category Theory
Citation
Christian Williams and Michael Stay. (2021). Native Type Theory.
Why this reference is included
Williams and Stay’s paper Native Type Theory (2021) is one of the program’s working technical references. Cited across Book I (Categorical Foundations), Part 18, Chapter Star-Autonomous Categories and the Diagonal Barrier; Book I (Categorical Foundations), Part 18, Chapter The Enrichment Frontier — the central framing is “to related work. The structural exclusion theorem connects to three active research programs that pursue type theories with substructural features: Williams–Stay native type…”.
Cited in
-
Book I — Categorical Foundations Part 18Chapter Star-Autonomous Categories and the Diagonal Barrier
to related work. The structural exclusion theorem connects to three active research programs that pursue type theories with substructural features: Williams–Stay native type theory : type constructors derived from term constructors via embedding into a presheaf topos
-
Book I — Categorical Foundations Part 18Chapter The Enrichment Frontier
Williams and Stay propose native type theory — type theories with natively *-autonomous semantics rather than cartesian-closed semantics
-
Book I — Categorical Foundations Part 18Chapter The Enrichment Frontier
Williams–Stay : native *-autonomous type theory (programmatic)