ChurchRosserModulo
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.{-# 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.SRTclosureThe 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 _≈_._▷⋆_ : X → X → 𝓤 ̇ _▷⋆_ = rt-closure _▷_ _∿_ : X → X → 𝓤 ̇ _∿_ = srt-closure _▷_We abbreviate the "reducts up to _≈_" conclusion._≋_ : 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)We now state the two local hypotheses.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')) whereCoherence lifts from single steps to reduction sequences. If x ≈ x' and x reduces to y, then x' reduces to some y' with y ≈ y'.▷-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 , eyThe strip lemma modulo _≈_ says that a single reduction step and a reduction sequence from a common source have reducts that agree up to _≈_.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) ecChurch-Rosser modulo _≈_ says that convertible points have reducts that agree up to _≈_. This is the setoid counterpart of from-∿.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 eacWe 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.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)