------------------------------------------------------------------------
-- The one-sided Step function, used to define similarity and the
-- two-sided step function
------------------------------------------------------------------------

{-# OPTIONS --without-K #-}

open import Labelled-transition-system

module Similarity.Step
         (lts : LTS)
         (open LTS lts)
         (_[_]↝_ : Proc  Label  Proc  Set)
         where

open import Equality.Propositional
open import Interval using (ext)
open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection equality-with-J as Bijection using (_↔_)
import Equivalence equality-with-J as Eq
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J

open import Indexed-container hiding (⟨_⟩)
open import Relation

private
 module Temporarily-private where

  -- If _[_]↝_ is instantiated with _[_]⟶_, then this is basically the
  -- function s from Section 6.3.4.2 in Pous and Sangiorgi's
  -- "Enhancements of the bisimulation proof method", except that
  -- clause (3) is omitted.
  --
  -- Similarly, if _[_]↝_ is instantiated with _[_]⇒̂_, then this is
  -- basically the function w from Section 6.5.2.4, except that
  -- "P R Q" is omitted.

  record Step {r} (R : Rel₂ r Proc) (pq : Proc × Proc) : Set r where
    constructor ⟨_⟩

    private
      p = proj₁ pq
      q = proj₂ pq

    field
      challenge :  {p′ μ} 
                  p [ μ ]⟶ p′   λ q′  q [ μ ]↝ q′ × R (p′ , q′)

open Temporarily-private using (Step)

-- Used to aid type inference. Note that this type is parametrised
-- (see the module telescope above). The inclusion of a value of this
-- type in the definition of S̲t̲e̲p̲ below makes it easier for Agda to
-- infer the LTS parameter from the types ν S̲t̲e̲p̲ i (p , q) and
-- ν′ S̲t̲e̲p̲ i (p , q).

record Magic : Set where

-- The Magic type is isomorphic to the unit type.

Magic↔⊤ : Magic  
Magic↔⊤ = record
  { surjection = record
    { right-inverse-of = λ _  refl
    }
  ; left-inverse-of = λ _  refl
  }

-- The Step function, expressed as an indexed container.

S̲t̲e̲p̲ : Container (Proc × Proc) (Proc × Proc)
S̲t̲e̲p̲ =
   { (p , q)  Magic  -- Included in order to aid type inference.
                   ×
                 (∀ {p′ μ}  p [ μ ]⟶ p′   λ q′  q [ μ ]↝ q′)
     })
    
   { {o = p , q} (_ , lr) (p′ , q′) 
        λ μ   λ (p⟶p′ : p [ μ ]⟶ p′)  proj₁ (lr p⟶p′)  q′
       })

-- The definition of Step in terms of a container is pointwise
-- isomorphic to the direct definition.

Step↔S̲t̲e̲p̲ :
   {r} {R : Rel₂ r Proc} {pq}  Step R pq   S̲t̲e̲p̲  R pq
Step↔S̲t̲e̲p̲ {R = R} {pq} = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ s  to₁ s , to₂ s
      ; from = from
      }
    ; right-inverse-of = λ where
        (_ , f) 
          Σ-≡,≡→≡ refl $
            implicit-extensionality ext λ _  ext (to₂∘from f)
    }
  ; left-inverse-of = λ _  refl
  }
  where
  to₁ : Step R pq  Container.Shape S̲t̲e̲p̲ pq
  to₁ Step.⟨ lr  =
      _
    ,  p⟶p′  Σ-map id proj₁ (lr p⟶p′))

  to₂ :
    (s : Step R pq) 
    Container.Position S̲t̲e̲p̲ (to₁ s)  R
  to₂ Step.⟨ lr  (_ , p⟶p′ , refl) = proj₂ (proj₂ (lr p⟶p′))

  from :  S̲t̲e̲p̲  R pq  Step R pq
  from ((_ , lr) , f) =
    Step.⟨  p⟶p′ 
              let q′ , q⟶q′ = lr p⟶p′
              in  q′ , q⟶q′ , f (_ , p⟶p′ , refl))
         

  to₂∘from :
     {p′q′} {s : Container.Shape S̲t̲e̲p̲ pq}
    (f : Container.Position S̲t̲e̲p̲ s  R) 
    (pos : Container.Position S̲t̲e̲p̲ s p′q′) 
    to₂ (from (s , f)) pos  f pos
  to₂∘from f (_ , _ , refl) = refl

module S̲t̲e̲p̲ {r} {R : Rel₂ r Proc} {p q} where

  -- A "constructor".

  ⟨_⟩ :
    (∀ {p′ μ}  p [ μ ]⟶ p′   λ q′  q [ μ ]↝ q′ × R (p′ , q′)) 
     S̲t̲e̲p̲  R (p , q)
   lr  = _↔_.to Step↔S̲t̲e̲p̲ Step.⟨ lr 

  -- A "projection".

  challenge :
     S̲t̲e̲p̲  R (p , q) 
     {p′ μ}  p [ μ ]⟶ p′   λ q′  q [ μ ]↝ q′ × R (p′ , q′)
  challenge = Step.challenge  _↔_.from Step↔S̲t̲e̲p̲

open Temporarily-private public

-- An unfolding lemma for ⟦ S̲t̲e̲p̲ ⟧₂.

⟦S̲t̲e̲p̲⟧₂↔ :
   {x} {X : Rel₂ x Proc}
  (R :  {o}  Rel₂ (# 0) (X o)) 
   {p q} (p∼q₁ p∼q₂ :  S̲t̲e̲p̲  X (p , q)) 

   S̲t̲e̲p̲ ⟧₂ R (p∼q₁ , p∼q₂)

    

  (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) 
   let q′₁ , q⟶q′₁ , p′≤q′₁ = S̲t̲e̲p̲.challenge p∼q₁ p⟶p′
       q′₂ , q⟶q′₂ , p′≤q′₂ = S̲t̲e̲p̲.challenge p∼q₂ p⟶p′
   in  λ (q′₁≡q′₂ : q′₁  q′₂) 
        subst (q [ μ ]↝_) q′₁≡q′₂ q⟶q′₁  q⟶q′₂
          ×
        R (subst (X  (p′ ,_)) q′₁≡q′₂ p′≤q′₁ , p′≤q′₂))

⟦S̲t̲e̲p̲⟧₂↔ {X = X} R {p} {q}
                   (s₁@(_ , ch₁) , f₁) (s₂@(_ , ch₂) , f₂) =

  ( λ (eq : s₁  s₂) 
    {o} (p : Container.Position S̲t̲e̲p̲ s₁ o) 
   R (f₁ p , f₂ (subst  s  Container.Position S̲t̲e̲p̲ s o) eq p)))     ↝⟨ inverse $ Σ-cong ≡×≡↔≡  _  F.id) 

  ( λ (eq : proj₁ s₁  proj₁ s₂ ×  {_ _}  ch₁)  ch₂) 
    {o} (p : Container.Position S̲t̲e̲p̲ s₁ o) 
   R (f₁ p , f₂ (subst  s  Container.Position S̲t̲e̲p̲ s o)
                       (cong₂ _,_ (proj₁ eq) (proj₂ eq)) p)))          ↝⟨ inverse Σ-assoc 

  ( λ (eq₁ : proj₁ s₁  proj₁ s₂) 
    λ (eq₂ :  {_ _}  ch₁)  ch₂) 
    {o} (p : Container.Position S̲t̲e̲p̲ s₁ o) 
   R (f₁ p , f₂ (subst  s  Container.Position S̲t̲e̲p̲ s o)
                       (cong₂ _,_ eq₁ eq₂) p)))                        ↝⟨ drop-⊤-left-Σ (_⇔_.to contractible⇔↔⊤ $
                                                                          mono₁ 0 (_⇔_.from contractible⇔↔⊤ Magic↔⊤) _ _) 
  ( λ (eq :  {_ _}  ch₁)  ch₂) 
    {o} (p : Container.Position S̲t̲e̲p̲ s₁ o) 
   R (f₁ p , f₂ (subst  s  Container.Position S̲t̲e̲p̲ s o)
                       (cong₂ _,_ refl eq) p)))                        ↝⟨ (∃-cong λ eq  implicit-∀-cong ext $ ∀-cong ext λ _ 
                                                                           ≡⇒↝ _ $
                                                                           cong  (eq : s₁  s₂) 
                                                                                   R (f₁ _ , f₂ (subst  s  Container.Position S̲t̲e̲p̲ s _) eq _))) $
                                                                           trans-reflˡ (cong (_ ,_) eq)) 
  ( λ (eq :  {_ _}  ch₁)  ch₂) 
    {o} (p : Container.Position S̲t̲e̲p̲ s₁ o) 
   R (f₁ p , f₂ (subst  s  Container.Position S̲t̲e̲p̲ s o)
                       (cong (_ ,_) eq) p)))                           ↝⟨ (∃-cong λ eq  implicit-∀-cong ext λ {o}  ∀-cong ext λ p 
                                                                           ≡⇒↝ _ $ cong  p  R {o = o} (f₁ _ , f₂ p)) $ sym $
                                                                           subst-∘  (s : Container.Shape S̲t̲e̲p̲ _)  Container.Position S̲t̲e̲p̲ s o)
                                                                                   _ eq) 
  ( λ (eq :  {_ _}  ch₁)  ch₂) 
    {o} (p : Container.Position S̲t̲e̲p̲ s₁ o) 
   R (f₁ p , f₂ (subst  (ch :  {_ _}  _) 
                          Container.Position S̲t̲e̲p̲ (_ , ch) o)
                       eq p)))                                         ↔⟨⟩

  ( λ (eq : _≡_ {A =  {p′ μ}  _} ch₁ ch₂) 
    {p′q′} 
   (pos :  λ μ   λ (p⟶p′ : p [ μ ]⟶ proj₁ p′q′) 
          proj₁ (ch₁ p⟶p′)  proj₂ p′q′) 
   R (f₁ pos ,
      f₂ (subst  ch   λ μ   λ (p⟶p′ : p [ μ ]⟶ proj₁ p′q′) 
                        proj₁ (ch p⟶p′)  proj₂ p′q′)
                eq pos)))                                              ↝⟨ (∃-cong λ _  Bijection.implicit-Π↔Π) 

  ( λ (eq : _≡_ {A =  {p′ μ}  _} ch₁ ch₂) 
    p′q′ 
   (pos :  λ μ   λ (p⟶p′ : p [ μ ]⟶ proj₁ p′q′) 
          proj₁ (ch₁ p⟶p′)  proj₂ p′q′) 
   R (f₁ pos ,
      f₂ (subst  ch   λ μ   λ (p⟶p′ : p [ μ ]⟶ proj₁ p′q′) 
                        proj₁ (ch p⟶p′)  proj₂ p′q′)
                eq pos)))                                              ↝⟨ (∃-cong λ _  currying) 

  ( λ (eq : _≡_ {A =  {p′ μ}  _} ch₁ ch₂) 
    p′ q′ 
   (pos :  λ μ   λ (p⟶p′ : p [ μ ]⟶ p′)  proj₁ (ch₁ p⟶p′)  q′) 
   R (f₁ pos ,
      f₂ (subst  ch   λ μ   λ (p⟶p′ : p [ μ ]⟶ p′) 
                        proj₁ (ch p⟶p′)  q′)
                eq pos)))                                              ↝⟨ (∃-cong λ _  ∀-cong ext λ _  ∀-cong ext λ _  currying) 

  ( λ (eq : _≡_ {A =  {p′ μ}  _} ch₁ ch₂) 
    p′ q′ μ 
   (pos :  λ (p⟶p′ : p [ μ ]⟶ p′)  proj₁ (ch₁ p⟶p′)  q′) 
   R (f₁ (μ , pos) ,
      f₂ (subst  ch   λ μ   λ (p⟶p′ : p [ μ ]⟶ p′) 
                        proj₁ (ch p⟶p′)  q′)
                eq (μ , pos))))                                        ↝⟨ (∃-cong λ _  ∀-cong ext λ _  ∀-cong ext λ _  ∀-cong ext λ _ 
                                                                           currying) 
  ( λ (eq : _≡_ {A =  {p′ μ}  _} ch₁ ch₂) 
    p′ q′ μ (p⟶p′ : p [ μ ]⟶ p′) (≡q′ : proj₁ (ch₁ p⟶p′)  q′) 
   R (f₁ (μ , p⟶p′ , ≡q′) ,
      f₂ (subst  ch   λ μ   λ (p⟶p′ : p [ μ ]⟶ p′) 
                        proj₁ (ch p⟶p′)  q′)
                eq (μ , p⟶p′ , ≡q′))))                                 ↝⟨ (∃-cong λ _  ∀-cong ext λ _  Π-comm) 

  ( λ (eq : _≡_ {A =  {p′ μ}  _} ch₁ ch₂) 
    p′ μ q′ (p⟶p′ : p [ μ ]⟶ p′) (≡q′ : proj₁ (ch₁ p⟶p′)  q′) 
   R (f₁ (μ , p⟶p′ , ≡q′) ,
      f₂ (subst  ch   λ μ   λ (p⟶p′ : p [ μ ]⟶ p′) 
                        proj₁ (ch p⟶p′)  q′)
                eq (μ , p⟶p′ , ≡q′))))                                 ↝⟨ (∃-cong λ _  ∀-cong ext λ _  ∀-cong ext λ _  Π-comm) 

  ( λ (eq : _≡_ {A =  {p′ μ}  _} ch₁ ch₂) 
    p′ μ (p⟶p′ : p [ μ ]⟶ p′) q′ (≡q′ : proj₁ (ch₁ p⟶p′)  q′) 
   R (f₁ (μ , p⟶p′ , ≡q′) ,
      f₂ (subst  ch   λ μ   λ (p⟶p′ : p [ μ ]⟶ p′) 
                        proj₁ (ch p⟶p′)  q′)
                eq (μ , p⟶p′ , ≡q′))))                                 ↝⟨ (∃-cong λ _  ∀-cong ext λ _  ∀-cong ext λ _  ∀-cong ext λ _ 
                                                                              inverse $ ∀-intro ext _) 
  ( λ (eq : _≡_ {A =  {p′ μ}  _} ch₁ ch₂) 
    p′ μ (p⟶p′ : p [ μ ]⟶ p′) 
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (subst  ch   λ μ   λ (p⟶p′′ : p [ μ ]⟶ p′) 
                        proj₁ (ch p⟶p′′)  proj₁ (ch₁ p⟶p′))
                eq (μ , p⟶p′ , refl))))                                ↝⟨ (∃-cong λ eq  ∀-cong ext λ _  ∀-cong ext λ _  ∀-cong ext λ _ 
                                                                           ≡⇒↝ _ $ cong (R  (f₁ _ ,_)  f₂) $ lemma₁ eq) 
  ( λ (eq : _≡_ {A =  {p′ μ}  _} ch₁ ch₂) 
    p′ μ (p⟶p′ : p [ μ ]⟶ p′) 
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (μ , p⟶p′ , sym (cong  ch  proj₁ (ch p⟶p′)) eq))))         ↝⟨ (∃-cong λ eq  ∀-cong ext λ _  inverse Bijection.implicit-Π↔Π) 

  ( λ (eq : _≡_ {A =  {p′ μ}  _} ch₁ ch₂) 
    p′ {μ} (p⟶p′ : p [ μ ]⟶ p′) 
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (μ , p⟶p′ , sym (cong  ch  proj₁ (ch p⟶p′)) eq))))         ↝⟨ (∃-cong λ eq  inverse Bijection.implicit-Π↔Π) 

  ( λ (eq : _≡_ {A =  {p′ μ}  _} ch₁ ch₂) 
    {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) 
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (μ , p⟶p′ , sym (cong  ch  proj₁ (ch p⟶p′)) eq))))         ↝⟨ (Σ-cong (inverse $ implicit-extensionality-isomorphism
                                                                                               {k = bijection} ext) λ eq 
                                                                           implicit-∀-cong ext $ implicit-∀-cong ext $ ∀-cong ext λ p⟶p′ 
                                                                           ≡⇒↝ _ $ sym $ cong  eq 
                                                                             R (f₁ _ , f₂ (_ , p⟶p′ , sym (cong  ch  proj₁ (ch p⟶p′)) eq)))) $
                                                                           _↔_.right-inverse-of (implicit-extensionality-isomorphism ext) eq) 
  ( λ (eq :  p′   {μ}  ch₁ {p′ = p′} {μ = μ})  ch₂) 
   let eq′ = _↔_.to (implicit-extensionality-isomorphism ext) eq in
    {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) 
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (μ , p⟶p′ , sym (cong  ch  proj₁ (ch p⟶p′)) eq′))))        ↝⟨ (∃-cong λ eq 
                                                                           implicit-∀-cong ext $ implicit-∀-cong ext $ ∀-cong ext λ p⟶p′ 
                                                                           ≡⇒↝ _ $ cong  eq  R (f₁ _ , f₂ (_ , p⟶p′ , sym eq))) $
                                                                           lemma₂ eq) 
  ( λ (eq :  p′   {μ}  ch₁ {p′ = p′} {μ = μ})  ch₂) 
    {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) 
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (μ , p⟶p′ , sym (cong  ch  proj₁ (ch p′ p⟶p′))
                               (Eq.good-ext ext eq)))))                ↝⟨ (Σ-cong (inverse $ ∀-cong ext λ _ 
                                                                                   implicit-extensionality-isomorphism
                                                                                     {k = bijection} ext) λ eq 
                                                                           implicit-∀-cong ext $ implicit-∀-cong ext $ ∀-cong ext λ p⟶p′ 
                                                                           ≡⇒↝ _ $ sym $ cong  eq 
                                                                             R (f₁ _ , f₂ (_ , p⟶p′ , sym (cong  ch  proj₁ (ch _ p⟶p′))
                                                                                                                (Eq.good-ext ext eq))))) $
                                                                           ext (_↔_.right-inverse-of
                                                                                  (implicit-extensionality-isomorphism ext)  eq)) 
  ( λ (eq :  p′ μ  ch₁ {p′ = p′} {μ = μ}  ch₂) 
   let eq′ = implicit-extensionality (Eq.good-ext ext)  eq in
    {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) 
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (μ , p⟶p′ , sym (cong  ch  proj₁ (ch p′ p⟶p′))
                               (Eq.good-ext ext eq′)))))               ↝⟨ (∃-cong λ _ 
                                                                           implicit-∀-cong ext $ implicit-∀-cong ext $ ∀-cong ext λ _ 
                                                                           ≡⇒↝ _ $ cong  eq  R (f₁ _ , f₂ (_ , _ , sym eq))) $
                                                                           lemma₃ _) 
  ( λ (eq :  p′ μ  ch₁ {p′ = p′} {μ = μ}  ch₂) 
    {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) 
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (μ , p⟶p′ , sym (cong  ch  proj₁ (ch p⟶p′)) (eq p′ μ)))))  ↝⟨ Σ-cong (inverse Bijection.implicit-Π↔Π)  _  F.id) 

  ( λ (eq :  {p′} μ  ch₁ {p′ = p′} {μ = μ}  ch₂) 
    {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) 
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (μ , p⟶p′ , sym (cong  ch  proj₁ (ch p⟶p′)) (eq μ)))))     ↝⟨ Σ-cong (implicit-∀-cong ext $ inverse Bijection.implicit-Π↔Π)
                                                                                  _  F.id) 
  ( λ (eq :  {p′ μ}  ch₁ {p′ = p′} {μ = μ}  ch₂) 
    {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) 
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (μ , p⟶p′ , sym (cong  ch  proj₁ (ch p⟶p′)) eq))))         ↝⟨ (∃-cong λ eq 
                                                                           implicit-∀-cong ext $ implicit-∀-cong ext $ ∀-cong ext λ p⟶p′ 
                                                                           ≡⇒↝ _ $ cong  eq  R (f₁ _ , f₂ (_ , _ , sym eq))) $ sym $
                                                                           cong-∘ proj₁ (_$ p⟶p′) (eq {μ = _})) 
  ( λ (eq :  {p′ μ}  ch₁ {p′ = p′} {μ = μ}  ch₂) 
    {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) 
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (μ , p⟶p′ , sym (cong proj₁ $ cong (_$ p⟶p′) eq))))           ↝⟨ Σ-cong (implicit-∀-cong ext $ implicit-∀-cong ext $ inverse $
                                                                                  Eq.extensionality-isomorphism ext)
                                                                                  _  F.id) 
  ( λ (eq :  {p′ μ} (p⟶p′ : p [ μ ]⟶ p′)  ch₁ p⟶p′  ch₂ p⟶p′) 
    {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) 
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (μ , p⟶p′ , sym (cong proj₁ (eq p⟶p′)))))                     ↝⟨ inverse implicit-ΠΣ-comm 

  (∀ {p′} 
    λ (eq :  {μ} (p⟶p′ : p [ μ ]⟶ p′)  ch₁ p⟶p′  ch₂ p⟶p′) 
    {μ} (p⟶p′ : p [ μ ]⟶ p′) 
   R (f₁ (μ , p⟶p′ , refl) ,
      f₂ (μ , p⟶p′ , sym (cong proj₁ (eq p⟶p′)))))                     ↝⟨ implicit-∀-cong ext $ inverse implicit-ΠΣ-comm 

  (∀ {p′ μ} 
    λ (eq : (p⟶p′ : p [ μ ]⟶ p′)  ch₁ p⟶p′  ch₂ p⟶p′) 
    p⟶p′  R (f₁ (μ , p⟶p′ , refl) ,
               f₂ (μ , p⟶p′ , sym (cong proj₁ (eq p⟶p′)))))            ↝⟨ implicit-∀-cong ext $ implicit-∀-cong ext $ inverse ΠΣ-comm 

  (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) 
    λ (eq : ch₁ p⟶p′  ch₂ p⟶p′) 
   R (f₁ (μ , p⟶p′ , refl) , f₂ (μ , p⟶p′ , sym (cong proj₁ eq))))     ↝⟨ (inverse $ implicit-∀-cong ext $ implicit-∀-cong ext $ ∀-cong ext λ _ 
                                                                           Σ-cong Bijection.Σ-≡,≡↔≡ λ _  F.id) 
  (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) 
   let q′₁ , q⟶q′₁ = ch₁ p⟶p′
       q′₂ , q⟶q′₂ = ch₂ p⟶p′
   in  λ (eq :  λ (q′₁≡q′₂ : q′₁  q′₂) 
                  subst (q [ μ ]↝_) q′₁≡q′₂ q⟶q′₁  q⟶q′₂) 
      R (f₁ (μ , p⟶p′ , refl) ,
         f₂ (μ , p⟶p′ , sym (cong proj₁ (uncurry Σ-≡,≡→≡ eq)))))       ↝⟨ (implicit-∀-cong ext $ implicit-∀-cong ext $ ∀-cong ext λ _ 
                                                                           ∃-cong λ eq 
                                                                           ≡⇒↝ _ $ cong  eq  R (f₁ _ , f₂ (_ , _ , sym eq))) $
                                                                           proj₁-Σ-≡,≡→≡ (proj₁ eq) (proj₂ eq)) 
  (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) 
   let q′₁ , q⟶q′₁ = ch₁ p⟶p′
       q′₂ , q⟶q′₂ = ch₂ p⟶p′
   in  λ (eq :  λ (q′₁≡q′₂ : q′₁  q′₂) 
                  subst (q [ μ ]↝_) q′₁≡q′₂ q⟶q′₁  q⟶q′₂) 
      R (f₁ (μ , p⟶p′ , refl) , f₂ (μ , p⟶p′ , sym (proj₁ eq))))       ↝⟨ (implicit-∀-cong ext $ implicit-∀-cong ext $ ∀-cong ext λ _ 
                                                                           inverse Σ-assoc) 
  (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) 
   let q′₁ , q⟶q′₁ = ch₁ p⟶p′
       q′₂ , q⟶q′₂ = ch₂ p⟶p′
   in  λ (q′₁≡q′₂ : q′₁  q′₂) 
        subst (q [ μ ]↝_) q′₁≡q′₂ q⟶q′₁  q⟶q′₂
          ×
        R (f₁ (μ , p⟶p′ , refl) , f₂ (μ , p⟶p′ , sym q′₁≡q′₂)))        ↝⟨ (implicit-∀-cong ext $ implicit-∀-cong ext $ ∀-cong ext λ p⟶p′ 
                                                                           ∃-cong λ q′₁≡q′₂  ∃-cong λ _  ≡⇒↝ _ $
                                                                           lemma₄ q′₁≡q′₂) 
  (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) 
   let q′₁ , q⟶q′₁ = ch₁ p⟶p′
       q′₂ , q⟶q′₂ = ch₂ p⟶p′
   in  λ (q′₁≡q′₂ : q′₁  q′₂) 
        subst (q [ μ ]↝_) q′₁≡q′₂ q⟶q′₁  q⟶q′₂
          ×
        R (subst (X  (p′ ,_)) q′₁≡q′₂ (f₁ (_ , p⟶p′ , refl)) ,
           f₂ (_ , p⟶p′ , refl)))                                      ↔⟨⟩

  (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) 
   let q′₁ , q⟶q′₁ , p′≤q′₁ = S̲t̲e̲p̲.challenge (s₁ , f₁) p⟶p′
       q′₂ , q⟶q′₂ , p′≤q′₂ = S̲t̲e̲p̲.challenge (s₂ , f₂) p⟶p′
   in  λ (q′₁≡q′₂ : q′₁  q′₂) 
        subst (q [ μ ]↝_) q′₁≡q′₂ q⟶q′₁  q⟶q′₂
          ×
        R (subst (X  (p′ ,_)) q′₁≡q′₂ p′≤q′₁ , p′≤q′₂))               

  where

  lemma₁ = λ {p q} {f g :  {p′ μ}  p [ μ ]⟶ p′   (q [ μ ]↝_)}
             (eq :  {p′ μ}  f {p′ = p′} {μ = μ})  g)
             {p′ μ} {p⟶p′ : p [ μ ]⟶ p′} 

    subst  ch 
              λ μ   λ (p⟶p′′ : p [ μ ]⟶ p′) 
             proj₁ (ch p⟶p′′)  proj₁ (f p⟶p′))
          eq (μ , p⟶p′ , refl)                          ≡⟨ push-subst-pair′ {y≡z = eq} _ _ _ 

    ( μ
    , subst₂  { (ch , μ) 
                   λ (p⟶p′′ : p [ μ ]⟶ p′) 
                  proj₁ (ch p⟶p′′)  proj₁ (f p⟶p′) })
             eq (subst-const eq) (p⟶p′ , refl)
    )                                                   ≡⟨ cong (μ ,_) $
                                                           cong  eq  subst  { (ch , μ) 
                                                                                    λ (p⟶p′′ : p [ μ ]⟶ p′) 
                                                                                   proj₁ (ch p⟶p′′)  proj₁ (f p⟶p′) })
                                                                              eq (p⟶p′ , refl)) $
                                                           Σ-≡,≡→≡-subst-const eq refl 
    ( μ
    , subst  { (ch , μ) 
                  λ (p⟶p′′ : p [ μ ]⟶ p′) 
                 proj₁ (ch p⟶p′′)  proj₁ (f p⟶p′) })
            (cong₂ _,_ eq refl) (p⟶p′ , refl)
    )                                                   ≡⟨⟩

    ( μ
    , subst  { (ch , μ) 
                  λ (p⟶p′′ : p [ μ ]⟶ p′) 
                 proj₁ (ch p⟶p′′)  proj₁ (f p⟶p′) })
            (cong (_, _) eq) (p⟶p′ , refl)
    )                                                   ≡⟨ cong (μ ,_) $ sym $
                                                           subst-∘ _ _ eq 
    ( μ
    , subst  ch 
                λ (p⟶p′′ : p [ μ ]⟶ p′) 
               proj₁ (ch p⟶p′′)  proj₁ (f p⟶p′))
            eq (p⟶p′ , refl)
    )                                                   ≡⟨ cong (μ ,_) $
                                                           push-subst-pair′ {y≡z = eq} _ _ _ 
    ( μ
    , p⟶p′
    , subst₂  { (ch , p⟶p′′) 
                  proj₁ (ch p⟶p′′)  proj₁ (f p⟶p′) })
             eq (subst-const eq) refl
    )                                                   ≡⟨ cong  eq  (_ , p⟶p′ , subst  { (ch , p⟶p′′)  proj₁ (ch p⟶p′′)  proj₁ (f p⟶p′) })
                                                                                          eq refl)) $
                                                           Σ-≡,≡→≡-subst-const eq refl 
    ( μ
    , p⟶p′
    , subst  { (ch , p⟶p′′) 
                 proj₁ (ch p⟶p′′)  proj₁ (f p⟶p′) })
            (cong (_, _) eq) refl
    )                                                   ≡⟨ cong  eq  (_ , p⟶p′ , eq)) $ sym $
                                                           subst-∘ _ _ eq 
    ( μ
    , p⟶p′
    , subst  ch  proj₁ (ch p⟶p′)  proj₁ (f p⟶p′))
            eq refl
    )                                                   ≡⟨ cong  eq  (_ , p⟶p′ , eq)) $
                                                           subst-∘ _ _ eq 
    ( μ
    , p⟶p′
    , subst (_≡ proj₁ (f p⟶p′))
            (cong  ch  proj₁ (ch p⟶p′)) eq) refl
    )                                                   ≡⟨ cong  eq  (_ , p⟶p′ , subst (_≡ _) eq refl)) $
                                                           sym $ sym-sym (cong  ch  proj₁ (ch p⟶p′)) eq) 
    ( μ
    , p⟶p′
    , subst (_≡ proj₁ (f p⟶p′))
            (sym $ sym $
               cong  ch  proj₁ (ch p⟶p′)) eq)
            refl
    )                                                   ≡⟨ cong  eq  (_ , p⟶p′ , eq)) $
                                                           subst-trans (sym $ cong  ch  proj₁ (ch p⟶p′)) eq) ⟩∎
    ( μ
    , p⟶p′
    , sym (cong  ch  proj₁ (ch p⟶p′)) eq)
    )                                                   

  lemma₂ = λ {p q} {f g :  {p′ μ}  p [ μ ]⟶ p′   (q [ μ ]↝_)}
             (eq :  p′   {μ}  f {p′ = p′} {μ = μ})  g)
             {p′ μ} {p⟶p′ : p [ μ ]⟶ p′} 

    cong  ch  proj₁ (ch p⟶p′))
         (_↔_.to (implicit-extensionality-isomorphism ext) eq)  ≡⟨⟩

    cong  ch  proj₁ (ch p⟶p′))
         (implicit-extensionality (Eq.good-ext ext) eq)         ≡⟨ cong-∘ _ _ (Eq.good-ext ext eq) ⟩∎

    cong  ch  proj₁ (ch p′ p⟶p′)) (Eq.good-ext ext eq)       

  lemma₃ = λ {p q} {f g :  {p′ μ}  p [ μ ]⟶ p′   (q [ μ ]↝_)}
             (eq :  p′ μ  f {p′ = p′} {μ = μ}  g)
             {p′ μ p⟶p′} 

    cong  (ch :  _ {μ}  _)  proj₁ (ch p′ {μ = μ} p⟶p′))
         (Eq.good-ext ext
            (implicit-extensionality (Eq.good-ext ext)  eq))     ≡⟨⟩

    cong  ch  proj₁ (ch p′ p⟶p′))
         (Eq.good-ext ext
            (cong  f {x}  f x)  (Eq.good-ext ext  eq)))      ≡⟨ cong (cong  ch  proj₁ (ch p′ p⟶p′))) $ sym $
                                                                     Eq.cong-post-∘-good-ext {h = λ f {x}  f x} ext ext (Eq.good-ext ext  eq) 
    cong  ch  proj₁ (ch p′ p⟶p′))
         (cong  f x {y}  f x y)
               (Eq.good-ext ext (Eq.good-ext ext  eq)))          ≡⟨ cong-∘ _ _ (Eq.good-ext ext (Eq.good-ext ext  eq)) 

    cong  ch  proj₁ (ch p′ μ p⟶p′))
         (Eq.good-ext ext (Eq.good-ext ext  eq))                 ≡⟨ sym $ cong-∘ _ _ (Eq.good-ext ext (Eq.good-ext ext  eq)) 

    cong  ch  proj₁ (ch μ p⟶p′))
         (cong (_$ p′) (Eq.good-ext ext (Eq.good-ext ext  eq)))  ≡⟨ cong (cong  ch  proj₁ (ch μ p⟶p′))) $ Eq.cong-good-ext ext _ 

    cong  ch  proj₁ (ch μ p⟶p′)) (Eq.good-ext ext (eq p′))     ≡⟨ sym $ cong-∘ _ _ (Eq.good-ext ext (eq p′)) 

    cong  ch  proj₁ (ch p⟶p′))
         (cong (_$ μ) (Eq.good-ext ext (eq p′)))                  ≡⟨ cong (cong  ch  proj₁ (ch p⟶p′))) $ Eq.cong-good-ext ext _ ⟩∎

    cong  ch  proj₁ (ch p⟶p′)) (eq p′ μ)                       

  lemma₄ :
     {p′ μ} {p⟶p′ : p [ μ ]⟶ p′}
    (q′₁≡q′₂ : proj₁ (ch₁ p⟶p′)  proj₁ (ch₂ p⟶p′)) 
    R (f₁ (μ , p⟶p′ , refl) , f₂ (μ , p⟶p′ , sym q′₁≡q′₂))
      
    R (subst (X  (p′ ,_)) q′₁≡q′₂ (f₁ (_ , p⟶p′ , refl)) ,
       f₂ (_ , p⟶p′ , refl))
  lemma₄ {p′} {μ} {p⟶p′} q′₁≡q′₂ =
    R (f₁ (μ , p⟶p′ , refl) , f₂ (μ , p⟶p′ , sym q′₁≡q′₂))        ≡⟨ cong (R  (f₁ _ ,_)) $ lemma′ q′₁≡q′₂ 

    R (f₁ (μ , p⟶p′ , refl) ,
       subst (X  (p′ ,_)) (sym q′₁≡q′₂) (f₂ (_ , p⟶p′ , refl)))  ≡⟨ lemma″ q′₁≡q′₂ ⟩∎

    R (subst (X  (p′ ,_)) q′₁≡q′₂ (f₁ (_ , p⟶p′ , refl)) ,
       f₂ (_ , p⟶p′ , refl))                                      
    where
    lemma′ :
       {q′₁} (q′₁≡q′₂ : q′₁  proj₁ (ch₂ p⟶p′)) 
      f₂ (μ , p⟶p′ , sym q′₁≡q′₂)
        
      subst (X  (p′ ,_)) (sym q′₁≡q′₂) (f₂ (_ , p⟶p′ , refl))
    lemma′ refl = refl

    lemma″ :
       {q′₂ x} (q′₁≡q′₂ : proj₁ (ch₁ p⟶p′)  q′₂) 
      R (f₁ (μ , p⟶p′ , refl) , subst (X  (p′ ,_)) (sym q′₁≡q′₂) x)
        
      R (subst (X  (p′ ,_)) q′₁≡q′₂ (f₁ (_ , p⟶p′ , refl)) , x)
    lemma″ refl = refl