M-type (the type of non-well-founded, labelled trees) [ag-000J]

{-# OPTIONS --cubical --guardedness --two-level --no-level-universe #-}
module ag-000J where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sum
open import Cubical.Data.Nat

data 𝟘 : Type where
data 𝟙 : Type where
  ⋆ : 𝟙
data Maybe (X : Type) : Type where
  none : Maybe X
  some : X → Maybe X
record ℕ∞ : Type where
  coinductive
  field
    pred∞ : Maybe ℕ∞

M-type 是 non-well-formed, labelled trees 的型別，有可能有有限也可能有無限長的 path。 M 是 strictly positive coinductive types 的 universal type。

record M (S : Type) (P : S → Type) : Type where
  coinductive
  field
    shape : S
    pos : P shape → M S P

M S P 代表了 conatural number

module conatural-number where
  open ℕ∞
  open M

  S = 𝟙 ⊎ 𝟙

  P : S → Type
  P (inl _) = 𝟘
  P (inr _) = 𝟙

  N∞ = M S P

  inf : ℕ∞
  pred∞ inf = none
  inf' : ℕ∞
  pred∞ inf' = some inf

  i : N∞
  shape i = inl ⋆
  pos i = λ ()

  i' : N∞
  shape i' = inr ⋆
  pos i' = λ x → i