Agda中证明自由回路的依赖递归性质蕴含圆的泛性质

背景 #

我正依据HoTT书籍第6章定义圆𝕊¹的归纳原理并证明其相关性质。核心难点在于HoTT用判断相等定义递归/归纳原理，这无法在Agda中表述，因此参考unimath采用**自由回路（free-loop）**来定义圆𝕊¹的递归/归纳原理，但在证明目标命题时陷入困境。

目标命题 #

需要证明的命题如下（含义：若ev-free-loop-∏是截面，则它同时也是收缩）：

free-loop-∏-induction→universal-property-circle : ∀ {n m : Level} {X : Set n} {A : Set m}
                                                 → (S : free-loop X)
                                                 → (∀ P → free-loop-∏-induction {n} {m} {X} S P)
                                                 → universal-property-circle {n} {m} {X} {A}

相关定义 #

用到的核心定义：

free-loop : ∀ {n : Level} → Set n → Set n
free-loop X = Σ[ x ∈ X ] (x ≡ x)

free-dependent-loop : ∀ {n m : Level} {X : Set n} → free-loop X → (X → Set m) → Set m
free-dependent-loop ⟨ x , l ⟩ P = Σ[ a ∈ P x ] (transport l P a ≡ a)

ev-free-loop-∏ : ∀ {n m : Level} {X : Set n} 
                → (S : free-loop X)
                → (P : X → Set m) 
                → (∀ (x : X) → P x) → free-dependent-loop S P
ev-free-loop-∏ ⟨ b , l ⟩ P h = ⟨ h b , congd h l ⟩

free-loop-∏-induction : ∀ {n m : Level} {X : Set n} (S : free-loop X) (P : X → Set m) → Set (n ⊔ m)
free-loop-∏-induction S P = section (ev-free-loop-∏ S P)

universal-property-circle : ∀ {n m : Level} {X : Set n} {A : Set m} → Set (n ⊔ m)
universal-property-circle {_} {_} {X} {A} = (X → A) ≃ (Σ[ a ∈ A ] a ≡ a)

不完整的证明草稿 #

目前写出的不完整证明如下，其中包含多个未验证的公设：

free-loop-∏-induction→universal-property-circle {_} {_} {X} {A} ⟨ b , l ⟩ φ
    = ⟨ f , ⟨ ⟨ g , f∘g∼id ⟩ , ⟨ g , g∘f∼id ⟩ ⟩ ⟩ where
        postulate ∏-induction→induction : ∀ {n m : Level} {X : Set n} {A : Set m}
                                        → (S : free-loop X)
                                        → (∀ P → free-loop-∏-induction {n} {m} {X} S P)
                                        → free-loop-induction {n} {m} {X} {A} S
        S = ⟨ b , l ⟩
        φ' = (∏-recursion→recursion S φ)
        f = ev-free-loop S
        g : (Σ[ a ∈ A ] a ≡ a) → (X → A)
        g = proj₁ φ'
        f∘g∼id : (f ∘ g) ∼ id
        f∘g∼id t = proj₂ φ' t
        g∘f∼id : (g ∘ f) ∼ id
        g∘f∼id h = funext (g (f h)) h ξ where
          ε : ∀ h → g (f h) b ≡ h b
          ε h = cong proj₁ ( proj₂ φ' (f h))
          postulate μ : transport (ε h) (λ z → z ≡ z) (cong (g (f h)) l) ≡ cong h l          
          ξ : ∀ (x : X) → g (f h) x ≡ h x
          ξ = unicity-circle-∏ {_} {_} {X} {A} S φ (g (f h)) h (ε h) μ

待解决问题 #

1. 依赖自由回路归纳（free-loop-∏-induction）是否蕴含自由回路归纳（free-loop-induction）？
2. 公设μ是否成立？
3. 如何补全完整的证明，消除这些未验证的公设？

内容的提问来源于stack exchange，提问作者Werner Germán Busch