Setoids in type theory

2003 ◽  
Vol 13 (2) ◽  
pp. 261-293 ◽  
Author(s):  
GILLES BARTHE ◽  
VENANZIO CAPRETTA ◽  
OLIVIER PONS

Formalising mathematics in dependent type theory often requires to represent sets as setoids, i.e. types with an explicit equality relation. This paper surveys some possible definitions of setoids and assesses their suitability as a basis for developing mathematics. According to whether the equality relation is required to be reflexive or not we have total or partial setoid, respectively. There is only one definition of total setoid, but four different definitions of partial setoid, depending on four different notions of setoid function. We prove that one approach to partial setoids in unsuitable, and that the other approaches can be divided in two classes of equivalence. One class contains definitions of partial setoids that are equivalent to total setoids; the other class contains an inherently different definition, that has been useful in the modeling of type systems. We also provide some elements of discussion on the merits of each approach from the viewpoint of formalizing mathematics. In particular, we exhibit a difficulty with the common definition of subsetoids in the partial setoid approach.

2004 ◽  
Vol 14 (1) ◽  
pp. 1-2
Author(s):  
GILLES BARTHE ◽  
PETER DYBJEN ◽  
PETER THIEMANN

Modern programming languages rely on advanced type systems that detect errors at compile-time. While the benefits of type systems have long been recognized, there are some areas where the standard systems in programming languages are not expressive enough. Language designers usually trade expressiveness for decidability of the type system. Some interesting programs will always be rejected (despite their semantical soundness) or be assigned uninformative types.


2015 ◽  
Vol 25 (5) ◽  
pp. 1010-1039 ◽  
Author(s):  
BENEDIKT AHRENS ◽  
KRZYSZTOF KAPULKIN ◽  
MICHAEL SHULMAN

We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition of ‘category’ for which equality and equivalence of categories agree. Such categories satisfy a version of the univalence axiom, saying that the type of isomorphisms between any two objects is equivalent to the identity type between these objects; we call them ‘saturated’ or ‘univalent’ categories. Moreover, we show that any category is weakly equivalent to a univalent one in a universal way. In homotopical and higher-categorical semantics, this construction corresponds to a truncated version of the Rezk completion for Segal spaces, and also to the stack completion of a prestack.


2001 ◽  
Vol 11 (4) ◽  
pp. 437-437
Author(s):  
Gilles Barthe ◽  
Peter Dybjer ◽  
Peter Thiemann

Modern programming languages rely on advanced type systems that detect errors at compile-time. While the benefits of type systems have long been recognized, there are some areas where the standard systems in programming languages are not expressive enough. Language designers usually trade expressiveness for decidability of the type system. Some interesting programs will always be rejected (despite their semantical soundness) or be assigned uninformative types.There are several remedies to this situation. Dependent type systems, which allow the formation of types that explicitly depend on other types or values, are one of the most promising approaches. These systems are well-investigated from a theoretical point of view by logicians and type theorists. For example, dependent types are used in proof assistants to implement various logics and there are sophisticated proof editors for developing programs in a dependently typed language.To the present day, the impact of these developments on practical programming has been small, partially because of the level of sophistication of these systems and of their type checkers. Only recently, there have been efforts to integrate dependent systems into intermediate languages in compilers and programming languages. Additional uses have been identified in high-profile applications such as mobile code security, where terms of a dependently typed lambda calculus to encode safety proofs.A special issue of the Journal of Functional Programming will be devoted to the interplay between dependent type theory and programming practice. We welcome technical contributions in the field, as well as position papers that:[bull ] make researchers in programming languages aware of new developments and research directions on the theory side;[bull ] point out to theorists practical uses of advanced type systems and urge them to address theoretical problems arising in emerging applications.Authors who are concerned about the appropriateness of a topic are welcome to contact the guest editors. Manuscripts should be unpublished works and not submitted elsewhere. Revised and enhanced versions of papers published in conference proceedings that have not appeared in archival journals are eligible for submission. All submissions will be reviewed according to the usual standards of scholarship and originality.Submissions should be sent to Gilles Barthe ([email protected]), with a copy to Nasreen Ahmad ([email protected]). Submitted articles should be sent in postscript format, preferably gzipped and uuencoded. In addition, please send, as plain text, title, abstract and contact information.The submission deadline is December 1st, 2001.


Author(s):  
Avtandil kyzy Ya

Abstract: This paper highlights similarities and different features of the category of kinesics “hand gestures”, its frequency usage and acceptance by different individuals in two different cultures. This study shows its similarities, differences and importance of the gestures, for people in both cultures. Consequently, kinesics study was mentioned as a main part of body language. As indicated in the article, the study kinesics was not presented in the Kyrgyz culture well enough, though Kyrgyz people use hand gestures a lot in their everyday life. The research paper begins with the common definition of hand gestures as a part of body language, several handshake categories like: the finger squeeze, the limp fish, the two-handed handshake were explained by several statements in the English and Kyrgyz languages. Furthermore, this article includes definitions and some idioms containing hand, shake, squeeze according to the Oxford and Academic Dictionary to show readers the figurative meanings of these common words. The current study was based on the books of writers Allan and Barbara Pease “The definite book of body language” 2004, Romana Lefevre “Rude hand gestures of the world”2011 etc. Key words: kinesics, body language, gestures, acoustics, applause, paralanguage, non-verbal communication, finger squeeze, perceptions, facial expressions. Аннотация. Бул макалада вербалдык эмес сүйлѳшүүнүн бѳлүгү болуп эсептелген “колдордун жандоо кыймылы”, алардын эки башка маданиятта колдонулушу, айырмачылыгы жана окшош жактары каралган. Макаланын максаты болуп “колдордун жандоо кыймылынын” мааниси, айырмасы жана эки маданиятта колдонулушу эсептелет. Ошону менен бирге, вербалдык эмес сүйлѳшүүнүн бѳлүгү болуп эсептелген “кинесика” илими каралган. Берилген макалада кѳрсѳтүлгѳндѳй, “кинесика” илими кыргыз маданиятында толугу менен изилденген эмес, ошого карабастан “кинесика” илиминин бѳлүгү болуп эсептелген “колдордун жандоо кыймылы” кыргыз элинин маданиятында кѳп колдонулат. Андан тышкары, “колдордун жандоо кыймылынын” бир нече түрү, англис жана кыргыз тилдеринде ма- селен аркылуу берилген.Тѳмѳнкү изилдѳѳ ишин жазууда чет элдик жазуучулардын эмгектери колдонулду. Түйүндүү сѳздѳр: кинесика, жандоо кыймылы, акустика,кол чабуулар, паралингвистика, вербалдык эмес баарлашуу,кол кысуу,кабыл алуу сезими. Аннотация. В данной статье рассматриваются сходства и различия “жестикуляции” и частота ее использования, в американской и кыргызской культурах. Следовательно, здесь было упомянуто понятие “кинесика” как основная часть языка тела. Как указано в статье, “кинесика” не была представлена в кыргызской культуре достаточно хорошо, хотя кыргызский народ часто использует жестикуляцию в повседневной жизни. Исследовательская работа начинается с общего определения “жестикуляции” как части языка тела и несколько категорий жестикуляции, таких как: сжатие пальца, слабое рукопожатие, рукопожатие двумя руками, были объяснены несколькими примерами на английском и кыргызском языках. Кроме того, эта статья включает определения слов “рука”, “рукопожатие”, “сжатие” и некоторые идиомы, содержащие данных слов согласно Оксфордскому и Академическому словарю, чтобы показать читателям их образное значение. Данное исследование было основано на книгах писателей Аллана и Барбары Пиз «Определенная книга языка тела» 2004 года, Романа Лефевра «Грубые жестикуляции мира» 2011 года и т.д. Ключевые слова: кинесика, язык жестов, жесты, акустика, аплодисменты, паралингвистика, невербальная коммуникация, сжатие пальца, чувство восприятия, выражение лиц.


2021 ◽  
Vol 31 ◽  
Author(s):  
ANDREA VEZZOSI ◽  
ANDERS MÖRTBERG ◽  
ANDREAS ABEL

Abstract Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types (HITs). This paper describes an extension of the dependently typed functional programming language Agda with cubical primitives, making it into a full-blown proof assistant with native support for univalence and a general schema of HITs. These new primitives allow the direct definition of function and propositional extensionality as well as quotient types, all with computational content. Additionally, thanks also to copatterns, bisimilarity is equivalent to equality for coinductive types. The adoption of cubical type theory extends Agda with support for a wide range of extensionality principles, without sacrificing type checking and constructivity.


2014 ◽  
Vol 49 (1) ◽  
pp. 503-515 ◽  
Author(s):  
Robert Atkey ◽  
Neil Ghani ◽  
Patricia Johann

2019 ◽  
Vol 3 (ICFP) ◽  
pp. 1-29 ◽  
Author(s):  
Daniel Gratzer ◽  
Jonathan Sterling ◽  
Lars Birkedal

Author(s):  
Aleš Bizjak ◽  
Hans Bugge Grathwohl ◽  
Ranald Clouston ◽  
Rasmus E. Møgelberg ◽  
Lars Birkedal

Sign in / Sign up

Export Citation Format

Share Document