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…
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…
Space-Valued Diagrams, Type-Theoretically (Extended Abstract)
Nicolai Kraus, Christian Sattler
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 stabl…
Higher Homotopies in a Hierarchy of Univalent Universes
Nicolai Kraus, Christian Sattler
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…