Как можно использовать исключение идентичности (в agda), чтобы доказать Экман-Хилтон для путей более высокой размерности в HoTT?

Question

Я пытаюсь воспроизвести основную лемму из книги HoTT (стр. 70) для доказательства теоремы Экмана-Хилтона, используя только J (без сопоставления с образцом).

В нем говорится: «Но, в общем, два способа определения горизонтальной композиции согласуются, α ⋆ β = α ⋆ 'β, как мы можем видеть индукцией по α и β, а затем по двум оставшимся 1-путям, сводя все к рефлексивности ... "

Я совершенно не понимаю, правильна ли подпись типа E - должны ли r' и s иметь разные пути? d не уточняется, поэтому я предполагаю, что что-то не так с E? Я также действительно не понимаю, какие два пути я должен использовать, чтобы завершить доказательство, это r' и s? Если да, то я не понимаю, какими должны быть эти окончательные мотивы? Разве уменьшение β до r не устраняет необходимость в дальнейшей индукции по 1-путям?

Любые ответы / решения и, что еще важнее, способы осмысления проблемы приветствуются.

_⋆≡⋆'_ : {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  !}

Ниже приведен остальной код, чтобы попасть сюда.

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

В формализации индукция на основе пути намного удобнее, чем двусторонняя версия. С основанным J мы по существу переписываем в типе цели правую конечную точку пути на левую и сам путь к рефлексивности. С неосновным J мы перезаписываем обе конечные точки в непрозрачную переменную fre sh, следовательно, мы теряем «соединение» левой конечной точки с другими конструкциями в области видимости (поскольку левая конечная точка может встречаться в других типах в scope).

Я не рассматривал точную проблему с вашим определением, но отмечу, что с основанным J это почти тривиально.

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 β