在立方模式下定义非一元函数 [英] Defining non-unary functions in Cubical mode

问题描述

我想在Cubical模式下定义一个具有两个更高归纳类型的参数的函数.我使用 cubical包作为我的前奏"库.

I'd like to define a function with two, higher inductive typed, arguments in Cubical mode. I am using the cubical package as my "prelude" library.

我首先将整数的商类型定义为HIT:

I first define a quotient type for integers as a 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′)

然后我可以使用模式匹配来定义一元函数:

I can then define a unary function using pattern matching:

_+1 : ℤ → ℤ
(x - y) +1 = suc x - y
quot {x} {y} prf i +1 = quot {suc x} {y} (cong suc prf) i

到目前为止，太好了.但是，如果我想定义一个二进制函数(例如加法)怎么办?

So far, so good. But what if I want to define a binary function, such as addition?

首先，让我们摆脱无聊的算术证明:

First, let's get the boring arithmetic proofs out of the way:

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)   ∎

我现在尝试使用模式匹配来定义_+_，但是我不知道如何处理面部中心点"，可以这么说:

I now try to define _+_ using pattern matching, but I have no idea how to handle the "points in the center of the face", so to speak:

_+_ : ℤ → ℤ → ℤ
(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 = ?

所以基本上我有以下情况:

So basically what I have is the following situation:

                 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₂)

我正在使用此结构将q₀水平推出i:

I am using this construction to push out q₀ horizontally by i:

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))

并使用它，我对+的尝试如下:

and using this, my attempt at + is as follows:

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

但这失败，并出现以下类型错误:

But this fails with the following type error:

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 ℤ

一个提示可能是出问题的是，尽管这三个方面都退化得很好:

One hint to what might be going wrong is that while these three sides degenerate nicely:

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:

I guess because qᵢ is pulled from the left side, so there could still be a hole between the right side and the pushed-all-the-way qᵢ, i.e. this would still be possible, with a hole at O between qᵢ i1 and q₁:

                 p₀
      X+A ------------> X′+A
       |               /|
    q₀ |              / | q₁
       |             |  |
       |             | O|
       |              \ |
       V         p₁    \|
      X+A′ -----------> X′+A′

并直观地讲得通，因为q₁是关于自然数的一些代数陈述，而qᵢ i1是关于不同自然数的不同代数陈述的连续变形版本，因此仍然必须存在某种联系两者之间但我不知道从哪里开始建立该连接(即在qᵢ i1和q₁之间明确构造2路径)

and intiutively it makes sense, because q₁ is some algebraic statement about natural numbers, and qᵢ i1 is a continuously deformed version of a different algebraic statement about different natural numbers, so there still has to be some kind of connection made between the two; but I don't know where to start on making that connection (i.e. constructing explicitly the 2-path between qᵢ i1 and q₁)

推荐答案

事实证明，确实在我已经进行过的形式化过程中，qᵢ i1和q₁之间确实存在漏洞试图做.当我回到 HoTT书来尝试针对所有商类型更抽象地解决此问题时，而不仅仅是这种特定的ℤ类型.引用第6.10节:

It turns out there really was a possibility of a hole between qᵢ i1 and q₁ with the formalization I've been trying to do. The solution hit me when I went back to the HoTT book to try and solve this more abstractly for all quotient types, not just this particular ℤ type. To quote from section 6.10:

我们也可以直接描述为高感性A/R型 由

We can also describe this directly, as the higher inductive type A/R generated by

• 函数q : A → A/R;

对于每个a, b : A，例如R(a, b)，等于q(a) = q(b)；和

For each a, b : A such that R(a, b), an equality q(a) = q(b); and

0截断构造函数:对于所有x, y : A/R和r,s : x = y，我们都有r = s.

The 0-truncation constructor: for all x, y : A/R and r,s : x = y, we have r = s.

所以我所缺少的是第三点:缺少高级类型的结构是需要明确建模的东西.

So what I was missing was that third point: that the lack of higher-typed structure is something that needs to be explicitly modeled.

使用此信息，我在ℤ中添加了第三个构造函数:

Using this information, I have added a third constructor to my ℤ:

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)，而没有其他问题.一个小小的毛病是，尝试使用模式匹配会导致一些奇怪的功能不健全"错误，因此我最终通过以下显式消除器进行了操作:

This allowed me to prove right (and thus, surface) with no further issues. One slight hiccup is that trying to use pattern matching caused some weird "function is not fibrant" errors, so I ended up going via the following explicit eliminator:

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完全实现_+_:

and so for reference, the full implementation of _+_ using ℤ-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))

这篇关于在立方模式下定义非一元函数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！