How does one use identity elimination (in agda) to prove Eckmann Hilton for higher dimensional paths in HoTT?

Question

I'm trying to replicate the main lemma in the HoTT book (page 70) for proving the Eckmann Hilton Theorem, only using J (no pattern matching).

It says "But, in general, the two ways of defining horizontal composition agree, α ⋆ β = α ⋆' β, as we can see by induction on α and β and then on the two remaining 1-paths, to reduce everything to reflexivity..."

I'm quite confused as to if the E type signature is correct - should r' and s have different paths? d won't refine, so I assume there's something wrong with E? I also don't really understand which two paths I'm supposed to induct upon to complete the proof, are they r' and s? If so, I don't understand what these final motives should be? Doesn't reducing 'β' down to r eliminate the need for further induction on 1-paths?

Any answers/solutions, and more imporatntly, ways of thinking about the problem are welcome.

_⋆≡⋆'_ : {A : Set} → {a b c : A} {p q : a ≡ b} {r' s : b ≡ c} (α : p ≡ q) (β : r' ≡ s) → (α ⋆ β) ≡ (α ⋆' β)
_⋆≡⋆'_ {A} {a} {b} {c} {p} {q} {r'} {s} α β = J D d p q α c r' s β
  where
    D : (p q : a ≡ b) → p ≡ q → Set
    D p q α = (c : A) (r' s : b ≡ c) (β : r' ≡ s) → (α ⋆ β) ≡ (α ⋆' β)
    E : (r' s : b ≡ c) → r' ≡ s → Set
    -- E p q β = (r ⋆ β) ≡ (r ⋆' β) 
    E r' s β = (_⋆_ {A} {b = b} {c} {r} {r} {r' = r'} {s = s} r β) ≡ (r ⋆' β)
    e : ((s : b ≡ c) → E s s r)
    e r = r --this is for testing purposes
    d : ((p : a ≡ b) → D p p r)
    d p c r' s β = {!J E e  !}

Below is the rest of the code to get here.

module q where

data _≡_ {A : Set} (a : A) : A → Set where
  r : a ≡ a

infix 20 _≡_

J : {A : Set}
    → (D : (x y : A) → (x ≡ y) →  Set)
    -- → (d : (a : A) → (D a a r ))
    → ((a : A) → (D a a r ))
    → (x y : A)
    → (p : x ≡ y)
    ------------------------------------
    → D x y p
J D d x .x r = d x

_∙_ : {A : Set} → {x y : A} → (p : x ≡ y) → {z : A} → (q : y ≡ z) → x ≡ z
_∙_ {A} {x} {y} p {z} q = J D d x y p z q
    where
    D : (x₁ y₁ : A) → x₁ ≡ y₁ → Set
    D x y p = (z : A) → (q : y ≡ z) → x ≡ z
    d : (z₁ : A) → D z₁ z₁ r
    d = λ v z q → q

infixl 40 _∙_

_⁻¹ : {A : Set} {x y : A} → x ≡ y → y ≡ x
-- _⁻¹ {A = A} {x} {y} p = J2 D d x y p
_⁻¹ {A} {x} {y} p = J D d x y p
  where
    D : (x y : A) → x ≡ y → Set
    D x y p = y ≡ x
    d : (a : A) → D a a r
    d a = r

infixr 50 _⁻¹

iₗ : {A : Set} {x y : A} (p : x ≡ y) → p ≡ r ∙ p
iₗ {A} {x} {y} p = J D d x y p 
  where
    D : (x y : A) → x ≡ y → Set
    D x y p = p ≡ r ∙ p
    d : (a : A) → D a a r
    d a = r

iᵣ : {A : Set} {x y : A} (p : x ≡ y) → p ≡ p ∙ r
iᵣ {A} {x} {y} p = J D d x y p 
  where
    D : (x y : A) → x ≡ y → Set
    D x y p = p ≡ p ∙ r
    d : (a : A) → D a a r
    d a = r

_∙ᵣ_ : {A : Set} → {b c : A} {a : A} {p q : a ≡ b} (α : p ≡ q) (r' : b ≡ c) → p ∙ r' ≡ q ∙ r'
_∙ᵣ_ {A} {b} {c} {a} {p} {q} α r' = J D d b c r' a α
  where
    D : (b c : A) → b ≡ c → Set
    D b c r' = (a : A) {p q : a ≡ b} (α : p ≡ q) → p ∙ r' ≡ q ∙ r'
    d : (a : A) → D a a r
    d a a' {p} {q} α = iᵣ p ⁻¹ ∙ α ∙ iᵣ q

-- iᵣ == ruₚ in the book

_∙ₗ_ : {A : Set} → {a b : A} (q : a ≡ b) {c : A} {r' s : b ≡ c} (β : r' ≡ s) → q ∙ r' ≡ q ∙ s
_∙ₗ_ {A} {a} {b} q {c} {r'} {s} β = J D d a b q c β
  where
    D : (a b : A) → a ≡ b → Set
    D a b q = (c : A) {r' s : b ≡ c} (β : r' ≡ s) → q ∙ r' ≡ q ∙ s
    d : (a : A) → D a a r
    d a a' {r'} {s} β = iₗ r' ⁻¹ ∙ β ∙ iₗ s

_⋆_ : {A : Set} → {a b c : A} {p q : a ≡ b} {r' s : b ≡ c} (α : p ≡ q) (β : r' ≡ s) → p ∙ r' ≡ q ∙ s
_⋆_ {A} {q = q} {r' = r'} α β = (α ∙ᵣ r') ∙ (q ∙ₗ β)

_⋆'_ : {A : Set} → {a b c : A} {p q : a ≡ b} {r' s : b ≡ c} (α : p ≡ q) (β : r' ≡ s) → p ∙ r' ≡ q ∙ s
_⋆'_ {A} {p = p} {s = s} α β =  (p ∙ₗ β) ∙ (α ∙ᵣ s)

Answer 1

In formalization, based path induction is far more convenient than the two-sided version. With based J, we essentially rewrite in the goal type the right endpoint of a path to the left one and the path itself to reflexivity. With non-based J, we rewrite both endpoints to a "fresh" opaque variable, hence we lose the "connection" of the left endpoint to other constructions in scope (since the left endpoint may occur in other types in scope).

I haven't looked at the exact issue with your definition, but I note that with based J it's almost trivial.

data _≡_ {A : Set} (a : A) : A → Set where
  r : a ≡ a

infix 20 _≡_

J : {A : Set}{x : A}(P : ∀ y → x ≡ y → Set) → P x r → ∀ {y} p → P y p
J {A} {x} P pr r = pr

tr : {A : Set}(P : A → Set){x y : A} → x ≡ y → P x → P y
tr P p px = J (λ y _ → P y) px p

_∙_ : {A : Set} → {x y z : A} → (p : x ≡ y) → (q : y ≡ z) → x ≡ z
_∙_ {A} {x} {y} {z} p q = tr (x ≡_) q p

ap : {A B : Set}(f : A → B){x y : A} → x ≡ y → f x ≡ f y
ap f {x} {y} p = tr (λ y → f x ≡ f y) p r

infixl 40 _∙_

_∙ᵣ_ : {A : Set} → {b c : A} {a : A} {p q : a ≡ b} (α : p ≡ q) (r' : b ≡ c) → p ∙ r' ≡ q ∙ r'
α ∙ᵣ r' = ap (_∙ r') α

_∙ₗ_ : {A : Set} → {a b : A} (q : a ≡ b) {c : A} {r' s : b ≡ c} (β : r' ≡ s) → q ∙ r' ≡ q ∙ s
q ∙ₗ β = ap (q ∙_) β

_⋆_ : {A : Set} → {a b c : A} {p q : a ≡ b} {r' s : b ≡ c} (α : p ≡ q) (β : r' ≡ s) → p ∙ r' ≡ q ∙ s
_⋆_ {q = q} {r'} α β = (α ∙ᵣ r') ∙ (q ∙ₗ β)

_⋆'_ : {A : Set} → {a b c : A} {p q : a ≡ b} {r' s : b ≡ c} (α : p ≡ q) (β : r' ≡ s) → p ∙ r' ≡ q ∙ s
_⋆'_ {A} {p = p} {s = s} α β = (p ∙ₗ β) ∙ (α ∙ᵣ s)

_⋆≡⋆'_ : {A : Set} → {a b c : A} {p q : a ≡ b} {r' s : b ≡ c} (α : p ≡ q) (β : r' ≡ s) → (α ⋆ β) ≡ (α ⋆' β)
_⋆≡⋆'_ {A} {a} {b} {c} {p} {q} {r'} {s} α β =
  J (λ s β → (α ⋆ β) ≡ (α ⋆' β))
    (J (λ q α → (α ⋆ r) ≡ (α ⋆' r))
       r
       α)   -- induction on α
    β       -- induction on β