[Agda] Recursion on transfinite numbers.

[Serge Leblanc]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20250219/1bc88571/attachment.html>
-------------- next part --------------
{-# OPTIONS --cubical --safe #-}

module HITOrdinal where

open import Cubical.Core.Primitives using (_≡_; Level; Type)
open import Cubical.Foundations.Prelude using (_∙_; refl; isSet; isProp; cong; PathP; toPathP; isProp→isSet)
open import Cubical.Foundations.HLevels using (isOfHLevel→isOfHLevelDep)
open import Cubical.Data.Nat using (ℕ; zero; suc)


open import Cubical.Foundations.Everything public


variable ℓ ℓ' ℓ'' : Level


private
 variable
  A : Type ℓ
  x y z : A

infix  1 begin_
infixr 2 _≡⟨_⟩_
infix  3 _∎

begin_ : x ≡ y → x ≡ y
begin x≡y = x≡y

_≡⟨_⟩_ : (x : A) → x ≡ y → y ≡ z → x ≡ z
x ≡⟨ x≡y ⟩ y≡z = x≡y ∙ y≡z

_∎ : (x : A) → x ≡ x
_ ∎ = refl

infixr 40 ω^_⊕_

data HITOrd : Type₀ where
  𝟎 : HITOrd
  ω^_⊕_ : HITOrd → HITOrd → HITOrd
  swap : ∀ a b c → ω^ a ⊕ ω^ b ⊕ c ≡ ω^ b ⊕ ω^ a ⊕ c
  trunc : isSet HITOrd

fromNat : ℕ → HITOrd
fromNat zero = 𝟎
fromNat (suc n) = ω^ 𝟎 ⊕ (fromNat n)


ind : (A : HITOrd → Type ℓ)
    → (a₀    : A 𝟎)
    → (_⋆_   : ∀ {x y} → A x → A y → A (ω^ x ⊕ y))
    → (⋆swap : ∀ {x y z} (a : A x) (b : A y) (c : A z)
             → PathP _ (a ⋆ (b ⋆ c)) (b ⋆ (a ⋆ c)))
    → (sv    : ∀ {x} → isSet (A x))
    → ∀ x → A x
ind A a₀ _⋆_ ⋆swap sv 𝟎 = a₀
ind A a₀ _⋆_ ⋆swap sv (ω^ x ⊕ y) = ind A a₀ _⋆_ ⋆swap sv x ⋆ ind A a₀ _⋆_ ⋆swap sv y
ind A a₀ _⋆_ ⋆swap sv (swap x y z i) = ⋆swap
        (ind A a₀ _⋆_ ⋆swap sv x)
        (ind A a₀ _⋆_ ⋆swap sv y)
        (ind A a₀ _⋆_ ⋆swap sv z) i
ind A a₀ _⋆_ ⋆swap sv (trunc a b p q i₁ i₂) = {! isOfHLevel→isOfHLevelDep 2  !}

{-
indProp : {P : HITOrd → Type ℓ}
        → (∀ {x} → isProp (P x))
        → P 𝟎
        → (∀ {x y} → P x → P y → P (ω^ x ⊕ y))
        → ∀ x → P x
indProp pv p₀ _⋆_ =
  ind _ p₀ _⋆_ (λ a b c → toPathP (pv _ _)) (isProp→isSet pv _ _)
-}

example : (a b c : HITOrd) → ω^ a ⊕ ω^ b ⊕ ω^ c ⊕ 𝟎 ≡ ω^ c ⊕ ω^ b ⊕ ω^ a ⊕ 𝟎
example a b c = begin
    ω^ a ⊕ ω^ b ⊕ ω^ c ⊕ 𝟎 ≡⟨ swap a b _ ⟩
    ω^ b ⊕ ω^ a ⊕ ω^ c ⊕ 𝟎 ≡⟨ cong (ω^ b ⊕_) (swap a c _) ⟩
    ω^ b ⊕ ω^ c ⊕ ω^ a ⊕ 𝟎 ≡⟨ swap b c _ ⟩
    ω^ c ⊕ ω^ b ⊕ ω^ a ⊕ 𝟎 ∎

ω^⟨_⟩ : HITOrd → HITOrd
ω^⟨ a ⟩ = ω^ a ⊕ 𝟎

𝟏 ω : HITOrd
𝟏 = ω^⟨ 𝟎 ⟩
ω = ω^⟨ 𝟏 ⟩
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0xD2B8A2825F8DABB7.asc
Type: application/pgp-keys
Size: 1400 bytes
Desc: OpenPGP public key
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20250219/1bc88571/attachment.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature.asc
Type: application/pgp-signature
Size: 236 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20250219/1bc88571/attachment.sig>