在 Cubical 模式下定义非一元函数
Defining non-unary functions in Cubical mode
我想用立方模式下的两个更高归纳类型的参数定义一个函数。我正在使用 the cubical package 作为我的 "prelude" 库。
我首先定义一个整数的商类型为 HIT:
{-# OPTIONS --cubical #-}
module _ where
open import Data.Nat renaming (_+_ to _+̂_)
open import Cubical.Core.Prelude
data ℤ : Set where
_-_ : (x : ℕ) → (y : ℕ) → ℤ
quot : ∀ {x y x′ y′} → (x ℕ+ y′) ≡ (x′ ℕ+ y) → (x - y) ≡ (x′ - y′)
然后我可以使用模式匹配定义一元函数：
_+1 : ℤ → ℤ
(x - y) +1 = suc x - y
quot {x} {y} prf i +1 = quot {suc x} {y} (cong suc prf) i
到目前为止，还不错。但是如果我想定义一个二元函数，比如加法呢？
首先，让我们把枯燥的算术证明抛开：
import Data.Nat.Properties
open Data.Nat.Properties.SemiringSolver
using (prove; solve; _:=_; con; var; _:+_; _:*_; :-_; _:-_)
open import Relation.Binary.PropositionalEquality renaming (refl to prefl; _≡_ to _=̂_) using ()
fromPropEq : ∀ {ℓ A} {x y : A} → _=̂_ {ℓ} {A} x y → x ≡ y
fromPropEq prefl = refl
open import Function using (_$_)
reorder : ∀ x y a b → (x +̂ a) +̂ (y +̂ b) ≡ (x +̂ y) +̂ (a +̂ b)
reorder x y a b = fromPropEq $ solve 4 (λ x y a b → (x :+ a) :+ (y :+ b) := (x :+ y) :+ (a :+ b)) prefl x y a b
inner-lemma : ∀ x y a b a′ b′ → a +̂ b′ ≡ a′ +̂ b → (x +̂ a) +̂ (y +̂ b′) ≡ (x +̂ a′) +̂ (y +̂ b)
inner-lemma x y a b a′ b′ prf = begin
(x +̂ a) +̂ (y +̂ b′) ≡⟨ reorder x y a b′ ⟩
(x +̂ y) +̂ (a +̂ b′) ≡⟨ cong (x +̂ y +̂_) prf ⟩
(x +̂ y) +̂ (a′ +̂ b) ≡⟨ sym (reorder x y a′ b) ⟩
(x +̂ a′) +̂ (y +̂ b) ∎
outer-lemma : ∀ x y x′ y′ a b → x +̂ y′ ≡ x′ +̂ y → (x +̂ a) +̂ (y′ +̂ b) ≡ (x′ +̂ a) +̂ (y +̂ b)
outer-lemma x y x′ y′ a b prf = begin
(x +̂ a) +̂ (y′ +̂ b) ≡⟨ reorder x y′ a b ⟩
(x +̂ y′) +̂ (a +̂ b) ≡⟨ cong (_+̂ (a +̂ b)) prf ⟩
(x′ +̂ y) +̂ (a +̂ b) ≡⟨ sym (reorder x′ y a b) ⟩
(x′ +̂ a) +̂ (y +̂ b) ∎
我现在尝试使用模式匹配来定义 _+_，但我不知道如何处理 "points in the center of the face"，可以这么说：
_+_ : ℤ → ℤ → ℤ
(x - y) + (a - b) = (x +̂ a) - (y +̂ b)
(x - y) + quot {a} {b} {a′} {b′} eq₂ j = quot {x +̂ a} {y +̂ b} {x +̂ a′} {y +̂ b′} (inner-lemma x y a b a′ b′ eq₂) j
quot {x} {y} {x′} {y′} eq₁ i + (a - b) = quot {x +̂ a} {y +̂ b} {x′ +̂ a} {y′ +̂ b} (outer-lemma x y x′ y′ a b eq₁) i
quot {x} {y} {x′} {y′} eq₁ i + quot {a} {b} {a′} {b′} eq₂ j = ?
所以基本上我遇到的是以下情况：
p Xᵢ
X ---------+---> X′
p₀ i
A X+A --------\---> X′+A
| | |
q| q₀ | | qᵢ
| | |
Aⱼ + j+ [+] <--- This is where we want to get to!
| | |
V V p₁ |
A′ X+A′ -------/---> X′+A′
i
与
X = (x - y)
X′ = (x′ - y′)
A = (a - b)
A′ = (a′ - b′)
p : X ≡ X′
p = quot eq₁
q : A ≡ A′
q = quot eq₂
p₀ : X + A ≡ X′ + A
p₀ = quot (outer-lemma x y x′ y′ a b eq₁)
p₁ : X + A′ ≡ X′ + A′
p₁ = quot (outer-lemma x y x′ y′ a′ b′ eq₁)
q₀ : X + A ≡ X + A′
q₀ = quot (inner-lemma x y a b a′ b′ eq₂)
q₁ : X′ + A ≡ X′ + A′
q₁ = quot (inner-lemma x′ y′ a b a′ b′ eq₂)
我正在使用通过i水平推出q₀:
slidingLid : ∀ {ℓ} {A : Set ℓ} {a b c d} (p₀ : a ≡ b) (p₁ : c ≡ d) (q : a ≡ c) → ∀ i → p₀ i ≡ p₁ i
slidingLid p₀ p₁ q i j = comp (λ _ → A)
(λ{ k (i = i0) → q j
; k (j = i0) → p₀ (i ∧ k)
; k (j = i1) → p₁ (i ∧ k)
})
(inc (q j))
并使用它，我对 + 的尝试如下：
quot {x} {y} {x′} {y′} eq₁ i + quot {a} {b} {a′} {b′} eq₂ j = Xᵢ+Aⱼ
where
X = (x - y)
X′ = (x′ - y′)
A = (a - b)
A′ = (a′ - b′)
p : X ≡ X′
p = quot eq₁
q : A ≡ A′
q = quot eq₂
p₀ : X + A ≡ X′ + A
p₀ = quot (outer-lemma x y x′ y′ a b eq₁)
p₁ : X + A′ ≡ X′ + A′
p₁ = quot (outer-lemma x y x′ y′ a′ b′ eq₁)
q₀ : X + A ≡ X + A′
q₀ = quot (inner-lemma x y a b a′ b′ eq₂)
qᵢ : ∀ i → p₀ i ≡ p₁ i
qᵢ = slidingLid p₀ p₁ q₀
q₁ : X′ + A ≡ X′ + A′
q₁ = quot (inner-lemma x′ y′ a b a′ b′ eq₂)
Xᵢ+Aⱼ = qᵢ i j
但这失败并出现以下类型错误：
quot (inner-lemma x′ y′ a b a′ b′ eq₂) j !=
hcomp
(λ { i ((~ i1 ∨ ~ j ∨ j) = i1)
→ transp (λ j₁ → ℤ) i
((λ { i₁ (i1 = i0) → q₀ eq₁ i1 eq₂ j j
; i₁ (j = i0) → p₀ eq₁ i1 eq₂ j (i1 ∧ i₁)
; i₁ (j = i1) → p₁ eq₁ i1 eq₂ j (i1 ∧ i₁)
})
(i ∨ i0) _)
})
(transp (λ _ → ℤ) i0 (ouc (inc (q₀ eq₁ i1 eq₂ j j))))
of type ℤ
一个可能出错的提示是，虽然这三个方面很好地退化：
top : ∀ i → qᵢ i i0 ≡ p i + q i0
top i = refl
bottom : ∀ i → qᵢ i i1 ≡ p i + q i1
bottom i = refl
left : qᵢ i0 ≡ q₀
left = refl
最右边没有：
right : qᵢ i1 ≡ q₁
right = ? -- refl fails here
我猜是因为qᵢ是从左边拉出来的，所以右边和被推到尽头的qᵢ之间还是会有一个洞，即这样还是会有可能，在 qᵢ i1 和 q₁ 之间的 O 处有一个洞：
p₀
X+A ------------> X′+A
| /|
q₀ | / | q₁
| | |
| | O|
| \ |
V p₁ \|
X+A′ -----------> X′+A′
直觉上是有道理的，因为 q₁ 是一些关于自然数的代数陈述，而 qᵢ i1 是关于不同自然数的不同代数陈述的连续变形版本，所以仍然有成为两者之间的某种联系；但我不知道从哪里开始建立这种联系（即明确构建 qᵢ i1 和 q₁ 之间的 2 路径）
这是一个部分答案，希望它能引诱某人解决这个难题的下一个部分。
所以，我设法证明了 right，并由此证明了从 left 到 right 有一个连续曲面：
right : qᵢ i1 ≡ q₁
right i = comp
(λ j → p j + A ≡ p j + A′)
(λ { j (i = i0) → qᵢ j
; j (i = i1) → cong (λ ξ → quot {x} {y} {x′} {y′} eq₁ j + ξ) q
}
(inc (left i))
surface : PathP (λ i → p₀ i ≡ p₁ i) q₀ q₁
surface i = comp (λ j → p₀ i ≡ p₁ i)
(λ { j (i = i0) → q₀
; j (i = i1) → right j
})
(inc (qᵢ i))
Xᵢ+Aⱼ = surface i j
Xᵢ+Aⱼ的这个定义通过了类型检查，但在终止检查期间失败了。基本上，所有出现的 _+_ 都被标记为有问题；特别是 right 定义中的函数：p j + A 和 p j + A′ 调用，以及 cong (λ ξ → quot {x} {y} {x′} {y′} eq₁ j + ξ) q.
中的同余函数
前两个对我来说意义不大：我已经为中点+点和点+点的情况定义了_+-，p j + A和[中的第二个参数=18=]分明就是分。
第三个，我正在寻找建议。
事实证明 在 qᵢ i1 和 q₁ 之间存在漏洞的可能性，我一直在尝试进行形式化。当我回到 the HoTT book 尝试为所有商类型更抽象地解决这个问题时，这个解决方案打动了我，而不仅仅是这个特定的 ℤ 类型。引用第 6.10 节：
We can also describe this directly, as the higher inductive type A/R
generated by
A function q : A → A/R;
For each a, b : A such that R(a, b), an equality q(a) = q(b); and
The 0-truncation constructor: for all x, y : A/R and r,s : x = y, we have r = s.
所以我缺少的是第三点：缺少更高类型的结构是需要明确建模的东西。
利用这些信息，我在 ℤ:
中添加了第三个构造函数
Same : ℕ → ℕ → ℕ → ℕ → Set
Same x y x′ y′ = x +̂ y′ ≡ x′ +̂ y
data ℤ : Set where
_-_ : (x : ℕ) → (y : ℕ) → ℤ
quot : ∀ {x y x′ y′} → Same x y x′ y′ → (x - y) ≡ (x′ - y′)
trunc : {x y : ℤ} → (p q : x ≡ y) → p ≡ q
这使我能够证明 right（因此，surface）没有进一步的问题。一个小问题是尝试使用模式匹配导致了一些奇怪的 "function is not fibrant" 错误，所以我最终通过以下显式消除器：
module ℤElim {ℓ} {P : ℤ → Set ℓ}
(point* : ∀ x y → P (x - y))
(quot* : ∀ {x y x′ y′} same → PathP (λ i → P (quot {x} {y} {x′} {y′} same i)) (point* x y) (point* x′ y′))
(trunc* : ∀ {x y} {p q : x ≡ y} → ∀ {fx : P x} {fy : P y} (eq₁ : PathP (λ i → P (p i)) fx fy) (eq₂ : PathP (λ i → P (q i)) fx fy) → PathP (λ i → PathP (λ j → P (trunc p q i j)) fx fy) eq₁ eq₂)
where
ℤ-elim : ∀ x → P x
ℤ-elim (x - y) = point* x y
ℤ-elim (quot p i) = quot* p i
ℤ-elim (trunc p q i j) = trunc* (cong ℤ-elim p) (cong ℤ-elim q) i j
等供参考，_+_的完整实现使用ℤ-elim:
_+_ : ℤ → ℤ → ℤ
_+_ = ℤ-elim
(λ x y → ℤ-elim
(λ a b → (x +̂ a) - (y +̂ b))
(λ eq₂ → quot (inner-lemma x y eq₂))
trunc)
(λ {x} {y} {x′} {y′} eq₁ i → ℤ-elim
(λ a b → quot (outer-lemma x y eq₁) i)
(λ {a} {b} {a′} {b′} eq₂ j → lemma {x} {y} {x′} {y′} {a} {b} {a′} {b′} eq₁ eq₂ i j )
trunc)
(λ {_} {_} {_} {_} {x+} {y+} eq₁ eq₂ i →
funExt λ a → λ j → trunc {x+ a} {y+ a} (ap eq₁ a) (ap eq₂ a) i j)
where
lemma : ∀ {x y x′ y′ a b a′ b′} → Same x y x′ y′ → Same a b a′ b′ → I → I → ℤ
lemma {x} {y} {x′} {y′} {a} {b} {a′} {b′} eq₁ eq₂ i j = surface i j
where
{-
p Xᵢ
X ---------+---> X′
p₀ i
A X+A --------\---> X′+A
| | |
q| q₀ | | qᵢ
| | |
Aⱼ + j+ [+] <--- This is where we want to get to!
| | |
V V p₁ |
A′ X+A′ -------/---> X′+A′
i
-}
X = x - y
X′ = x′ - y′
A = a - b
A′ = a′ - b′
X+A = (x +̂ a) - (y +̂ b)
X′+A = (x′ +̂ a) - (y′ +̂ b)
X+A′ = (x +̂ a′) - (y +̂ b′)
X′+A′ = (x′ +̂ a′) - (y′ +̂ b′)
p : X ≡ X′
p = quot eq₁
q : A ≡ A′
q = quot eq₂
p₀ : X+A ≡ X′+A
p₀ = quot (outer-lemma x y eq₁)
p₁ : X+A′ ≡ X′+A′
p₁ = quot (outer-lemma x y eq₁)
q₀ : X+A ≡ X+A′
q₀ = quot (inner-lemma x y eq₂)
q₁ : X′+A ≡ X′+A′
q₁ = quot (inner-lemma x′ y′ eq₂)
qᵢ : ∀ i → p₀ i ≡ p₁ i
qᵢ = slidingLid p₀ p₁ q₀
left : qᵢ i0 ≡ q₀
left = refl
right : qᵢ i1 ≡ q₁
right = trunc (qᵢ i1) q₁
surface : PathP (λ i → p₀ i ≡ p₁ i) q₀ q₁
surface i = comp (λ j → p₀ i ≡ p₁ i)
(λ { j (i = i0) → left j
; j (i = i1) → right j
})
(inc (qᵢ i))
我想用立方模式下的两个更高归纳类型的参数定义一个函数。我正在使用 the cubical package 作为我的 "prelude" 库。
我首先定义一个整数的商类型为 HIT:
{-# OPTIONS --cubical #-}
module _ where
open import Data.Nat renaming (_+_ to _+̂_)
open import Cubical.Core.Prelude
data ℤ : Set where
_-_ : (x : ℕ) → (y : ℕ) → ℤ
quot : ∀ {x y x′ y′} → (x ℕ+ y′) ≡ (x′ ℕ+ y) → (x - y) ≡ (x′ - y′)
然后我可以使用模式匹配定义一元函数：
_+1 : ℤ → ℤ
(x - y) +1 = suc x - y
quot {x} {y} prf i +1 = quot {suc x} {y} (cong suc prf) i
到目前为止，还不错。但是如果我想定义一个二元函数，比如加法呢？
首先，让我们把枯燥的算术证明抛开：
import Data.Nat.Properties
open Data.Nat.Properties.SemiringSolver
using (prove; solve; _:=_; con; var; _:+_; _:*_; :-_; _:-_)
open import Relation.Binary.PropositionalEquality renaming (refl to prefl; _≡_ to _=̂_) using ()
fromPropEq : ∀ {ℓ A} {x y : A} → _=̂_ {ℓ} {A} x y → x ≡ y
fromPropEq prefl = refl
open import Function using (_$_)
reorder : ∀ x y a b → (x +̂ a) +̂ (y +̂ b) ≡ (x +̂ y) +̂ (a +̂ b)
reorder x y a b = fromPropEq $ solve 4 (λ x y a b → (x :+ a) :+ (y :+ b) := (x :+ y) :+ (a :+ b)) prefl x y a b
inner-lemma : ∀ x y a b a′ b′ → a +̂ b′ ≡ a′ +̂ b → (x +̂ a) +̂ (y +̂ b′) ≡ (x +̂ a′) +̂ (y +̂ b)
inner-lemma x y a b a′ b′ prf = begin
(x +̂ a) +̂ (y +̂ b′) ≡⟨ reorder x y a b′ ⟩
(x +̂ y) +̂ (a +̂ b′) ≡⟨ cong (x +̂ y +̂_) prf ⟩
(x +̂ y) +̂ (a′ +̂ b) ≡⟨ sym (reorder x y a′ b) ⟩
(x +̂ a′) +̂ (y +̂ b) ∎
outer-lemma : ∀ x y x′ y′ a b → x +̂ y′ ≡ x′ +̂ y → (x +̂ a) +̂ (y′ +̂ b) ≡ (x′ +̂ a) +̂ (y +̂ b)
outer-lemma x y x′ y′ a b prf = begin
(x +̂ a) +̂ (y′ +̂ b) ≡⟨ reorder x y′ a b ⟩
(x +̂ y′) +̂ (a +̂ b) ≡⟨ cong (_+̂ (a +̂ b)) prf ⟩
(x′ +̂ y) +̂ (a +̂ b) ≡⟨ sym (reorder x′ y a b) ⟩
(x′ +̂ a) +̂ (y +̂ b) ∎
我现在尝试使用模式匹配来定义 _+_，但我不知道如何处理 "points in the center of the face"，可以这么说：
_+_ : ℤ → ℤ → ℤ
(x - y) + (a - b) = (x +̂ a) - (y +̂ b)
(x - y) + quot {a} {b} {a′} {b′} eq₂ j = quot {x +̂ a} {y +̂ b} {x +̂ a′} {y +̂ b′} (inner-lemma x y a b a′ b′ eq₂) j
quot {x} {y} {x′} {y′} eq₁ i + (a - b) = quot {x +̂ a} {y +̂ b} {x′ +̂ a} {y′ +̂ b} (outer-lemma x y x′ y′ a b eq₁) i
quot {x} {y} {x′} {y′} eq₁ i + quot {a} {b} {a′} {b′} eq₂ j = ?
所以基本上我遇到的是以下情况：
p Xᵢ
X ---------+---> X′
p₀ i
A X+A --------\---> X′+A
| | |
q| q₀ | | qᵢ
| | |
Aⱼ + j+ [+] <--- This is where we want to get to!
| | |
V V p₁ |
A′ X+A′ -------/---> X′+A′
i
与
X = (x - y)
X′ = (x′ - y′)
A = (a - b)
A′ = (a′ - b′)
p : X ≡ X′
p = quot eq₁
q : A ≡ A′
q = quot eq₂
p₀ : X + A ≡ X′ + A
p₀ = quot (outer-lemma x y x′ y′ a b eq₁)
p₁ : X + A′ ≡ X′ + A′
p₁ = quot (outer-lemma x y x′ y′ a′ b′ eq₁)
q₀ : X + A ≡ X + A′
q₀ = quot (inner-lemma x y a b a′ b′ eq₂)
q₁ : X′ + A ≡ X′ + A′
q₁ = quot (inner-lemma x′ y′ a b a′ b′ eq₂)
我正在使用i水平推出q₀:
slidingLid : ∀ {ℓ} {A : Set ℓ} {a b c d} (p₀ : a ≡ b) (p₁ : c ≡ d) (q : a ≡ c) → ∀ i → p₀ i ≡ p₁ i
slidingLid p₀ p₁ q i j = comp (λ _ → A)
(λ{ k (i = i0) → q j
; k (j = i0) → p₀ (i ∧ k)
; k (j = i1) → p₁ (i ∧ k)
})
(inc (q j))
并使用它，我对 + 的尝试如下：
quot {x} {y} {x′} {y′} eq₁ i + quot {a} {b} {a′} {b′} eq₂ j = Xᵢ+Aⱼ
where
X = (x - y)
X′ = (x′ - y′)
A = (a - b)
A′ = (a′ - b′)
p : X ≡ X′
p = quot eq₁
q : A ≡ A′
q = quot eq₂
p₀ : X + A ≡ X′ + A
p₀ = quot (outer-lemma x y x′ y′ a b eq₁)
p₁ : X + A′ ≡ X′ + A′
p₁ = quot (outer-lemma x y x′ y′ a′ b′ eq₁)
q₀ : X + A ≡ X + A′
q₀ = quot (inner-lemma x y a b a′ b′ eq₂)
qᵢ : ∀ i → p₀ i ≡ p₁ i
qᵢ = slidingLid p₀ p₁ q₀
q₁ : X′ + A ≡ X′ + A′
q₁ = quot (inner-lemma x′ y′ a b a′ b′ eq₂)
Xᵢ+Aⱼ = qᵢ i j
但这失败并出现以下类型错误：
quot (inner-lemma x′ y′ a b a′ b′ eq₂) j != hcomp (λ { i ((~ i1 ∨ ~ j ∨ j) = i1) → transp (λ j₁ → ℤ) i ((λ { i₁ (i1 = i0) → q₀ eq₁ i1 eq₂ j j ; i₁ (j = i0) → p₀ eq₁ i1 eq₂ j (i1 ∧ i₁) ; i₁ (j = i1) → p₁ eq₁ i1 eq₂ j (i1 ∧ i₁) }) (i ∨ i0) _) }) (transp (λ _ → ℤ) i0 (ouc (inc (q₀ eq₁ i1 eq₂ j j)))) of type ℤ
一个可能出错的提示是，虽然这三个方面很好地退化：
top : ∀ i → qᵢ i i0 ≡ p i + q i0
top i = refl
bottom : ∀ i → qᵢ i i1 ≡ p i + q i1
bottom i = refl
left : qᵢ i0 ≡ q₀
left = refl
最右边没有：
right : qᵢ i1 ≡ q₁
right = ? -- refl fails here
我猜是因为qᵢ是从左边拉出来的，所以右边和被推到尽头的qᵢ之间还是会有一个洞，即这样还是会有可能，在 qᵢ i1 和 q₁ 之间的 O 处有一个洞：
p₀
X+A ------------> X′+A
| /|
q₀ | / | q₁
| | |
| | O|
| \ |
V p₁ \|
X+A′ -----------> X′+A′
直觉上是有道理的，因为 q₁ 是一些关于自然数的代数陈述，而 qᵢ i1 是关于不同自然数的不同代数陈述的连续变形版本，所以仍然有成为两者之间的某种联系；但我不知道从哪里开始建立这种联系（即明确构建 qᵢ i1 和 q₁ 之间的 2 路径）
这是一个部分答案，希望它能引诱某人解决这个难题的下一个部分。
所以，我设法证明了 right，并由此证明了从 left 到 right 有一个连续曲面：
right : qᵢ i1 ≡ q₁
right i = comp
(λ j → p j + A ≡ p j + A′)
(λ { j (i = i0) → qᵢ j
; j (i = i1) → cong (λ ξ → quot {x} {y} {x′} {y′} eq₁ j + ξ) q
}
(inc (left i))
surface : PathP (λ i → p₀ i ≡ p₁ i) q₀ q₁
surface i = comp (λ j → p₀ i ≡ p₁ i)
(λ { j (i = i0) → q₀
; j (i = i1) → right j
})
(inc (qᵢ i))
Xᵢ+Aⱼ = surface i j
Xᵢ+Aⱼ的这个定义通过了类型检查，但在终止检查期间失败了。基本上，所有出现的 _+_ 都被标记为有问题；特别是 right 定义中的函数：p j + A 和 p j + A′ 调用，以及 cong (λ ξ → quot {x} {y} {x′} {y′} eq₁ j + ξ) q.
前两个对我来说意义不大：我已经为中点+点和点+点的情况定义了_+-，p j + A和[中的第二个参数=18=]分明就是分。
第三个，我正在寻找建议。
事实证明 在 qᵢ i1 和 q₁ 之间存在漏洞的可能性，我一直在尝试进行形式化。当我回到 the HoTT book 尝试为所有商类型更抽象地解决这个问题时，这个解决方案打动了我，而不仅仅是这个特定的 ℤ 类型。引用第 6.10 节：
We can also describe this directly, as the higher inductive type A/R generated by
A function
q : A → A/R;For each
a, b : Asuch thatR(a, b), an equalityq(a) = q(b); andThe 0-truncation constructor: for all
x, y : A/Randr,s : x = y, we haver = s.
所以我缺少的是第三点：缺少更高类型的结构是需要明确建模的东西。
利用这些信息，我在 ℤ:
Same : ℕ → ℕ → ℕ → ℕ → Set
Same x y x′ y′ = x +̂ y′ ≡ x′ +̂ y
data ℤ : Set where
_-_ : (x : ℕ) → (y : ℕ) → ℤ
quot : ∀ {x y x′ y′} → Same x y x′ y′ → (x - y) ≡ (x′ - y′)
trunc : {x y : ℤ} → (p q : x ≡ y) → p ≡ q
这使我能够证明 right（因此，surface）没有进一步的问题。一个小问题是尝试使用模式匹配导致了一些奇怪的 "function is not fibrant" 错误，所以我最终通过以下显式消除器：
module ℤElim {ℓ} {P : ℤ → Set ℓ}
(point* : ∀ x y → P (x - y))
(quot* : ∀ {x y x′ y′} same → PathP (λ i → P (quot {x} {y} {x′} {y′} same i)) (point* x y) (point* x′ y′))
(trunc* : ∀ {x y} {p q : x ≡ y} → ∀ {fx : P x} {fy : P y} (eq₁ : PathP (λ i → P (p i)) fx fy) (eq₂ : PathP (λ i → P (q i)) fx fy) → PathP (λ i → PathP (λ j → P (trunc p q i j)) fx fy) eq₁ eq₂)
where
ℤ-elim : ∀ x → P x
ℤ-elim (x - y) = point* x y
ℤ-elim (quot p i) = quot* p i
ℤ-elim (trunc p q i j) = trunc* (cong ℤ-elim p) (cong ℤ-elim q) i j
等供参考，_+_的完整实现使用ℤ-elim:
_+_ : ℤ → ℤ → ℤ
_+_ = ℤ-elim
(λ x y → ℤ-elim
(λ a b → (x +̂ a) - (y +̂ b))
(λ eq₂ → quot (inner-lemma x y eq₂))
trunc)
(λ {x} {y} {x′} {y′} eq₁ i → ℤ-elim
(λ a b → quot (outer-lemma x y eq₁) i)
(λ {a} {b} {a′} {b′} eq₂ j → lemma {x} {y} {x′} {y′} {a} {b} {a′} {b′} eq₁ eq₂ i j )
trunc)
(λ {_} {_} {_} {_} {x+} {y+} eq₁ eq₂ i →
funExt λ a → λ j → trunc {x+ a} {y+ a} (ap eq₁ a) (ap eq₂ a) i j)
where
lemma : ∀ {x y x′ y′ a b a′ b′} → Same x y x′ y′ → Same a b a′ b′ → I → I → ℤ
lemma {x} {y} {x′} {y′} {a} {b} {a′} {b′} eq₁ eq₂ i j = surface i j
where
{-
p Xᵢ
X ---------+---> X′
p₀ i
A X+A --------\---> X′+A
| | |
q| q₀ | | qᵢ
| | |
Aⱼ + j+ [+] <--- This is where we want to get to!
| | |
V V p₁ |
A′ X+A′ -------/---> X′+A′
i
-}
X = x - y
X′ = x′ - y′
A = a - b
A′ = a′ - b′
X+A = (x +̂ a) - (y +̂ b)
X′+A = (x′ +̂ a) - (y′ +̂ b)
X+A′ = (x +̂ a′) - (y +̂ b′)
X′+A′ = (x′ +̂ a′) - (y′ +̂ b′)
p : X ≡ X′
p = quot eq₁
q : A ≡ A′
q = quot eq₂
p₀ : X+A ≡ X′+A
p₀ = quot (outer-lemma x y eq₁)
p₁ : X+A′ ≡ X′+A′
p₁ = quot (outer-lemma x y eq₁)
q₀ : X+A ≡ X+A′
q₀ = quot (inner-lemma x y eq₂)
q₁ : X′+A ≡ X′+A′
q₁ = quot (inner-lemma x′ y′ eq₂)
qᵢ : ∀ i → p₀ i ≡ p₁ i
qᵢ = slidingLid p₀ p₁ q₀
left : qᵢ i0 ≡ q₀
left = refl
right : qᵢ i1 ≡ q₁
right = trunc (qᵢ i1) q₁
surface : PathP (λ i → p₀ i ≡ p₁ i) q₀ q₁
surface i = comp (λ j → p₀ i ≡ p₁ i)
(λ { j (i = i0) → left j
; j (i = i1) → right j
})
(inc (qᵢ i))