title: Defining non-unary functions in Cubical mode
body: <p>I'd like to define a function with two, higher inductive typed, arguments in Cubical mode. I am using <a href="https://github.com/agda/cubical" rel="noreferrer">the <code>cubical</code> package</a> as my "prelude" library.</p>
  
  <p>I first define a quotient type for integers as a HIT:</p>
  
  <pre><code>{-# 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′)
  </code></pre>
  
  <p>I can then define a unary function using pattern matching:</p>
  
  <pre><code>_+1 : ℤ → ℤ
  (x - y) +1 = suc x - y
  quot {x} {y} prf i +1 = quot {suc x} {y} (cong suc prf) i
  </code></pre>
  
  <p>So far, so good. But what if I want to define a binary function, such as addition?</p>
  
  <p>First, let's get the boring arithmetic proofs out of the way:</p>
  
  <pre><code>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)   ∎
  </code></pre>
  
  <p>I now try to define <code>_+_</code> using pattern matching, but I have no idea how to handle the "points in the center of the face", so to speak:</p>
  
  <pre><code>_+_ : ℤ → ℤ → ℤ
  (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 = ?
  </code></pre>
  
  <p>So basically what I have is the following situation:</p>
  
  <pre><code>                 p   Xᵢ
           X  ---------+---&gt; X′
  
                   p₀  i
     A     X+A --------\---&gt; X′+A
     |     |           |
    q|  q₀ |           | qᵢ
     |     |           |
  Aⱼ +    j+          [+]  &lt;--- This is where we want to get to!
     |     |           |
     V     V       p₁  |
     A′    X+A′ -------/---&gt; X′+A′
                       i
  </code></pre>
  
  <p>with</p>
  
  <pre><code>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₂)
  </code></pre>
  
  <p>I am using <a href="https://stackoverflow.com/a/53199767/477476">this construction</a> to push out <code>q₀</code> horizontally by <code>i</code>:</p>
  
  <pre><code>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))
  </code></pre>
  
  <p>and using this, my attempt at <code>+</code> is as follows:</p>
  
  <pre><code>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
  </code></pre>
  
  <p>But this fails with the following type error:</p>
  
  <blockquote>
  <pre><code>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 ℤ
  </code></pre>
  </blockquote>
  
  <p>One hint to what might be going wrong is that while these three sides degenerate nicely:</p>
  
  <pre><code>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
  </code></pre>
  
  <p>the rightmost side doesn't:</p>
  
  <pre><code>right : qᵢ i1 ≡ q₁
  right = ? -- refl fails here
  </code></pre>
  
  <p>I guess because <code>qᵢ</code> is pulled from the left side, so there could still be a hole between the right side and the pushed-all-the-way <code>qᵢ</code>, i.e. this would still be possible, with a hole at <code>O</code> between <code>qᵢ i1</code> and <code>q₁</code>:</p>
  
  <pre><code>                 p₀
        X+A ------------&gt; X′+A
         |               /|
      q₀ |              / | q₁
         |             |  |
         |             | O|
         |              \ |
         V         p₁    \|
        X+A′ -----------&gt; X′+A′
  </code></pre>
  
  <p>and intiutively it makes sense, because <code>q₁</code> is some algebraic statement about natural numbers, and <code>qᵢ i1</code> 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 <code>qᵢ i1</code> and <code>q₁</code>) </p>