<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Aptos;
panose-1:2 11 0 4 2 2 2 2 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
font-size:11.0pt;
font-family:"Aptos",sans-serif;
mso-ligatures:standardcontextual;
mso-fareast-language:EN-US;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#467886;
text-decoration:underline;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:11.0pt;
mso-ligatures:none;
mso-fareast-language:EN-US;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="EN-GB" link="#467886" vlink="#96607D" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal"><span style="color:black">Hi,<br>
<br>
On Monday, the MSP101 talk will be given by </span>Fredrik Nordvall Forsberg<span style="color:black"> (MSP). See the details of the talk below.<o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="color:black"><br>
Best,<br>
Dilsat<br>
<br>
**********************************************************************<br>
<br>
Date: Monday, 3 March at 15:00<br>
<br>
Room: LT412, Livingstone Tower<br>
<br>
Zoom link: <a href="https://strath.zoom.us/j/85449272187?pwd=0qNkQqybiaKgBpbEBRv38x11x4db5n.1" target="_blank" title="https://strath.zoom.us/j/85449272187?pwd=0qNkQqybiaKgBpbEBRv38x11x4db5n.1"><span style="color:#96607D">https://strath.zoom.us/j/85449272187?pwd=0qNkQqybiaKgBpbEBRv38x11x4db5n.1</span></a><o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black">Live stream on Youtube: <a href="https://www.youtube.com/@msp101strathclyde4">
https://www.youtube.com/@msp101strathclyde4</a> <br>
<br>
Speaker: </span>Fredrik Nordvall Forsberg<span style="color:black"><br>
<br>
Title: </span>Representing type theory in type theory<span style="color:black"><o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="color:black"> <o:p></o:p></span></p>
<p class="MsoNormal" style="caret-color: rgb(0, 0, 0);font-variant-caps: normal;orphans: auto;text-align:start;widows: auto;-webkit-text-stroke-width: 0px;word-spacing:0px">
<span style="color:black">Abstract: </span>It is often claimed that type theory can act as a foundation of mathematics. If that is so, then type theory should in particular be able to reason about type theory itself. Of course, Dr Gödel points out that this
cannot work, in general, but we would expect that type theory could still reason about a slightly weaker version of itself. This turns out to be true, but messy, because type theory is quite complicated as a theory. After heroic attempts by Danielsson (2006)
and Chapman (2009) to represent type theory internally in type theory, Altenkirch and Kaposi (2016) made a breakthrough in using so-called quotient inductive-inductive types to represent the well typed terms of type theory, where quotient constructors are
used to encode beta and eta laws as equalities in the type. Being able to treat such laws as actual equalities is a major improvement, but quickly leads into so-called transport hell, where explicit transports along equalities show up in terms and needs to
be reasoned about. I will report on some recent work together with Liang-Ting Chen and Tzu-Chun Tsai on how one can use experimental (and hopefully future) features of Agda to improve on the quotient inductive-inductive representation and remove most uses
of transport.</p>
<p class="MsoNormal"><span style="color:black"><br>
**********************************************************************<o:p></o:p></span></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>