Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userConstructive sheaf models of type theory
65
0
0.0
(
0
)
Ask ChatGPT about the research
No Arabic abstract
We generalise sheaf models of intuitionistic logic to univalent type theory over a small category with a Grothendieck topology. We use in a crucial way that we have constructive models of univalence, that can then be relativized to any presheaf models, and these sheaf models are obtained by localisation for a left exact modality. We provide first an abstract notion of descent data which can be thought of as a higher version of the notion of prenucleus on frames, from which can be generated a nucleus (left exact modality) by transfinite iteration. We then provide several examples.
rate research
Read More
We introduce Z-stability, a notion capturing the intuition that if a function f maps a metric space into a normed space and if the norm of f(x) is small, then x is close to a zero of f. Working in Bishops constructive setting, we first study pointwi
We show that numerous distinctive concepts of constructive mathematics arise automatically from an antithesis translation of affine logic into intuitionistic logic via a Chu/Dialectica construction. This includes apartness relations, complemented subsets, anti-subgroups and anti-ideals, strict and non-strict order pairs, cut-valued metrics, and apartness spaces. We also explain the constructive bifurcation of some classical concepts using the choice between multiplicative and additive affine connectives. Affine logic and the antithesis construction thus systematically constructivize classical definitions, handling the resulting bookkeeping automatically.
We study idempotents in intensional Martin-Lof type theory, and in particular the question of when and whether they split. We show that in the presence of propositional truncation and Voevodskys univalence axiom, there exist idempotents that do not split; thus in plain MLTT not all idempotents can be proven to split. On the other hand, assuming only function extensionality, an idempotent can be split if and only if its witness of idempotency satisfies one extra coherence condition. Both proofs are inspired by parallel results of Lurie in higher category theory, showing that ideas from higher category theory and homotopy theory can have applications even in ordinary MLTT. Finally, we show that although the witness of idempotency can be recovered from a splitting, the one extra coherence condition cannot in general; and we construct the type of fully coherent idempotents, by splitting an idempotent on the type of partially coherent ones. Our results have been formally verified in the proof assistant Coq.
Cubical type theory provides a constructive justification of homotopy type theory. A crucial ingredient of cubical type theory is a path lifting operation which is explained computationally by induction on the type involving several non-canonical choices. We present in this article two canonicity results, both proved by a sconing argument: a homotopy canonicity result, every natural number is path equal to a numeral, even if we take away the equations defining the lifting operation on the type structure, and a canonicity result, which uses these equations in a crucial way. Both proofs are done internally in a presheaf model.
This is an introduction to Homotopy Type Theory and Univalent Foundations for philosophers, written as a chapter for the book Categories for the Working Philosopher (ed. Elaine Landry)
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
