38 citations · 95 across the 13 of their papers we have counts for
4 papers · 1 filter
Constructive sheaf models of type theory
Thierry Coquand, Fabian Ruch, Christian Sattler
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 mo…
The constructive Kan-Quillen model structure: two new proofs
Nicola Gambino, Christian Sattler, Karol Szumiło
We present two new proofs of Simon Henry's result that the category of simplicial sets admits a constructive counterpart of the classical Kan-Quillen model structure. Our proofs ar…
Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus
Andreas Abel, Christian Sattler
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 w…
Canonicity and homotopy canonicity for cubical type theory
Thierry Coquand, Simon Huber, Christian Sattler
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 comput…