相关疑难解决方法(0)

我想在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} …