Martin Escardo, July 2026.
Church-Rosser modulo an equivalence relation _≈_.
We consider an abstract reduction relation _▷_ and an equivalence
relation _≈_ on the same type, where two reducts of a common source may
agree only up to _≈_ rather than up to the identity type. Ordinary
confluence then fails, and what holds is confluence modulo _≈_.
For instance, when a ≈ b but a ≠ b, the peak
[(₀,a),(₁,b),(₀,b)] ▷ [(₀,b)] and ▷ [(₀,a)]
has two reducts that are ≈-related but not identical. We derive the
Church-Rosser property modulo _≈_ from two local hypotheses,
* local confluence modulo _≈_, in the form of a one-step diamond, and
* coherence of _≈_ with reduction, written ▷-respects-≈,
with no termination assumption, following the argument of
Relations.ChurchRosser. The reduction and the relation are abstract, so
nothing here is specific to groups.
\begin{code}
{-# OPTIONS --safe --without-K #-}
open import MLTT.Spartan
module EGroups.ChurchRosserModulo
{𝓤 𝓥 : Universe}
{X : 𝓤 ̇ }
(_▷_ : X → X → 𝓤 ̇ )
(_≈_ : X → X → 𝓥 ̇ )
(≈r : reflexive _≈_)
(≈s : symmetric _≈_)
(≈t : transitive _≈_)
where
open import Relations.SRTclosure
\end{code}
The reflexive-transitive closure of _▷_ gives reduction, and its
symmetric-reflexive-transitive closure gives convertibility. Notice that
_≈_ is not added to the closure. Convertibility is then generated by
_▷_ alone, and so lives in the universe 𝓤 of the reduction,
independently of the universe 𝓥 of _≈_.
\begin{code}
_▷⋆_ : X → X → 𝓤 ̇
_▷⋆_ = rt-closure _▷_
_∿_ : X → X → 𝓤 ̇
_∿_ = srt-closure _▷_
\end{code}
We abbreviate the "reducts up to _≈_" conclusion.
\begin{code}
_≋_ : X → X → 𝓤 ⊔ 𝓥 ̇
x ≋ y = Σ z₀ ꞉ X , Σ z₁ ꞉ X , (x ▷⋆ z₀) × (y ▷⋆ z₁) × (z₀ ≈ z₁)
does-not-reduce : X → 𝓤 ̇
does-not-reduce x = (z : X) → ¬ (x ▷ z)
▷⋆-from-irreducible : (x y : X) → does-not-reduce x → x ▷⋆ y → x ＝ y
▷⋆-from-irreducible x x nx (0 , refl) = refl
▷⋆-from-irreducible x y nx (succ m , z , d , i) = 𝟘-elim (nx z d)
\end{code}
We now state the two local hypotheses.
\begin{code}
module _
(Church-Rosser≈
: (x y₀ y₁ : X)
→ x ▷ y₀
→ x ▷ y₁
→ (y₀ ≈ y₁)
+ (Σ z₀ ꞉ X , Σ z₁ ꞉ X , (y₀ ▷ z₀) × (y₁ ▷ z₁) × (z₀ ≈ z₁)))
(▷-respects-≈
: (x x' y : X)
→ x ≈ x'
→ x ▷ y
→ Σ y' ꞉ X , (x' ▷ y') × (y ≈ y'))
where
\end{code}
Coherence lifts from single steps to reduction sequences. If x ≈ x'
and x reduces to y, then x' reduces to some y' with y ≈ y'.
\begin{code}
▷-respects-≈⋆ : (x x' y : X)
→ x ≈ x'
→ x ▷⋆ y
→ Σ y' ꞉ X , (x' ▷⋆ y') × (y ≈ y')
▷-respects-≈⋆ x x' y e (m , i) = f m x x' y e i
where
f : (m : ℕ) (x x' y : X)
→ x ≈ x'
→ iteration _▷_ m x y
→ Σ y' ꞉ X , (x' ▷⋆ y') × (y ≈ y')
f 0 x x' x e refl = x' , rt-reflexive _▷_ x' , e
f (succ m) x x' y e (z , d , i) = γ (▷-respects-≈ x x' z e d)
where
γ : (Σ z' ꞉ X , (x' ▷ z') × (z ≈ z')) → Σ y' ꞉ X , (x' ▷⋆ y') × (y ≈ y')
γ (z' , d' , ez) = δ (f m z z' y ez i)
where
δ : (Σ y' ꞉ X , (z' ▷⋆ y') × (y ≈ y')) → Σ y' ꞉ X , (x' ▷⋆ y') × (y ≈ y')
δ (y' , r , ey) =
y' ,
rt-transitive _▷_ x' z' y' (rt-extension _▷_ x' z' d') r ,
ey
\end{code}
The strip lemma modulo _≈_ says that a single reduction step and a
reduction sequence from a common source have reducts that agree
up to _≈_.
\begin{code}
Church-Rosser⋆-modulo : (x y₀ y₁ : X) → x ▷ y₀ → x ▷⋆ y₁ → y₀ ≋ y₁
Church-Rosser⋆-modulo x y₀ y₁ b (m , i) = f m x y₀ y₁ b i
where
f : (m : ℕ) (x y₀ y₁ : X) → x ▷ y₀ → iteration _▷_ m x y₁ → y₀ ≋ y₁
f 0 x y₀ x b refl = y₀ , y₀ ,
rt-reflexive _▷_ y₀ ,
rt-extension _▷_ x y₀ b ,
≈r y₀
f (succ m) x y₀ y₁ b (w , d , i) = γ (Church-Rosser≈ x y₀ w b d)
where
γ : (y₀ ≈ w)
+ (Σ z₀ ꞉ X , Σ z₁ ꞉ X , (y₀ ▷ z₀) × (w ▷ z₁) × (z₀ ≈ z₁))
→ y₀ ≋ y₁
γ (inl e) = δ (▷-respects-≈⋆ w y₀ y₁ (≈s y₀ w e) (m , i))
where
δ : (Σ y' ꞉ X , (y₀ ▷⋆ y') × (y₁ ≈ y')) → y₀ ≋ y₁
δ (y' , r , ey) = y' , y₁ , r , rt-reflexive _▷_ y₁ , ≈s y₁ y' ey
γ (inr (z₀ , z₁ , d₀ , d₁ , e)) = δ (f m w z₁ y₁ d₁ i)
where
δ : z₁ ≋ y₁ → y₀ ≋ y₁
δ (c₀ , c₁ , r₁ , r₂ , ec) = ε (▷-respects-≈⋆ z₁ z₀ c₀ (≈s z₀ z₁ e) r₁)
where
ε : (Σ d ꞉ X , (z₀ ▷⋆ d) × (c₀ ≈ d)) → y₀ ≋ y₁
ε (d , r₃ , ed) =
d ,
c₁ ,
rt-transitive _▷_ y₀ z₀ d (rt-extension _▷_ y₀ z₀ d₀) r₃ ,
r₂ ,
≈t d c₀ c₁ (≈s c₀ d ed) ec
\end{code}
Church-Rosser modulo _≈_ says that convertible points have reducts that
agree up to _≈_. This is the setoid counterpart of from-∿.
\begin{code}
Church-Rosser-modulo : (x y : X) → x ∿ y → x ≋ y
Church-Rosser-modulo x y (m , e) = f m x y e
where
f : (m : ℕ) (x y : X) → iteration (s-closure _▷_) m x y → x ≋ y
f 0 x x refl = x , x ,
rt-reflexive _▷_ x , rt-reflexive _▷_ x , ≈r x
f (succ m) x y (z , st , i) = γ st (f m z y i)
where
γ : s-closure _▷_ x z → z ≋ y → x ≋ y
γ (inl d) (t₀ , t₁ , zt₀ , yt₁ , et) =
t₀ , t₁ , rt-transitive _▷_ x z t₀ (rt-extension _▷_ x z d) zt₀ , yt₁ , et
γ (inr d) (t₀ , t₁ , zt₀ , yt₁ , et) =
δ (Church-Rosser⋆-modulo z x t₀ d zt₀)
where
δ : x ≋ t₀ → x ≋ y
δ (a₀ , a₁ , xa₀ , t₀a₁ , ea) = ε (▷-respects-≈⋆ t₀ t₁ a₁ et t₀a₁)
where
ε : (Σ c ꞉ X , (t₁ ▷⋆ c) × (a₁ ≈ c)) → x ≋ y
ε (c , t₁c , eac) = a₀ , c ,
xa₀ ,
rt-transitive _▷_ y t₁ c yt₁ t₁c ,
≈t a₀ a₁ c ea eac
\end{code}
We derive the consequence that we will need later. If two
▷-irreducible points are convertible, they are already ≈-related. This
is the setoid replacement for the fact that convertible normal forms
are equal.
\begin{code}
irreducibles-related-by-∿-are-≈ : (x y : X)
→ does-not-reduce x
→ does-not-reduce y
→ x ∿ y
→ x ≈ y
irreducibles-related-by-∿-are-≈ x y nx ny e = γ (Church-Rosser-modulo x y e)
where
γ : x ≋ y → x ≈ y
γ (z₀ , z₁ , r₀ , r₁ , ez) =
transport (x ≈_) (▷⋆-from-irreducible y z₁ ny r₁ ⁻¹)
(transport (_≈ z₁) (▷⋆-from-irreducible x z₀ nx r₀ ⁻¹) ez)
\end{code}