Delay.agda

module wip.Delay where
open import 1Lab.Prelude
open import Data.Sum
open import Data.Nat

private variable
  ℓ : Level
  A B : Type ℓ

record Delay {ℓ} (A : Type ℓ) : Type ℓ where
  coinductive
  field force : A ⊎ Delay A

open Delay

mutual
  record Code {ℓ} {A : Type ℓ} (a b : Delay A) : Type ℓ where
    coinductive
    field force' : Code' (a .force) (b .force)

  data Code' {ℓ} {A : Type ℓ} : (a b : A ⊎ Delay A) → Type ℓ where
    inl' : ∀ {a b} → a ≡ b → Code' (inl a) (inl b)
    inr' : ∀ {a b} → Code a b → Code' (inr a) (inr b)

open Code

Code-is-prop : is-set A → ∀ (a b : Delay A) → is-prop (Code a b)
Code-is-prop h a b p q i .force' with a .force | b .force | p .force' | q .force'
... | inl a' | inl b' | inl' p' | inl' q' = inl' (h a' b' p' q' i)
... | inr a' | inr b' | inr' p' | inr' q' = inr' (Code-is-prop h a' b' p' q' i)

encode : {a b : Delay A} → a ≡ b → Code a b
encode {a = a} {b = b} p .force' with a .force | b .force | ap force p
... | inl _ | inl _ | p' = inl' (inl-inj p')
... | inr _ | inr _ | p' = inr' (encode (inr-inj p'))
... | inl _ | inr _ | p' = absurd (⊎-disjoint p')
... | inr _ | inl _ | p' = absurd (⊎-disjoint (sym p'))

decode : {a b : Delay A} → Code a b → a ≡ b
decode {a = a} {b = b} c i .force with a .force | b .force | c .force'
... | inl _ | inl _ | inl' x = inl (x i)
... | inr _ | inr _ | inr' x = inr (decode x i)

decode-encode : {a b : Delay A} (p : a ≡ b) → decode (encode p) ≡ p
decode-encode {a = a} {b = b} p i j .force with a .force | b .force | ap force p
... | inl x | inl x₁ | p' = ⊎Path.decode-encode p' i j
... | inr x | inr x₁ | p' = {!(ap (ap inr) (decode-encode (inr-inj p')) ∙ ⊎Path.decode-encode p') i j!}
... | inl _ | inr _ | p' = {! absurd (⊎-disjoint p') i j !}
... | inr _ | inl _ | p' = {!   !}

Delay-is-set : is-set A → is-set (Delay A)
Delay-is-set h a b p q = sym (decode-encode p) ∙ ap decode (Code-is-prop h a b (encode p) (encode q)) ∙ decode-encode q