{-# OPTIONS --without-K --safe --guardedness --no-sized-types #-}

-------------------------------------------------------------
-- Intensional equality is a linear simulation from w to w --
-------------------------------------------------------------


open import dtt
open import equality
open import Simulations

module Simulations.identity {I : Set} (w : IS I) where

open IS w renaming (Command to A ; Response to D ; next to n)

private coalg : {i₁ i₂ : I} → i₁ ≡ i₂ → Φ w w _≡_ i₁ i₂
coalg {i₁} {i₂} eq =
      J (λ i₁ i₂ eq₁ → Φ w w _≡_ i₁ i₂)
        (λ i → λ a → a , (λ d → d , refl))
        i₁ i₂ eq
-- coalg {i} {.i} refl = λ a → a , (λ d → d , refl)

ID : w ⊸ w
ID = record {
            R = _≡_ ;
            coalg = coalg
            }