To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

A generalization of the T… - University of Gothenburg, Sweden Till startsida
To content Read more about how we use cookies on

A generalization of the Takeuti-Gandy interpretation

Journal article
Authors B. Barras
Thierry Coquand
Simon Huber
Published in Mathematical Structures in Computer Science
Volume 25
Issue 5
Pages 1071-1099
ISSN 0960-1295
Publication year 2015
Published at Department of Computer Science and Engineering, Computing Science, Programming Logic
Department of Computer Science and Engineering (GU)
Pages 1071-1099
Language en
Keywords IDENTITY, Computer Science, Theory & Methods
Subject categories Computer and Information Science


We present an interpretation of a version of dependent type theory where a type is interpreted by a Kan semisimplicial set. This interprets only a weak notion of conversion similar to the one used in the first published version of Martin-Lof type theory. Each truncated version of this model can be carried out internally in dependent type theory, and we have formalized the first truncated level, which is enough to represent isomorphisms of algebraic structure as equality.

Page Manager: Webmaster|Last update: 9/11/2012

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?