<!DOCTYPE html><html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<p>Dear Serge,</p>
<p>I'm not sure which notion of transfinite numbers you have in
mind, but I have just updated our development at<br>
</p>
<p><a class="moz-txt-link-freetext" href="https://bitbucket.org/nicolaikraus/constructive-ordinals-in-hott/">https://bitbucket.org/nicolaikraus/constructive-ordinals-in-hott/</a><br>
</p>
<p>to work with the latest versions of Agda and the cubical library.
Hopefully that helps, otherwise I'm of course happy to discuss
further!</p>
<p>Best wishes,<br>
Fred<br>
</p>
<p><br>
</p>
<div class="moz-cite-prefix">On 19/02/2025 11:46, Serge Leblanc
wrote:<br>
</div>
<blockquote type="cite" cite="mid:329acd36-e94d-464e-855e-9a5ace21e622@gmail.com">
<div style="background-color:#fff2e6; border:2px dotted #ff884d"><span style="font-size:12pt; font-family:sans-serif; color:black; font-weight:bold; padding:.2em">CAUTION:
This email originated outside the University. Check before
clicking links or attachments.
</span><br>
</div>
<div>
<p>Dear All,</p>
<p>Can someone help me to realize the principle of recursion on
transfinite numbers ?
<br>
I based it on the work of Fredrik Nordvall Forsberg but he
uses an old version of the Cubical libraries.<br>
</p>
<p>Cordialement,<br>
</p>
<div class="moz-signature">-- <br>
Serge Leblanc
<hr>
gpg --search-keys 0xD2B8A2825F8DABB7 <br>
GnuPG Fingerprint = 123E 9312 453A 8F8E 7FDB ABD7 D2B8 A282
5F8D ABB7</div>
</div>
<br>
<fieldset class="moz-mime-attachment-header"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
</body>
</html>