{-# 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