<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; color: rgb(0, 0, 0); font-size: 14px; font-family: Calibri, sans-serif; "><div><br></div><div><br></div><span id="OLK_SRC_BODY_SECTION"><blockquote style="margin:0 0 0 40px; border:none; padding:0px;"><div style="font-family:Calibri; font-size:11pt; text-align:left; color:black; BORDER-BOTTOM: medium none; BORDER-LEFT: medium none; PADDING-BOTTOM: 0in; PADDING-LEFT: 0in; PADDING-RIGHT: 0in; BORDER-TOP: #b5c4df 1pt solid; BORDER-RIGHT: medium none; PADDING-TOP: 3pt"><span style="font-weight:bold">From: </span> Thorsten Altenkirch <<a href="mailto:psztxa@exmail.nottingham.ac.uk">psztxa@exmail.nottingham.ac.uk</a>><br><span style="font-weight:bold">To: </span> Peter Hancock <<a href="mailto:hancock@spamcop.net">hancock@spamcop.net</a>>, Agda List <<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>><br><span style="font-weight:bold">Subject: </span> Re: [Agda] Re: eta expansion<br></div><div><br></div></blockquote><span style="color: rgb(0, 0, 0); font-family: Calibri, sans-serif; font-size: 14px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; display: inline !important; float: none; "><blockquote style="margin:0 0 0 40px; border:none; padding:0px;">Indeed the universe of finite sets (U=Nat,T=Fin) is univalent and this is easily provable in vanilla type theory (without univalence).</blockquote></span></span><div><br></div><div>I have to correct myself:</div><div><br></div><div>This is incorrect while isomorphism is logically equivalent to equality of the codes (natural numbers), this is not an isomorphism since the equality of numbers is propositional but the isomorphism is obviously not. Indeed, the only univalent universe in vanilla type theory is (Bool,isTrue). </div><div><br></div><div>To construct a univalent universe of finite sets one would need to use a higher inductive type.</div><div><br></div><div>Thorsten</div><span id="OLK_SRC_BODY_SECTION"><span style="color: rgb(0, 0, 0); font-family: Calibri, sans-serif; font-size: 14px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; display: inline !important; float: none; "><span class="Apple-converted-space"><blockquote style="margin:0 0 0 40px; border:none; padding:0px;"> </blockquote></span></span></span>
<br><br>
<br></body></html>