arXiv subjects

Christian Sattler

Publications and source records attributed to Christian Sattler.

26 records · Page 2Linked to original sources

arXiv2020

Partial Univalence in n-truncated Type Theory

It is well known that univalence is incompatible with uniqueness of identity proofs (UIP), the axiom that all types are h-sets. This is due to finite h-sets having non-trivial automorphisms as soon as they are not h-propositions. A natural question is then whether univalence restricted to h-propositions is compatible with UIP. We answer this affirmatively by constructing a model where types are elements of a closed universe defined as a higher inductive type in homotopy type theory. This universe has a path constructor for simultaneous "partial" univalent completion, i.e., restricted to h-propositions. More generally, we show that univalence restricted to $(n-1)$-types is consistent with the assumption that all types are $n$-truncated. Moreover we parametrize our construction by a suitably well-behaved container, to abstract from a concrete choice of type formers for the universe.

cs.LO↗

arXiv2019

Idempotent completion of cubes in posets

This note concerns the category $\Box$ of cartesian cubes with connections, equivalently the full subcategory of posets on objects $[1]^n$ with $n \geq 0$. We show that the idempotent completion of $\Box$ consists of finite complete posets. It follows that cubical sets, ie presheaves over $\Box$, are equivalent to presheaves over finite complete posets. This yields an alternative exposition of a result by Kapulkin and Voevodsky that simplicial sets form a subtopos of cubical sets.

math.CT↗

arXiv2019

Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus

We observe that normalization by evaluation for simply-typed lambda-calculus with weak coproducts can be carried out in a weak bi-cartesian closed category of presheaves equipped with a monad that allows us to perform case distinction on neutral terms of sum type. The placement of the monad influences the normal forms we obtain: for instance, placing the monad on coproducts gives us eta-long beta-pi normal forms where pi refers to permutation of case distinctions out of elimination positions. We further observe that placing the monad on every coproduct is rather wasteful, and an optimal placement of the monad can be determined by considering polarized simple types inspired by focalization. Polarization classifies types into positive and negative, and it is sufficient to place the monad at the embedding of positive types into negative ones. We consider two calculi based on polarized types: pure call-by-push-value (CBPV) and polarized lambda-calculus, the natural deduction calculus corresponding to focalized sequent calculus. For these two calculi, we present algorithms for normalization by evaluation. We further discuss different implementations of the monad and their relation to existing normalization proofs for lambda-calculus with sums. Our developments have been partially formalized in the Agda proof assistant.

cs.PL↗

arXiv2018

Constructive homotopy theory of marked semisimplicial sets

We develop the homotopy theory of semisimplicial sets constructively and without reference to point-set topology to obtain a constructive model for $ω$-groupoids. Most of the development is folklore, but for a few results the author is unaware of previously known constructive proofs. These include the statements that the unit of the free simplicial set adjunction is valued in weak equivalences and that the geometric product and cartesian product of fibrant semisimplicial sets are weakly equivalent. We then extend the development to marked semisimplicial sets in order to obtain a constructive model for $(ω, 1)$-categories.

math.CT↗

arXiv2017

The Equivalence Extension Property and Model Structures

We give an elementary construction of a certain class of model structures. In particular, we rederive the Kan model structure on simplicial sets without the use of topological spaces, minimal complexes, or any concrete model of fibrant replacement such as Kan's Ex^infinity functor. Our argument makes crucial use of the glueing construction developed by Cohen et al. in the specific setting of certain cubical sets.

math.CT↗

arXiv2017

Space-Valued Diagrams, Type-Theoretically (Extended Abstract)

Topologists are sometimes interested in space-valued diagrams over a given index category, but it is tricky to say what such a diagram even is if we look for a notion that is stable under equivalence. The same happens in (homotopy) type theory, where it is known only for special cases how one can define a type of type-valued diagrams over a given index category. We offer several constructions. We first show how to define homotopy coherent diagrams which come with all higher coherence laws explicitly, with two variants that come with assumption on the index category or on the type theory. Further, we present a construction of diagrams over certain Reedy categories. As an application, we add the degeneracies to the well-known construction of semisimplicial types, yielding a construction of simplicial types up to any given finite level. The current paper is only an extended abstract, and a full version is to follow. In the full paper, we will show that the different notions of diagrams are equivalent to each other and to the known notion of Reedy fibrant diagrams whenever the statement makes sense. In the current paper, we only sketch some core ideas of the proofs.

math.LO↗

arXiv2017

The Frobenius Condition, Right Properness, and Uniform Fibrations

We develop further the theory of weak factorization systems and algebraic weak factorization systems. In particular, we give a method for constructing (algebraic) weak factorization systems whose right maps can be thought of as (uniform) fibrations and that satisfy the (functorial) Frobenius condition. As applications, we obtain a new proof that the Quillen model structure for Kan complexes is right proper, avoiding entirely the use of topological realization and minimal fibrations, and we solve an open problem in the study of Voevodsky's simplicial model of type theory, proving a constructive version of the preservation of Kan fibrations by pushforward along Kan fibrations. Our results also subsume and extend work by Coquand and others on cubical sets.

math.CT↗

arXiv2015

Higher Homotopies in a Hierarchy of Univalent Universes

For Martin-Lof type theory with a hierarchy U(0): U(1): U(2): ... of univalent universes, we show that U(n) is not an n-type. Our construction also solves the problem of finding a type that strictly has some high truncation level without using higher inductive types. In particular, U(n) is such a type if we restrict it to n-types. We have fully formalized and verified our results within the dependently typed language and proof assistant Agda.

math.LO↗