Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / Atom feed
* [HoTT] New preprint : A model of Martin-Löf extensional type theory with universes formalized in Agda ( arXiv:1909.01414)
@ 2019-09-05  7:10 Erik Palmgren
  0 siblings, 0 replies; only message in thread
From: Erik Palmgren @ 2019-09-05  7:10 UTC (permalink / raw)
  To: homotopytypetheory

[-- Attachment #1: Type: text/plain, Size: 1548 bytes --]



From type theory to setoids and back
Erik Palmgren<https://arxiv.org/search/math?searchtype=author&query=Palmgren%2C+E>
(Submitted on 3 Sep 2019)
A model of Martin-Löf extensional type theory with universes is formalized in Agda, an interactive proof system based on Martin-Löf intensional type theory. This may be understood, we claim, as a solution to the old problem of modelling the full extensional theory in the intensional theory. Types are interpreted as setoids, and the model is therefore a setoid model. We solve the problem of intepreting type universes by utilizing Aczel's type of iterative sets, and show how it can be made into a setoid of small setoids containing the necessary setoid constructions.
In addition we interpret the bracket types of Awodey and Bauer. Further quotient types should be interpretable.
Comments:       30 pages
Subjects:       Logic (math.LO)
MSC classes:    03B15, 03B35, 03E70, 03F50
Cite as:        arXiv:1909.01414<https://arxiv.org/abs/1909.01414> [math.LO]
        (or arXiv:1909.01414v1<https://arxiv.org/abs/1909.01414v1> [math.LO] for this version)



https://arxiv.org/abs/1909.01414

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/6AC5AAA7-297B-4644-A116-4182A0FC935E%40math.su.se.

[-- Attachment #2: Type: text/html, Size: 4852 bytes --]

<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">
<div class=""><br class="">
</div>
<div class=""><br class="">
</div>
<div class="">
<h1 class="title mathjax" style="margin: 0.5em 0px 0.5em 20px; line-height: 28.799999237060547px;">
<span style="font-size: 12px;" class="">From type theory to setoids and back</span></h1>
<div class="authors" style="margin: 0.5em 0px 0.5em 20px; line-height: 24px;"><a href="https://arxiv.org/search/math?searchtype=author&amp;query=Palmgren%2C&#43;E" style="text-decoration: none;" class="">Erik Palmgren</a></div>
<div class="dateline" style="margin: 0.5em 0px 0.5em 20px;">(Submitted on 3 Sep 2019)</div>
<blockquote class="mathjax abstract" style="line-height: 1.55; margin-bottom: 1.5em;">
A model of Martin-Löf extensional type theory with universes is formalized in Agda, an interactive proof system based on Martin-Löf intensional type theory. This may be understood, we claim, as a solution to the old problem of modelling the full extensional
 theory in the intensional theory. Types are interpreted as setoids, and the model is therefore a setoid model. We solve the problem of intepreting type universes by utilizing Aczel's type of iterative sets, and show how it can be made into a setoid of small
 setoids containing the necessary setoid constructions.&nbsp;<br class="">
In addition we interpret the bracket types of Awodey and Bauer. Further quotient types should be interpretable.</blockquote>
<div class="metatable" style="line-height: 1.5; margin: 0px 0px 1.5em 20px;">
<table summary="Additional metadata" class="">
<tbody class="">
<tr class="">
<td class="label tablecell" style="padding: 0.1em 0.5em 0em 0em; vertical-align: top;">
<span style="font-size: 12px;" class="">Comments:</span></td>
<td class="comments mathjax tablecell" style="padding: 0.1em 0.5em 0em 0em; vertical-align: top;">
<span style="font-size: 12px;" class="">30 pages</span></td>
</tr>
<tr class="">
<td class="label tablecell" style="padding: 0.1em 0.5em 0em 0em; vertical-align: top;">
<span style="font-size: 12px;" class="">Subjects:</span></td>
<td class="subjects tablecell" style="padding: 0.1em 0.5em 0em 0em; vertical-align: top;">
<span class="primary-subject" style="font-weight: bold; font-size: 12px;">Logic (math.LO)</span></td>
</tr>
<tr class="">
<td class="label tablecell" style="padding: 0.1em 0.5em 0em 0em; vertical-align: top;">
<span style="font-size: 12px;" class=""><abbr title="Mathematical Subject Classification" style="border-bottom-width: 0px;" class="">MSC</abbr>&nbsp;classes:</span></td>
<td class="msc-classes tablecell" style="padding: 0.1em 0.5em 0em 0em; vertical-align: bottom;">
<span style="font-size: 12px;" class="">03B15, 03B35, 03E70, 03F50</span></td>
</tr>
<tr class="">
<td class="label tablecell" style="padding: 0.1em 0.5em 0em 0em; vertical-align: top;">
<span style="font-size: 12px;" class="">Cite as:</span></td>
<td class="arxivid tablecell" style="padding: 0.1em 0.5em 0em 0em; vertical-align: top; font-weight: bold;">
<span class="arxivid" style="font-size: 12px;"><a href="https://arxiv.org/abs/1909.01414" style="text-decoration: none;" class="">arXiv:1909.01414</a>&nbsp;[math.LO]</span></td>
</tr>
<tr class="">
<td class="label tablecell" style="padding: 0.1em 0.5em 0em 0em; vertical-align: top;">
<span style="font-size: 12px;" class="">&nbsp;</span></td>
<td class="arxividv tablecell" style="padding: 0.1em 0.5em 0em 0em; vertical-align: top;">
<span style="font-size: 12px;" class="">(or&nbsp;<span class="arxivid" style="font-weight: bold;"><a href="https://arxiv.org/abs/1909.01414v1" style="text-decoration: none;" class="">arXiv:1909.01414v1</a>&nbsp;[math.LO]</span>&nbsp;for this version)</span></td>
</tr>
</tbody>
</table>
</div>
<div class=""><br class="">
</div>
</div>
<div class=""><br class="">
</div>
<div class=""><br class="">
</div>
<div class=""><a href="https://arxiv.org/abs/1909.01414" class="">https://arxiv.org/abs/1909.01414</a></div>
</body>
</html>

<p></p>

-- <br />
You received this message because you are subscribed to the Google Groups &quot;Homotopy Type Theory&quot; group.<br />
To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br />
To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/6AC5AAA7-297B-4644-A116-4182A0FC935E%40math.su.se?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/6AC5AAA7-297B-4644-A116-4182A0FC935E%40math.su.se</a>.<br />

^ permalink raw reply	[flat|nested] only message in thread

only message in thread, back to index

Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-09-05  7:10 [HoTT] New preprint : A model of Martin-Löf extensional type theory with universes formalized in Agda ( arXiv:1909.01414) Erik Palmgren

Discussion of Homotopy Type Theory and Univalent Foundations

Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott

Example config snippet for mirrors

Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.hott


AGPL code for this site: git clone https://public-inbox.org/public-inbox.git