[Agda] Recursion on transfinite numbers.

[Naïm Favier]

Hi,

ind A a₀ _⋆_ ⋆swap sv (trunc a b p q i j) = isSet→SquareP
   {A = λ i j → A (trunc a b p q i j)}
   (λ _ _ → sv)
   (λ j → ind A a₀ _⋆_ ⋆swap sv (p j))
   (λ j → ind A a₀ _⋆_ ⋆swap sv (q j))
   refl refl i j

On 19/02/2025 12:46, Serge Leblanc wrote:
> 	
> Some people who received this message don't often get email from 33dbqnxpy7if at gmail.com. Learn why this is important <https://aka.ms/LearnAboutSenderIdentification>
> 	
> 
> 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