[Agda] Recursion on transfinite numbers.

[Fredrik Nordvall Forsberg]

Dear Serge,

I'm not sure which notion of transfinite numbers you have in mind, but I 
have just updated our development at

https://bitbucket.org/nicolaikraus/constructive-ordinals-in-hott/

to work with the latest versions of Agda and the cubical library. 
Hopefully that helps, otherwise I'm of course happy to discuss further!

Best wishes,
Fred


On 19/02/2025 11:46, Serge Leblanc wrote:
> CAUTION: This email originated outside the University. Check before 
> clicking links or attachments.
>
> Dear All,
>
> Can someone help me to realize the principle of recursion on 
> transfinite numbers ?
> I based it on the work of Fredrik Nordvall Forsberg but he uses an old 
> version of the Cubical libraries.
>
> Cordialement,
>
> -- 
> Serge Leblanc
> ------------------------------------------------------------------------
> gpg --search-keys 0xD2B8A2825F8DABB7
> GnuPG Fingerprint = 123E 9312 453A 8F8E 7FDB ABD7 D2B8 A282 5F8D ABB7
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20250219/764b4252/attachment-0001.html>