{-# OPTIONS --copatterns --sized-types #-}

module SizedInfiniteTypes where

open import Library

-- * Types
------------------------------------------------------------------------

-- Infinite type expressions

mutual
  data Ty {i : Size} : Set where
    -- 1̂   : Ty {i}
    -- _+̂_ : ∀ (a b : Ty {i}) → Ty {i}
    _×̂_ : ∀ (a b : Ty {i}) → Ty {i}
    _→̂_ : ∀ (a b : Ty {i}) → Ty {i}
    ▸̂_  : ∀ (a∞ : ∞Ty {i}) → Ty {i}

  record ∞Ty {i : Size} : Set where
    coinductive
    constructor delay_
    field       force_ : ∀{j : Size< i} → Ty {j}
open ∞Ty public

▸_ : ∀{i} → Ty {i} → Ty {↑ i}
▸ A = ▸̂ delay A

_⇒_ : ∀{i} (a∞ b∞ : ∞Ty {i}) → ∞Ty {i}
force (a∞ ⇒ b∞) = force a∞ →̂ force b∞

-- Guarded fixpoint types (needs sized types)

μ̂ : ∀{i} → (∀{j : Size< i} → ∞Ty {j} → Ty {j}) → ∞Ty {i}
(force (μ̂ {i} F)) {j} = F (μ̂ {j} F)

-- Type equality

mutual
  data _≅_ : (a b : Ty) → Set where
    _×̂_ : ∀{a a' b b'} (a≅ : a ≅ a') (b≅ : b ≅ b') → (a ×̂ b) ≅ (a' ×̂ b')
    _→̂_ : ∀{a a' b b'} (a≅ : a' ≅ a) (b≅ : b ≅ b') → (a →̂ b) ≅ (a' →̂ b')
    ▸̂_  : ∀{a∞ b∞}     (a≅ : a∞ ∞≅ b∞)             → ▸̂ a∞    ≅ ▸̂ b∞

  record _∞≅_ (a∞ b∞ : ∞Ty) : Set where
    coinductive
    constructor ≅delay
    field       ≅force : force a∞ ≅ force b∞
open _∞≅_ public

mutual
  ≅refl  : ∀{a} → a ≅ a
  ≅refl {a ×̂ b} = (≅refl {a}) ×̂ (≅refl {b})
  ≅refl {a →̂ b} = (≅refl {a}) →̂ (≅refl {b})
  ≅refl {▸̂ a∞ } = ▸̂ (≅refl∞ {a∞})

  ≅refl∞ : ∀{a∞} → a∞ ∞≅ a∞
  ≅force ≅refl∞ = ≅refl

mutual
  ≅sym : ∀ {a b} → a ≅ b → b ≅ a
  ≅sym (eq ×̂ eq₁) = (≅sym eq) ×̂ (≅sym eq₁)
  ≅sym (eq →̂ eq₁) = (≅sym eq) →̂ (≅sym eq₁)
  ≅sym (▸̂ a≅) = ▸̂  (≅sym∞ a≅)

  ≅sym∞ : ∀{a∞ b∞} → a∞ ∞≅ b∞ → b∞ ∞≅ a∞
  ≅force (≅sym∞ eq) = ≅sym (≅force eq)

mutual
  ≅trans : ∀ {a b c} → a ≅ b → b ≅ c → a ≅ c
  ≅trans (eq₁ ×̂ eq₂) (eq₁' ×̂ eq₂') = (≅trans eq₁ eq₁') ×̂ (≅trans eq₂ eq₂')
  ≅trans (eq₁ →̂ eq₂) (eq₁' →̂ eq₂') = (≅trans eq₁' eq₁) →̂ (≅trans eq₂ eq₂')
  ≅trans (▸̂ eq) (▸̂ eq') = ▸̂ (≅trans∞ eq eq')

  ≅trans∞ : ∀{a∞ b∞ c∞} → a∞ ∞≅ b∞ → b∞ ∞≅ c∞ → a∞ ∞≅ c∞
  ≅force (≅trans∞ eq eq') = ≅trans (≅force eq) (≅force eq')

-- Fill a 2-dimensional cube.

≅fill : ∀ {a a' b b'} (a≅b : a ≅ b) (a≅a' : a ≅ a') (a'≅b' : a' ≅ b') → b ≅ b'
≅fill a≅b a≅a' a'≅b' = ≅trans (≅sym a≅b) (≅trans a≅a' a'≅b')

postulate
  ≅-to-≡ : ∀ {a b} → a ≅ b → a ≡ b