Martin Escardo, 3 February 2021.

We consider one special kind of Church-Rosser property motivated by
our applications of this module to the contruction of free groups
without higher-inductive types other than propositional truncation.

\begin{code}

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

open import MLTT.Spartan

module Relations.ChurchRosser
         {𝓀 : Universe}
         {X : 𝓀 Μ‡ }
         (_β–·_ : X β†’ X β†’ 𝓀 Μ‡ )
       where

open import Relations.SRTclosure

infix 1 _◁▷_
infix 1 _◁▷[_]_
infix 1 _▷⋆_
infix 1 _β–·[_]_
infix 1 _∿_

_◁▷_ : X β†’ X β†’ 𝓀 Μ‡
_◁▷_ = s-closure _β–·_

_◁▷[_]_ : X β†’ β„• β†’ X β†’ 𝓀 Μ‡
x ◁▷[ n ] y = iteration _◁▷_ n x y

_∿_ : X β†’ X β†’ 𝓀 Μ‡
_∿_ = srt-closure _β–·_

_▷⋆_ : X β†’ X β†’ 𝓀 Μ‡
_▷⋆_ = rt-closure _β–·_

_β–·[_]_ : X β†’ β„• β†’ X β†’ 𝓀 Μ‡
x β–·[ n ] y = iteration _β–·_ n x y

to-∿ : (x y : X)
     β†’ (Ξ£ z κž‰ X , (x ▷⋆ z) Γ— (y ▷⋆ z))
     β†’ x ∿ y
to-∿ x y (z , r , s) = srt-transitive _β–·_ x z y
                        (rt-gives-srt _β–·_ x z r)
                        (srt-symmetric _β–·_ y z (rt-gives-srt _β–·_ y z s))

module _ (Church-Rosser : (x yβ‚€ y₁ : X)
                        β†’ x β–· yβ‚€
                        β†’ x β–· y₁
                        β†’ (yβ‚€ ＝ y₁) + (Ξ£ y κž‰ X , (yβ‚€ β–· y) Γ— (y₁ β–· y)))
       where

 Church-Rosser⋆ : (x yβ‚€ y₁ : X)
                β†’ x ▷⋆ yβ‚€
                β†’ x β–·  y₁
                β†’ Ξ£ y κž‰ X , (yβ‚€ ▷⋆ y) Γ— (y₁ ▷⋆ y)
 Church-Rosser⋆ x yβ‚€ y₁ (m , i) b = f m x yβ‚€ y₁ i b
  where
   f : (m : β„•) (x yβ‚€ y₁ : X)
     β†’ x β–·[ m ] yβ‚€
     β†’ x β–·  y₁
     β†’ Ξ£ y κž‰ X , (yβ‚€ ▷⋆ y) Γ— (y₁ ▷⋆ y)
   f 0        x x  y₁ refl        e = y₁ , rt-extension _β–·_ x y₁ e , rt-reflexive _β–·_ y₁
   f (succ m) x yβ‚€ y₁ (t , d , i) e = Ξ³ c
    where
     c : (y₁ ＝ t) + (Ξ£ y κž‰ X , (y₁ β–· y) Γ— (t β–· y))
     c = Church-Rosser x y₁ t e d

     Ξ³ : type-of c β†’ Ξ£ u κž‰ X , (yβ‚€ ▷⋆ u) Γ— (y₁ ▷⋆ u)
     Ξ³ (inl refl) = yβ‚€ , rt-reflexive _β–·_ yβ‚€ , m , i
     Ξ³ (inr (y , a , b)) = Ξ΄ IH
      where
       IH : Ξ£ u κž‰ X , (yβ‚€ ▷⋆ u) Γ— (y ▷⋆ u)
       IH = f m t yβ‚€ y i b

       Ξ΄ : type-of IH β†’ Ξ£ u κž‰ X , (yβ‚€ ▷⋆ u) Γ— (y₁ ▷⋆ u)
       Ξ΄ (u , b , n , j) = u , b , succ n , y , a , j

 from-∿ : (x y : X) β†’ x ∿ y β†’ Ξ£ z κž‰ X , (x ▷⋆ z) Γ— (y ▷⋆ z)
 from-∿ x y (m , e) = f m x y e
  where
   f : (m : β„•) (x y : X) β†’ x ◁▷[ m ] y β†’ Ξ£ z κž‰ X , (x ▷⋆ z) Γ— (y ▷⋆ z)
   f 0        x x refl        = x , rt-reflexive _β–·_ x , rt-reflexive _β–·_ x
   f (succ m) x y (z , d , i) = Ξ³ IH d
    where
     IH : Ξ£ t κž‰ X , (z ▷⋆ t) Γ— (y ▷⋆ t)
     IH = f m z y i

     Ξ³ : type-of IH β†’ x ◁▷ z β†’ Ξ£ u κž‰ X , (x ▷⋆ u) Γ— (y ▷⋆ u)
     Ξ³ (t , (n , i) , a) (inl c) = t , (succ n , z , c , i) , a
     Ξ³ (t , (n , i) , a) (inr c) = Ξ΄ Οƒ
      where
       Οƒ : Ξ£ u κž‰ X , (t ▷⋆ u) Γ— (x ▷⋆ u)
       Οƒ = Church-Rosser⋆ z t x (n , i) c

       Ξ΄ : type-of Οƒ β†’ Ξ£ u κž‰ X , (x ▷⋆ u) Γ— (y ▷⋆ u)
       Ξ΄ (u , d , e) = u , e , rt-transitive _β–·_ y t u a d

\end{code}