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

--------------------------------------------------
-- direct proof that bisimulation is transitive --
--------------------------------------------------

open import dtt
open import equality
open import Bisimulation


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

private
  module transitive (R₁ : Pow (states w)) (coalg₁ : R₁ ⊂ Φ w R₁)
                    (R₂ : Pow (states w)) (coalg₂ : R₂ ⊂ Φ w R₂) where

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

    R : Pow (states w)
    R (i , (T₁ , T₃)) = Σ (ν w i) (λ T₂ → R₁ ((i , (T₁ , T₂))) × R₂ (i , (T₂ , T₃)))

    private
     lemma :
      {i : I}
      (a₁ : A i) (f₁ : (d₁ : D i a₁) → ν w (n a₁ d₁))
      (a₂ : A i) (f₂ : (d₂ : D i a₂) → ν w (n a₂ d₂))
      (a₃ : A i) (f₃ : (d₃ : D i a₃) → ν w (n a₃ d₃))
      (eq₁₂ : a₁ ≡ a₂)
      (eq₂₃ : a₂ ≡ a₃)
      (d₁ : D i a₁) →
      let eq₁₃ : a₁ ≡ a₃
          eq₁₃ = trans eq₁₂ eq₂₃ in
      let ni₁ = n a₁ d₁ in
      let nT₁ : ν w ni₁
          nT₁ = f₁ d₁ in
      let d₂ : D i a₂
          d₂ = transport-d w eq₁₂ d₁ in
      let ni₂ = n a₂ d₂ in
      let nT₂ : ν w ni₂
          nT₂ = f₂ d₂ in
      let eqₙ₁ : ni₁ ≡ ni₂
          eqₙ₁ = transport-n w eq₁₂ d₁ in
      let nT₂' : ν w ni₁
          nT₂' = transport (ν w) (sym eqₙ₁) (f₂ d₂) in
      (nr₁ : R₁ (ni₁ , (nT₁ , nT₂'))) →

      let d₃ : D i a₃
          d₃ = transport-d w eq₂₃ d₂ in
      let ni₃ = n a₃ d₃ in
      let eqₙ₂ : ni₂ ≡ ni₃
          eqₙ₂ = transport-n w eq₂₃ d₂ in
      let nT₃' : ν w ni₂
          nT₃' = transport (ν w) (sym eqₙ₂) (f₃ d₃) in
      (nr₂ : R₂ (ni₂ , (nT₂ , nT₃'))) →

      let nT₃'' : ν w ni₁
          nT₃'' = transport (ν w)
                   (sym
                    (transport-n w eq₁₃ d₁))
                   (f₃
                    (transport-d w eq₁₃ d₁)) in

      R₂ (ni₁ , (nT₂' , nT₃''))
    lemma a₁ f₁ a₂ f₂ a₃ f₃ refl refl d₁ nr₁  nr₂ = nr₂

    coalg : R ⊂ Φ w R
    coalg {(i , (T₁ , T₃))} (T₂ , (r₁ , r₂)) =
      let a₁ = fst (νElim T₁) in
      let f₁ = snd (νElim T₁) in
      let a₂ = fst (νElim T₂) in
      let f₂ = snd (νElim T₂) in
      let a₃ = fst (νElim T₃) in
      let f₃ = snd (νElim T₃) in
      let eq₁₂ : a₁ ≡ a₂
          eq₁₂ = fst (coalg₁ r₁) in
      let eq₂₃ : a₂ ≡ a₃
          eq₂₃ = fst (coalg₂ r₂) in
      let eq₁₃ : a₁ ≡ a₃
          eq₁₃ = trans eq₁₂ eq₂₃ in
      eq₁₃ , λ (d₁ : D i a₁) →
      let ni₁ = n a₁ d₁ in
      let nT₁ : ν w ni₁
          nT₁ = f₁ d₁ in
      let d₂ : D i a₂
          d₂ = transport-d w eq₁₂ d₁ in
      let ni₂ = n a₂ d₂ in
      let nT₂ : ν w ni₂
          nT₂ = f₂ d₂ in
      let eqₙ₁ : ni₁ ≡ ni₂
          eqₙ₁ = transport-n w eq₁₂ d₁ in
      let nT₂' : ν w ni₁
          nT₂' = transport (ν w) (sym eqₙ₁) (f₂ d₂) in
      let nr₁ : R₁ (ni₁ , (nT₁ , nT₂'))
          nr₁ = snd (coalg₁ r₁) d₁ in

      let d₃ : D i a₃
          d₃ = transport-d w eq₂₃ d₂ in
      let ni₃ = n a₃ d₃ in
      let eqₙ₂ : ni₂ ≡ ni₃
          eqₙ₂ = transport-n w eq₂₃ d₂ in
      let nT₃' : ν w ni₂
          nT₃' = transport (ν w) (sym eqₙ₂) (f₃ d₃) in
      let nr₂ : R₂ (ni₂ , (nT₂ , nT₃'))
          nr₂ = snd (coalg₂ r₂) d₂ in

      let nT₃'' : ν w ni₁
          nT₃'' = transport (ν w)
                   (sym
                    (transport-n w eq₁₃ d₁))
                   (f₃
                    (transport-d w eq₁₃ d₁)) in

      let nr₂' : R₂ (ni₁ , (nT₂' , nT₃''))
          nr₂' =  lemma a₁ f₁ a₂ f₂ a₃ f₃ eq₁₂ eq₂₃ d₁ nr₁  nr₂ in
      nT₂' , nr₁ , nr₂'


----------------------------------------
-- proof that bisimilarity is reflexive:
transitivity : {i : I} {T₁ T₂ T₃ : ν w i} → T₁ ≈ T₂ → T₂ ≈ T₃ → T₁ ≈ T₃
transitivity {i} {T₁} {T₂} B₁ B₂ =
  let open Bisimilar B₁ renaming (carrier to R₁ ; coalg to coalg₁ ; init to r₁) in
  let open Bisimilar B₂ renaming (carrier to R₂ ; coalg to coalg₂ ; init to r₂) in
  record {
    carrier = transitive.R R₁ coalg₁ R₂ coalg₂ ;
    coalg = transitive.coalg R₁ coalg₁ R₂ coalg₂ ;
    init = T₂ , (r₁ , r₂) }