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

-------------------------------------------------
-- direct proof that bisimulation is reflexive --
-------------------------------------------------

open import dtt
open import equality
open import Bisimulation


module Bisimulation.reflexivity {I : Set} (w : IS I) where


private R : Pow (states w)
R (i , (T₁ , T₂)) = T₁ ≡ T₂


private coalg-refl : R ⊂ Φ w R
coalg-refl {( i , ( T₁ , T₂ ) )} refl =
  ( refl ,  (λ d₁ → refl))


----------------------------------------
-- proof that bisimilarity is reflexive:
reflexivity : {i : I} (T : ν w i) → T ≈ T
reflexivity T₁ =
  record {
         carrier = R ;
         coalg = coalg-refl ;
         init = refl }