[Agda] Explicit definition.

[Serge Leblanc]

Hi,

I can't seem to make an explicit definition of ⊕unitr in my example.

Can someone help me and explain my mistake?

Thanks.

-- 
Serge Leblanc
-------------------------
gpg --search-keys 0xD2B8A2825F8DABB7
GnuPG Fingerprint = 123E 9312 453A 8F8E 7FDB ABD7 D2B8 A282 5F8D ABB7

-------------- 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 (isSet→SquareP)
open import Cubical.Foundations.Everything public
open import Cubical.Data.Nat using (ℕ; zero; suc)
open import Cubical.Data.Sigma

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 ω^_⊕_
-- infix 30 _≤_ _≥_

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

_⊕_ : HITOrd → HITOrd → HITOrd
𝟎 ⊕ y = y
(ω^ a ⊕ b) ⊕ y = ω^ a ⊕ (b ⊕ y)
(swap a b c i) ⊕ y = swap a b (c ⊕ y) i
(trunc a b p q i j) ⊕ y = trunc (a ⊕ y) (b ⊕ y)
    (congS (λ x → x ⊕ y) p)
    (congS (λ x → x ⊕ y) q)
    i j

{-

_+ₒ_ : HITOrd → HITOrd → HITOrd

_≤_ _≥_ : HITOrd → HITOrd → Type₀
m ≤ n = Σ[ k ∈ HITOrd ] k +ₒ m ≡ n
m ≥ n = n ≤ m
m < n = (ω^ 𝟎 ⊕ m) ≤ n
m > n = n < m

-- _+ₒ_ : HITOrd → HITOrd → HITOrd
𝟎 +ₒ b = b
a@(ω^ _ ⊕ _) +ₒ 𝟎 = a
(ω^ a ⊕ a₁) +ₒ (ω^ b ⊕ b₁) with a

swap a a₁ a₂ i +ₒ b = {!   !}
trunc a a₁ x y i i₁ +ₒ b = {!   !}
a +ₒ swap b b₁ b₂ i = {!   !}
a +ₒ trunc b b₁ x y i i₁ = {!   !}


Trichotomy-suc : Trichotomy m n → Trichotomy (suc m) (suc n)
Trichotomy-suc (lt m<n) = lt (suc-≤-suc m<n)
Trichotomy-suc (eq m=n) = eq (cong suc m=n)
Trichotomy-suc (gt n<m) = gt (suc-≤-suc n<m)

_≟_ : ∀ m n → Trichotomy m n
zero ≟ zero = eq refl
zero ≟ suc n = lt (n , +-comm n 1)
suc m ≟ zero = gt (m , +-comm m 1)
suc m ≟ suc n = Trichotomy-suc (m ≟ 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 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

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

⊕unitl : (a : HITOrd) → 𝟎 ⊕ a ≡ a
⊕unitl a = refl

{-
⊕unitr : (a : HITOrd) → a ⊕ 𝟎 ≡ a
⊕unitr 𝟎 = refl
⊕unitr (ω^ a ⊕ b) = congS (λ x → ω^ a ⊕ x) (⊕unitr b)
⊕unitr (swap a a₁ a₂ i) = congS (λ x → swap a a₁ x i) (⊕unitr a₂)
⊕unitr (trunc a b x y i j) = {! trunc (⊕unitr a) (⊕unitr b) (cong ⊕unitr x) (cong ⊕unitr y) i j  !}
-}
-- isProp→isSet : ∀ {ℓ} {A : Type ℓ} → isProp A → isSet A
-- isProp→isSet pA x y p q i j = pA (p i0) (q j0)

⊕unitr : (a : HITOrd) → a ⊕ 𝟎 ≡ a
⊕unitr 𝟎 = refl
⊕unitr (ω^ a ⊕ b) = congS (ω^ a ⊕_) (⊕unitr b)
⊕unitr (swap a b c i) = congS (λ x → swap a b x i) (⊕unitr c)
⊕unitr (trunc a b x y i j) = isSet→SquareP
  {A = λ i j → trunc (a ⊕ 𝟎) (b ⊕ 𝟎) (λ k → x k ⊕ 𝟎) (λ k → y k ⊕ 𝟎) i j ≡ trunc a b x y i j}
  {! (λ i j → trunc _ _) !}
  (λ j → ⊕unitr (x j))
  (λ j → ⊕unitr (y j))
  refl refl i j


{-
⊕unitr : (a : HITOrd) → a ⊕ 𝟎 ≡ a
⊕unitr = indProp trunc base step
 where
  base : 𝟎 ⊕ 𝟎 ≡ 𝟎
  base = refl
  step : ∀ {x y} → _ → y ⊕ 𝟎 ≡ y
       → (ω^ x ⊕ y) ⊕ 𝟎 ≡ ω^ x ⊕ y
  step {x} _ = cong (ω^ x ⊕_)
-}


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

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

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

𝟏 ω ωꙻ : HITOrd
𝟏 = ω^⟨ 𝟎 ⟩
ω = ω^⟨ 𝟏 ⟩
ωꙻ = ω^⟨ ω ⟩

private
  1≡𝟏 : fromNat 1 ≡ 𝟏
  1≡𝟏 = refl


{-
_ₙx_ : ℕ → HITOrd → HITOrd
zero ₙx o = 𝟎
suc n ₙx o = o +ₒ (n ₙx o)

_⋗_ : ℕ × ℕ → HITOrd → HITOrd
(zero , b) ⋗ o = {! fromNat b !}
(suc a , b) ⋗ o = {!   !}
-}
-------------- 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/20250304/5e05e5ba/attachment-0001.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/20250304/5e05e5ba/attachment-0001.sig>