Reduction
Martin Escardo, July 2026. The reduction underlying the free egroup on a setoid. A word over an alphabet A is a list of letters, each an element of A tagged with a sign that marks whether it is formally inverted, as in Groups.Free. Two adjacent letters cancel when the second is the inverse of the first up to the setoid relation _≈_, rather than only when they are equal. As a consequence the reducts of a word agree only up to the letter-wise relation _≈[FA]_, so that confluence becomes confluence modulo _≈_ in the sense of the module EGroups.ChurchRosserModulo. We define the reduction relation, prove local confluence and hence, via that module, the Church-Rosser property, and then adapt the size-reduction of Groups.Free. The idea there is to keep redexes and reducts structural, so that the type of generators of a word stays 𝓤-small even when the underlying type A of generators is large. The type A lives in 𝓤⁺ and its relation _≈_ is valued in 𝓤, as needed for the universe setoid formed by 𝓤 and type equivalence.{-# OPTIONS --safe --without-K --no-exact-split #-} open import MLTT.Spartan module EGroups.Reduction {𝓤 : Universe} (A : 𝓤 ⁺ ̇ ) (_≈_ : A → A → 𝓤 ̇ ) (≈r : reflexive _≈_) (≈s : symmetric _≈_) (≈t : transitive _≈_) where open import MLTT.Two-Properties open import MLTT.List renaming (_∷_ to _•_ ; _++_ to _◦_ ; ++-assoc to ◦-assoc) open import UF.Embeddings open import UF.Size open import UF.SmallnessProperties open import Relations.SRTclosureThe letters and their formal inverse are exactly as in Groups.Free.X : 𝓤 ⁺ ̇ X = 𝟚 × A _⁻ : X → X (n , a) ⁻ = (complement n , a) FA : 𝓤 ⁺ ̇ FA = List X η : A → FA η a = (₀ , a) • []We define the relation on letters and extend it to words._≈[X]_ : X → X → 𝓤 ̇ (m , a) ≈[X] (n , b) = (m ＝ n) × (a ≈ b) ≈[X]-refl : (x : X) → x ≈[X] x ≈[X]-refl (m , a) = refl , ≈r a ≈[X]-sym : (x y : X) → x ≈[X] y → y ≈[X] x ≈[X]-sym (m , a) (n , b) (p , q) = (p ⁻¹) , ≈s a b q ≈[X]-trans : (x y z : X) → x ≈[X] y → y ≈[X] z → x ≈[X] z ≈[X]-trans (m , a) (n , b) (k , c) (p , q) (p' , q') = (p ∙ p') , ≈t a b c q q' ⁻-cong : (x y : X) → x ≈[X] y → (x ⁻) ≈[X] (y ⁻) ⁻-cong (m , a) (n , b) (p , q) = ap complement p , q _≈[FA]_ : FA → FA → 𝓤 ̇ [] ≈[FA] [] = 𝟙 [] ≈[FA] (y • t) = 𝟘 (x • s) ≈[FA] [] = 𝟘 (x • s) ≈[FA] (y • t) = (x ≈[X] y) × (s ≈[FA] t) ≈[FA]-refl : (s : FA) → s ≈[FA] s ≈[FA]-refl [] = ⋆ ≈[FA]-refl (x • s) = ≈[X]-refl x , ≈[FA]-refl s ≈[FA]-sym : (s t : FA) → s ≈[FA] t → t ≈[FA] s ≈[FA]-sym [] [] ⋆ = ⋆ ≈[FA]-sym (x • s) (y • t) (p , q) = ≈[X]-sym x y p , ≈[FA]-sym s t q ≈[FA]-trans : (s t u : FA) → s ≈[FA] t → t ≈[FA] u → s ≈[FA] u ≈[FA]-trans [] [] [] ⋆ ⋆ = ⋆ ≈[FA]-trans (x • s) (y • t) (z • u) (p , q) (p' , q') = ≈[X]-trans x y z p p' , ≈[FA]-trans s t u q q'_≈[FA]_ is a congruence for concatenation, and it reflects the list structure, via cons-split and left-split below, which allows us to transport a redex along an ≈[FA]-related word.◦-cong : (s s' t t' : FA) → s ≈[FA] s' → t ≈[FA] t' → (s ◦ t) ≈[FA] (s' ◦ t') ◦-cong [] [] t t' ⋆ q = q ◦-cong (x • s) (y • s') t t' (p , r) q = p , ◦-cong s s' t t' r q cons-split : (a : X) (s w : FA) → (a • s) ≈[FA] w → Σ b ꞉ X , Σ w₀ ꞉ FA , (w ＝ b • w₀) × (a ≈[X] b) × (s ≈[FA] w₀) cons-split a s [] () cons-split a s (b • w₀) (p , q) = b , w₀ , refl , p , q left-split : (u v w : FA) → (u ◦ v) ≈[FA] w → Σ u' ꞉ FA , Σ v' ꞉ FA , (w ＝ u' ◦ v') × (u ≈[FA] u') × (v ≈[FA] v') left-split [] v w p = [] , w , refl , ⋆ , p left-split (a • u₀) v w p = γ (cons-split a (u₀ ◦ v) w p) where γ : (Σ b ꞉ X , Σ w₀ ꞉ FA , (w ＝ b • w₀) × (a ≈[X] b) × ((u₀ ◦ v) ≈[FA] w₀)) → Σ u' ꞉ FA , Σ v' ꞉ FA , (w ＝ u' ◦ v') × ((a • u₀) ≈[FA] u') × (v ≈[FA] v') γ (b , w₀ , refl , ab , q) = δ (left-split u₀ v w₀ q) where δ : (Σ u₀' ꞉ FA , Σ v' ꞉ FA , (w₀ ＝ u₀' ◦ v') × (u₀ ≈[FA] u₀') × (v ≈[FA] v')) → Σ u' ꞉ FA , Σ v' ꞉ FA , (b • w₀ ＝ u' ◦ v') × ((a • u₀) ≈[FA] u') × (v ≈[FA] v') δ (u₀' , v' , refl , uu , rr) = (b • u₀') , v' , refl , (ab , uu) , rrWe reduce s to t when s has two adjacent letters x and y with y ≈-inverse to x, and t is s with that pair deleted._▷_ : FA → FA → 𝓤 ⁺ ̇ s ▷ t = Σ u ꞉ FA , Σ v ꞉ FA , Σ x ꞉ X , Σ y ꞉ X , (s ＝ u ◦ x • y • v) × (t ＝ u ◦ v) × (y ≈[X] (x ⁻))Coherence of _≈_ with reduction says that an ≈[FA]-equivalent of a reducible word is reducible to an ≈[FA]-equivalent of its reduct, which is the second hypothesis of confluence modulo _≈_.▷-respects-≈ : (s s' t : FA) → s ≈[FA] s' → s ▷ t → Σ t' ꞉ FA , (s' ▷ t') × (t ≈[FA] t') ▷-respects-≈ s s' t e (u , v , x , y , refl , refl , yx) = I (left-split u (x • y • v) s' e) where I : (Σ u' ꞉ FA , Σ z' ꞉ FA , (s' ＝ u' ◦ z') × (u ≈[FA] u') × ((x • y • v) ≈[FA] z')) → Σ t' ꞉ FA , (s' ▷ t') × ((u ◦ v) ≈[FA] t') I (u' , z' , refl , uu , exyv) = II (cons-split x (y • v) z' exyv) where II : (Σ x' ꞉ X , Σ w ꞉ FA , (z' ＝ x' • w) × (x ≈[X] x') × ((y • v) ≈[FA] w)) → Σ t' ꞉ FA , ((u' ◦ z') ▷ t') × ((u ◦ v) ≈[FA] t') II (x' , w , refl , xx , eyv) = III (cons-split y v w eyv) where III : (Σ y' ꞉ X , Σ v' ꞉ FA , (w ＝ y' • v') × (y ≈[X] y') × (v ≈[FA] v')) → Σ t' ꞉ FA , ((u' ◦ x' • w) ▷ t') × ((u ◦ v) ≈[FA] t') III (y' , v' , refl , yy , vv) = (u' ◦ v') , IV , ◦-cong u u' v v' uu vv where y'x' : y' ≈[X] (x' ⁻) y'x' = ≈[X]-trans y' (x ⁻) (x' ⁻) (≈[X]-trans y' y (x ⁻) (≈[X]-sym y y' yy) yx) (⁻-cong x x' xx) IV : (u' ◦ x' • y' • v') ▷ (u' ◦ v') IV = u' , v' , x' , y' , refl , refl , y'x'We collect some further letter and word algebra used by local confluence.inv-invol : (x : X) → (x ⁻) ⁻ ＝ x inv-invol (n , a) = ap (_, a) (complement-involutive n) to-≈[X] : {x y : X} → x ＝ y → x ≈[X] y to-≈[X] {x} refl = ≈[X]-refl x to-≈[FA] : {s t : FA} → s ＝ t → s ≈[FA] t to-≈[FA] {s} refl = ≈[FA]-refl s •-▷ : (x : X) {s t : FA} → s ▷ t → (x • s) ▷ (x • t) •-▷ x (u , v , a , b , ps , pt , ba) = (x • u) , v , a , b , ap (x •_) ps , ap (x •_) pt , ba redex-sym : (x y : X) → x ≈[X] (y ⁻) → y ≈[X] (x ⁻) redex-sym x y c = ≈[X]-sym (x ⁻) y (≈[X]-trans (x ⁻) ((y ⁻) ⁻) y (⁻-cong x (y ⁻) c) (to-≈[X] (inv-invol y)))We prove local confluence modulo _≈_, the setoid counterpart of Lemma[Church-Rosser] of Groups.Free. Two redexes of a common word either collapse to ≈[FA]-related contractums, when they coincide or overlap, or have a common reduct, when they are disjoint.are-joinable : FA → FA → 𝓤 ⁺ ̇ are-joinable r₀ r₁ = (r₀ ≈[FA] r₁) + (Σ z₀ ꞉ FA , Σ z₁ ꞉ FA , (r₀ ▷ z₀) × (r₁ ▷ z₁) × (z₀ ≈[FA] z₁)) Lemma[Church-Rosser≈] : (u₀ v₀ u₁ v₁ : FA) (a₀ b₀ a₁ b₁ : X) → b₀ ≈[X] (a₀ ⁻) → b₁ ≈[X] (a₁ ⁻) → u₀ ◦ a₀ • b₀ • v₀ ＝ u₁ ◦ a₁ • b₁ • v₁ → are-joinable (u₀ ◦ v₀) (u₁ ◦ v₁) Lemma[Church-Rosser≈] u₀ v₀ u₁ v₁ a₀ b₀ a₁ b₁ cb₀ cb₁ = f u₀ u₁ where f : (u₀ u₁ : FA) → u₀ ◦ a₀ • b₀ • v₀ ＝ u₁ ◦ a₁ • b₁ • v₁ → are-joinable (u₀ ◦ v₀) (u₁ ◦ v₁) f [] [] p = inl (to-≈[FA] (equal-tails (equal-tails p))) f [] (y₁ • []) p = inl e where b₁≈y₁ : b₁ ≈[X] y₁ b₁≈y₁ = ≈[X]-trans b₁ (b₀ ⁻) y₁ (transport (λ - → b₁ ≈[X] (- ⁻)) ((equal-heads (equal-tails p)) ⁻¹) cb₁) (≈[X]-trans (b₀ ⁻) a₀ y₁ (≈[X]-sym a₀ (b₀ ⁻) (redex-sym b₀ a₀ cb₀)) (to-≈[X] (equal-heads p))) e : v₀ ≈[FA] (y₁ • v₁) e = ≈[FA]-trans v₀ (b₁ • v₁) (y₁ • v₁) (to-≈[FA] (equal-tails (equal-tails p))) (b₁≈y₁ , ≈[FA]-refl v₁) f [] (y₁ • z₁ • u₁) p = inr ((u₁ ◦ v₁) , (u₁ ◦ v₁) , d , e , ≈[FA]-refl (u₁ ◦ v₁)) where d : v₀ ▷ (u₁ ◦ v₁) d = transport (_▷ (u₁ ◦ v₁)) ((equal-tails (equal-tails p)) ⁻¹) (u₁ , v₁ , a₁ , b₁ , refl , refl , cb₁) z₁y₁ : z₁ ≈[X] (y₁ ⁻) z₁y₁ = transport (λ - → z₁ ≈[X] (- ⁻)) (equal-heads p) (transport (λ - → - ≈[X] (a₀ ⁻)) (equal-heads (equal-tails p)) cb₀) e : (y₁ • z₁ • (u₁ ◦ v₁)) ▷ (u₁ ◦ v₁) e = [] , (u₁ ◦ v₁) , y₁ , z₁ , refl , refl , z₁y₁ f (y₀ • []) [] p = inl e where y₀≈b₀ : y₀ ≈[X] b₀ y₀≈b₀ = ≈[X]-trans y₀ a₁ b₀ (to-≈[X] (equal-heads p)) (≈[X]-trans a₁ (a₀ ⁻) b₀ (≈[X]-trans a₁ (b₁ ⁻) (a₀ ⁻) (redex-sym b₁ a₁ cb₁) (to-≈[X] (ap (_⁻) ((equal-heads (equal-tails p)) ⁻¹)))) (≈[X]-sym b₀ (a₀ ⁻) cb₀)) e : (y₀ • v₀) ≈[FA] v₁ e = ≈[FA]-trans (y₀ • v₀) (b₀ • v₀) v₁ (y₀≈b₀ , ≈[FA]-refl v₀) (to-≈[FA] (equal-tails (equal-tails p))) f (y₀ • z₀ • u₀) [] p = inr ((u₀ ◦ v₀) , (u₀ ◦ v₀) , d , e , ≈[FA]-refl (u₀ ◦ v₀)) where z₀y₀ : z₀ ≈[X] (y₀ ⁻) z₀y₀ = transport (λ - → z₀ ≈[X] (- ⁻)) ((equal-heads p) ⁻¹) (transport (λ - → - ≈[X] (a₁ ⁻)) ((equal-heads (equal-tails p)) ⁻¹) cb₁) d : (y₀ • z₀ • (u₀ ◦ v₀)) ▷ (u₀ ◦ v₀) d = [] , (u₀ ◦ v₀) , y₀ , z₀ , refl , refl , z₀y₀ e : v₁ ▷ (u₀ ◦ v₀) e = transport (_▷ (u₀ ◦ v₀)) (equal-tails (equal-tails p)) (u₀ , v₀ , a₀ , b₀ , refl , refl , cb₀) f (y₀ • u₀) (y₁ • u₁) p = g (f u₀ u₁ (equal-tails p)) where g : are-joinable (u₀ ◦ v₀) (u₁ ◦ v₁) → are-joinable (y₀ • (u₀ ◦ v₀)) (y₁ • (u₁ ◦ v₁)) g (inl e) = inl (to-≈[X] (equal-heads p) , e) g (inr (z₀ , z₁ , d₀ , d₁ , ez)) = inr ((y₀ • z₀) , (y₁ • z₁) , •-▷ y₀ d₀ , •-▷ y₁ d₁ , (to-≈[X] (equal-heads p) , ez))We repackage this as the local-confluence hypothesis of the module ChurchRosserModulo, on two reductions of a common word.Theorem[Church-Rosser≈] : (s t₀ t₁ : FA) → s ▷ t₀ → s ▷ t₁ → (t₀ ≈[FA] t₁) + (Σ z₀ ꞉ FA , Σ z₁ ꞉ FA , (t₀ ▷ z₀) × (t₁ ▷ z₁) × (z₀ ≈[FA] z₁)) Theorem[Church-Rosser≈] s t₀ t₁ (u₀ , v₀ , a₀ , b₀ , p₀ , q₀ , cb₀) (u₁ , v₁ , a₁ , b₁ , p₁ , q₁ , cb₁) = γ δ where δ : are-joinable (u₀ ◦ v₀) (u₁ ◦ v₁) δ = Lemma[Church-Rosser≈] u₀ v₀ u₁ v₁ a₀ b₀ a₁ b₁ cb₀ cb₁ (u₀ ◦ a₀ • b₀ • v₀ ＝⟨ p₀ ⁻¹ ⟩ s ＝⟨ p₁ ⟩ u₁ ◦ a₁ • b₁ • v₁ ∎) γ : are-joinable (u₀ ◦ v₀) (u₁ ◦ v₁) → (t₀ ≈[FA] t₁) + (Σ z₀ ꞉ FA , Σ z₁ ꞉ FA , (t₀ ▷ z₀) × (t₁ ▷ z₁) × (z₀ ≈[FA] z₁)) γ (inl e) = inl (≈[FA]-trans t₀ (u₀ ◦ v₀) t₁ (to-≈[FA] q₀) (≈[FA]-trans (u₀ ◦ v₀) (u₁ ◦ v₁) t₁ e (to-≈[FA] (q₁ ⁻¹)))) γ (inr (z₀ , z₁ , d₀ , d₁ , ez)) = inr (z₀ , z₁ , transport (_▷ z₀) (q₀ ⁻¹) d₀ , transport (_▷ z₁) (q₁ ⁻¹) d₁ , ez)Instantiating the module EGroups.ChurchRosserModulo with the reduction and the two hypotheses just proved gives the setoid Church-Rosser property and its consequence for generators.open import EGroups.ChurchRosserModulo _▷_ _≈[FA]_ ≈[FA]-refl ≈[FA]-sym ≈[FA]-trans public Church-Rosser≈ : (s t : FA) → s ∿ t → Σ z₀ ꞉ FA , Σ z₁ ꞉ FA , (s ▷⋆ z₀) × (t ▷⋆ z₁) × (z₀ ≈[FA] z₁) Church-Rosser≈ = Church-Rosser-modulo Theorem[Church-Rosser≈] ▷-respects-≈ η-irreducible : (a : A) → does-not-reduce (η a) η-irreducible a z ([] , v , x , y , p , q , c) = []-is-not-cons y v (equal-tails p) η-irreducible a z ((w • []) , v , x , y , p , q , c) = []-is-not-cons x (y • v) (equal-tails p) η-irreducible a z ((w • w₀ • u) , v , x , y , p , q , c) = []-is-not-cons w₀ (u ◦ x • y • v) (equal-tails p) η-identifies-∿-related-points : (a b : A) → η a ∿ η b → η a ≈[FA] η b η-identifies-∿-related-points a b = irreducibles-related-by-∿-are-≈ Theorem[Church-Rosser≈] ▷-respects-≈ (η a) (η b) (η-irreducible a) (η-irreducible b)We adapt the size-reduction of Groups.Free to the setoid reduction.redex : FA → 𝓤 ̇ redex [] = 𝟘 redex (x • []) = 𝟘 redex (x • y • s) = (y ≈[X] (x ⁻)) + redex (y • s) reduct : (s : FA) → redex s → FA reduct (x • y • s) (inl p) = s reduct (x • y • s) (inr r) = x • reduct (y • s) r reduct-gives-▷ : (s : FA) (r : redex s) → s ▷ reduct s r reduct-gives-▷ (x • y • s) (inl c) = [] , s , x , y , refl , refl , c reduct-gives-▷ (x • y • s) (inr r) = •-▷ x (reduct-gives-▷ (y • s) r) redex-chain : ℕ → FA → 𝓤 ̇ redex-chain 0 s = 𝟙 redex-chain (succ n) s = Σ r ꞉ redex s , redex-chain n (reduct s r) chain-reduct : (s : FA) (n : ℕ) → redex-chain n s → FA chain-reduct s 0 ρ = s chain-reduct s (succ n) (r , ρ) = chain-reduct (reduct s r) n ρ chain-lemma→ : (s : FA) (n : ℕ) (ρ : redex-chain n s) → iteration _▷_ n s (chain-reduct s n ρ) chain-lemma→ s 0 ρ = refl chain-lemma→ s (succ n) (r , ρ) = reduct s r , reduct-gives-▷ s r , chain-lemma→ (reduct s r) n ρThe following also mimics the development of Groups.Free._◗_ : FA → FA → 𝓤 ⁺ ̇ [] ◗ t = 𝟘 (x • []) ◗ t = 𝟘 (x • y • s) ◗ t = (y ≈[X] (x ⁻)) × (s ＝ t) _▶_ : FA → FA → 𝓤 ⁺ ̇ [] ▶ t = 𝟘 (x • s) ▶ [] = (x • s) ◗ [] (x • s) ▶ (y • t) = ((x • s) ◗ (y • t)) + ((x ＝ y) × (s ▶ t)) ▷-gives-▶ : {s t : FA} → s ▷ t → s ▶ t ▷-gives-▶ (u , v , x , y , refl , refl , c) = f u v x y c where f : (u v : FA) (x y : X) → y ≈[X] (x ⁻) → (u ◦ x • y • v) ▶ (u ◦ v) f [] [] x y c = c , refl f [] (z • v) x y c = inl (c , refl) f (w • u) v x y c = inr (refl , f u v x y c) lemma-reduct← : (s t : FA) → s ▶ t → Σ r ꞉ redex s , reduct s r ＝ t lemma-reduct← [] t () lemma-reduct← (x • []) [] () lemma-reduct← (x • []) (z • t) (inl ()) lemma-reduct← (x • []) (z • t) (inr (p , ())) lemma-reduct← (x • y • s) [] (p , q) = inl p , q lemma-reduct← (x • y • s) (z • t) (inl (p , q)) = inl p , q lemma-reduct← (x • y • s) (z • t) (inr (p , r)) = inr (pr₁ IH) , (ap (x •_) (pr₂ IH) ∙ ap (_• t) p) where IH : Σ r ꞉ redex (y • s) , reduct (y • s) r ＝ t IH = lemma-reduct← (y • s) t r ▷-gives-redex : (s t : FA) → s ▷ t → Σ r ꞉ redex s , reduct s r ＝ t ▷-gives-redex s t d = lemma-reduct← s t (▷-gives-▶ d) chain-lemma← : (s t : FA) (n : ℕ) → iteration _▷_ n s t → Σ ρ ꞉ redex-chain n s , chain-reduct s n ρ ＝ t chain-lemma← s t 0 r = ⋆ , r chain-lemma← s t (succ n) (z , b , c) = γ (▷-gives-redex s z b) where γ : (Σ r ꞉ redex s , reduct s r ＝ z) → Σ ρ ꞉ redex-chain (succ n) s , chain-reduct s (succ n) ρ ＝ t γ (r , refl) = δ (chain-lemma← (reduct s r) t n c) where δ : (Σ ρ ꞉ redex-chain n (reduct s r) , chain-reduct (reduct s r) n ρ ＝ t) → Σ ρ ꞉ redex-chain (succ n) s , chain-reduct s (succ n) ρ ＝ t δ (ρ , q) = (r , ρ) , q generator : FA → 𝓤 ⁺ ̇ generator s = Σ n ꞉ ℕ , Σ ρ ꞉ redex-chain n s , fiber η (chain-reduct s n ρ) underlying-generator : {s : FA} → generator s → A underlying-generator (n , ρ , a , p) = aUnlike in Groups.Free, we don't assume that A is a set, and, like in Groups.Free, we don't assume decidable equality on it. But η is the composite of pairing with the sign ₀ and the formation of a singleton list, and hence a decidable embedding, so that its fibers have any size, which is what keeps generator s small when A is large.η-is-embedding : is-embedding η η-is-embedding = ∘-is-embedding pair₀-is-embedding []-is-embedding η-is-decidable : each-fiber-of η is-decidable η-is-decidable = ∘-decidable-embeddings []-is-embedding pair₀-is-decidable []-is-decidable η-has-any-size : (𝓦 : Universe) → η is 𝓦 small-map η-has-any-size 𝓦 = decidable-embeddings-have-any-size 𝓦 η-is-embedding η-is-decidable generator-is-small : (s : FA) → generator s is 𝓤 small generator-is-small s = Σ-is-small (native-size ℕ) (λ n → Σ-is-small (native-size (redex-chain n s)) (λ ρ → η-has-any-size 𝓤 (chain-reduct s n ρ)))An ≈[FA]-equivalent of a generator is again a generator, up to _≈_. This is the setoid replacement for the injectivity of η after quotienting.≈[FA]-η→ : {a : A} (z : FA) → η a ≈[FA] z → Σ c ꞉ A , (z ＝ η c) × (c ≈ a) ≈[FA]-η→ [] () ≈[FA]-η→ ((m , c) • []) ((p , q) , ⋆) = c , ap (λ n → (n , c) • []) (p ⁻¹) , ≈s _ c q ≈[FA]-η→ ((m , c) • (x • t)) (_ , ())If η a is convertible to s, then s is a generator whose underlying element is equivalent to a. This uses the setoid Church-Rosser property and the irreducibility of η a.∿→generator⁺ : {a : A} {s : FA} → η a ∿ s → Σ γ ꞉ generator s , (underlying-generator γ ≈ a) ∿→generator⁺ {a} {s} e = γ (Church-Rosser≈ (η a) s e) where γ : (Σ z₀ ꞉ FA , Σ z₁ ꞉ FA , (η a ▷⋆ z₀) × (s ▷⋆ z₁) × (z₀ ≈[FA] z₁)) → Σ g ꞉ generator s , (underlying-generator g ≈ a) γ (z₀ , z₁ , r₀ , r₁ , ez) = δ (≈[FA]-η→ z₁ I₁) where I₀ : η a ＝ z₀ I₀ = ▷⋆-from-irreducible (η a) z₀ (η-irreducible a) r₀ I₁ : η a ≈[FA] z₁ I₁ = transport (_≈[FA] z₁) (I₀ ⁻¹) ez δ : (Σ c ꞉ A , (z₁ ＝ η c) × (c ≈ a)) → Σ g ꞉ generator s , (underlying-generator g ≈ a) δ (c , ezc , eca) = ε (transport (s ▷⋆_) ezc r₁) where ε : s ▷⋆ (η c) → Σ g ꞉ generator s , (underlying-generator g ≈ a) ε (n , it) = ζ (chain-lemma← s (η c) n it) where ζ : (Σ ρ ꞉ redex-chain n s , chain-reduct s n ρ ＝ η c) → Σ g ꞉ generator s , (underlying-generator g ≈ a) ζ (ρ , q) = (n , ρ , c , (q ⁻¹)) , eca ∿→generator : {a : A} {s : FA} → η a ∿ s → generator s ∿→generator e = pr₁ (∿→generator⁺ e) underlying-generator-∿→generator : {a : A} {s : FA} (e : η a ∿ s) → underlying-generator (∿→generator e) ≈ a underlying-generator-∿→generator e = pr₂ (∿→generator⁺ e) ◦-▷-left : {s s' : FA} → s ▷ s' → (t : FA) → (s ◦ t) ▷ (s' ◦ t) ◦-▷-left (u , v , x , y , refl , refl , c) t = u , (v ◦ t) , x , y , ◦-assoc u (x • y • v) t , ◦-assoc u v t , c ◦-▷-right : (s : FA) {t t' : FA} → t ▷ t' → (s ◦ t) ▷ (s ◦ t') ◦-▷-right s (u , v , x , y , refl , refl , c) = (s ◦ u) , v , x , y , ((◦-assoc s u (x • y • v)) ⁻¹) , ((◦-assoc s u v) ⁻¹) , cHence convertibility _∿_ is a congruence for concatenation, so _◦_ is a well-defined operation on the setoid of words up to _∿_, with no quotient taken. This is the setoid, together with its operation, from which the free egroup is built in the next module.∿-◦-left : {s s' : FA} → s ∿ s' → (t : FA) → (s ◦ t) ∿ (s' ◦ t) ∿-◦-left {s} {s'} e t = srt-induction _▷_ R R-sym R-refl R-trans R-base s s' e where R : FA → FA → 𝓤 ⁺ ̇ R p q = (p ◦ t) ∿ (q ◦ t) R-refl : reflexive R R-refl p = srt-reflexive _▷_ (p ◦ t) R-sym : symmetric R R-sym p q = srt-symmetric _▷_ (p ◦ t) (q ◦ t) R-trans : transitive R R-trans p q r = srt-transitive _▷_ (p ◦ t) (q ◦ t) (r ◦ t) R-base : _▷_ ⊑ R R-base p q d = srt-extension _▷_ (p ◦ t) (q ◦ t) (◦-▷-left d t) ∿-◦-right : (s : FA) {t t' : FA} → t ∿ t' → (s ◦ t) ∿ (s ◦ t') ∿-◦-right s {t} {t'} e = srt-induction _▷_ R R-sym R-refl R-trans R-base t t' e where R : FA → FA → 𝓤 ⁺ ̇ R p q = (s ◦ p) ∿ (s ◦ q) R-refl : reflexive R R-refl p = srt-reflexive _▷_ (s ◦ p) R-sym : symmetric R R-sym p q = srt-symmetric _▷_ (s ◦ p) (s ◦ q) R-trans : transitive R R-trans p q r = srt-transitive _▷_ (s ◦ p) (s ◦ q) (s ◦ r) R-base : _▷_ ⊑ R R-base p q d = srt-extension _▷_ (s ◦ p) (s ◦ q) (◦-▷-right s d) ◦-cong-∿ : {s s' t t' : FA} → s ∿ s' → t ∿ t' → (s ◦ t) ∿ (s' ◦ t') ◦-cong-∿ {s} {s'} {t} {t'} es et = srt-transitive _▷_ (s ◦ t) (s' ◦ t) (s' ◦ t') (∿-◦-left es t) (∿-◦-right s' et)