Categorical univalence of a universe does not entail function extensionality, as shown by polynomial models of type theory that refute the latter while satisfying the former.
Natural models of homotopy type theory
3 Pith papers cite this work, alongside 36 external citations. Polarity classification is still indexing.
3
Pith papers citing it
36
external citations · Crossref
citation-role summary
background 1
citation-polarity summary
verdicts
UNVERDICTED 3roles
background 1polarities
background 1representative citing papers
A dependent linear type theory is constructed by embedding linear logic into dependent type theory, yielding multiplicities that depend on variables, supporting W-types, with semantics in indexed Categories with Families and an Agda implementation.
Develops constructive higher sheaf models of type theory to support synthetic mathematics with univalence and higher inductive types.
citing papers explorer
-
Univalence without function extensionality
Categorical univalence of a universe does not entail function extensionality, as shown by polynomial models of type theory that refute the latter while satisfying the former.
-
Dependent Multiplicities in Dependent Linear Type Theory
A dependent linear type theory is constructed by embedding linear logic into dependent type theory, yielding multiplicities that depend on variables, supporting W-types, with semantics in indexed Categories with Families and an Agda implementation.
-
Constructive higher sheaf models with applications to synthetic mathematics
Develops constructive higher sheaf models of type theory to support synthetic mathematics with univalence and higher inductive types.