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.
Moss and Tamara von Glehn
5 Pith papers cite this work. Polarity classification is still indexing.
5
Pith papers citing it
citation-role summary
background 2
citation-polarity summary
verdicts
UNVERDICTED 5roles
background 2polarities
background 2representative 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.
Introduces the first intersection type system for a lambda calculus with algebraic effects and handlers that characterizes termination via subject reduction and expansion while inducing a sound simple type system with decidable HOMC.
Underapproximate types with symbolic traces guide synthesis of test generators that outperform defaults in property-based testing and model checking for effectful programs.
A finitary refinement type system is sound and complete for Scott-open properties in a fixpoint-like logic over spectral Scott domains.
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.
-
When Types Intersect and Effects Get Handled
Introduces the first intersection type system for a lambda calculus with algebraic effects and handlers that characterizes termination via subject reduction and expansion while inducing a sound simple type system with decidable HOMC.
-
Trace-Guided Synthesis of Effectful Test Generators
Underapproximate types with symbolic traces guide synthesis of test generators that outperform defaults in property-based testing and model checking for effectful programs.
-
A Complete Finitary Refinement Type System for Scott-Open Properties
A finitary refinement type system is sound and complete for Scott-open properties in a fixpoint-like logic over spectral Scott domains.