S.agda

{-# OPTIONS --cubical #-}
module S where

open import Cubical.Core.Everything
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Transport
open import Cubical.Foundations.HLevels
open import Cubical.Categories.Category
open import Cubical.Data.Sigma
open import Cubical.Data.Sum
open import Cubical.Data.Unit
open import Cubical.Data.Nat using (ℕ; zero; suc)

pattern 3+_ n = suc (suc (suc n))
pattern 2+_ n = suc (suc n)
pattern 1+_ n = suc n

infixl 6 _+_

-- The semiring ℕ[X]/(X≡X²+1)
data ℕ[X]/tree : Type where
  _+_ : ℕ[X]/tree → ℕ[X]/tree → ℕ[X]/tree
  X^ : ℕ → ℕ[X]/tree
  +-comm : {a b : ℕ[X]/tree} → a + b ≡ b + a
  +-assoc : {a b c : ℕ[X]/tree} → a + b + c ≡ a + (b + c)
  tree : ∀ n → X^ (1+ n) ≡ X^ (2+ n) + X^ n

data Tree : Type where
   inj : (Tree × Tree) ⊎ Unit → Tree

⊎-comm : ∀ {A B : Type} → A ⊎ B ≡ B ⊎ A
⊎-comm = isoToPath ⊎-swap-Iso

⊎-assoc : ∀ {A B C : Type} → (A ⊎ B) ⊎ C ≡ A ⊎ (B ⊎ C)
⊎-assoc = isoToPath ⊎-assoc-Iso

open Iso

Iso-Tree-tree : (A : Type) → Iso (Tree × A) ((Tree × Tree × A) ⊎ A)
Iso-Tree-tree A .fun (inj (inl (t₁ , t₂)) , a) = inl (t₁ , t₂ , a)
Iso-Tree-tree A .fun (inj (inr tt) , a) = inr a
Iso-Tree-tree A .inv (inl (t₁ , t₂ , a)) = inj (inl (t₁ , t₂)) , a
Iso-Tree-tree A .inv (inr a) = inj (inr tt) , a
Iso-Tree-tree A .rightInv (inl (t₁ , t₂ , a)) = refl
Iso-Tree-tree A .rightInv (inr a) = refl
Iso-Tree-tree A .leftInv (inj (inl (t₁ , t₂)) , a) = refl
Iso-Tree-tree A .leftInv (inj (inr tt) , a) = refl

Tree-tree : (A : Type) → (Tree × A) ≡ ((Tree × Tree × A) ⊎ A)
Tree-tree A = isoToPath (Iso-Tree-tree A)

toType : ℕ[X]/tree → Type
toType (a + b) = toType a ⊎ toType b
toType (X^ 0) = Unit
toType (X^ (1+ n)) = Tree × toType (X^ n)
toType (+-comm {a} {b} i) = ⊎-comm {toType a} {toType b} i
toType (+-assoc {a} {b} {c} i) = ⊎-assoc {toType a} {toType b} {toType c} i
toType (tree n i) = Tree-tree (toType (X^ n)) i

{-
/home/sam/code/scratch/S.agda:56,1-7
toType (+-comm i0) != toType x ⊎ toType x₁ of type Type
when checking the definition of toType
-}