在立方模式下定义非一元函数

Question

我想在Cubical模式下定义一个带有两个更高归纳类型的参数的函数。我将cubical软件包用作“前奏”库。

我首先将整数的商类型定义为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)   ?

我现在尝试_+_使用模式匹配进行定义，但是我不知道如何处理“面部中心点”。

_+_ : ? ? ? ? ?
(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?)

我正在使用此结构q?通过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))

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

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?，即，仍然可能存在，并且O在q? i1和之间有一个孔q?：

                 p?
      X+A ------------> X?+A
       |               /|
    q? |              / | q?
       |             |  |
       |             | O|
       |              \ |
       V         p?    \|
      X+A? -----------> X?+A?

直觉上是有道理的，因为它q?是关于自然数的一些代数陈述，并且q? i1是关于不同自然数的不同代数陈述的连续变形版本，因此两者之间仍然必须建立某种联系；但我不知道从何处开始建立该连接（即，明确构建q? i1和之间的2路径q?）

Answer 1

原来真的是之间的孔的可能性q? i1，并q?与形式化我一直在努力做的事。当我回到HoTT 书中尝试更抽象地解决所有商类型的问题时，我想到了这个解决方案，而不仅仅是这个特定的?类型。引自第 6.10 节：

我们也可以直接描述这一点，因为由

• 一个函数q : A ? A/R；

• 对于每个a, b : A这样的R(a, b)，一个等式q(a) = q(b)；和

• 0 截断构造函数：对于所有x, y : A/R和r,s : x = y，我们有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）没有进一步的问题。一个小问题是尝试使用模式匹配会导致一些奇怪的“函数不是纤维状”错误，所以我最终通过了以下显式消除器：

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

因此作为参考，_+_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))