Defining non-unary functions in Cubical mode











up vote
3
down vote

favorite
1












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.



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


with



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


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


the rightmost side doesn't:



right : qᵢ i1 ≡ q₁
right = ? -- refl fails here


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′


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










share|improve this question
























  • A note on readability, qᵢ and q₁ look very much alike, I mistook it for some kind of typo at first when I saw them in the expression qᵢ i1 ≡ q₁
    – Potato44
    Nov 9 at 18:11

















up vote
3
down vote

favorite
1












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.



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


with



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


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


the rightmost side doesn't:



right : qᵢ i1 ≡ q₁
right = ? -- refl fails here


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′


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










share|improve this question
























  • A note on readability, qᵢ and q₁ look very much alike, I mistook it for some kind of typo at first when I saw them in the expression qᵢ i1 ≡ q₁
    – Potato44
    Nov 9 at 18:11















up vote
3
down vote

favorite
1









up vote
3
down vote

favorite
1






1





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.



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


with



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


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


the rightmost side doesn't:



right : qᵢ i1 ≡ q₁
right = ? -- refl fails here


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′


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










share|improve this question















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.



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


with



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


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


the rightmost side doesn't:



right : qᵢ i1 ≡ q₁
right = ? -- refl fails here


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′


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







agda topology cubical-type-theory homotopy-type-theory






share|improve this question















share|improve this question













share|improve this question




share|improve this question








edited Nov 10 at 3:06

























asked Nov 4 at 13:38









Cactus

18.5k847109




18.5k847109












  • A note on readability, qᵢ and q₁ look very much alike, I mistook it for some kind of typo at first when I saw them in the expression qᵢ i1 ≡ q₁
    – Potato44
    Nov 9 at 18:11




















  • A note on readability, qᵢ and q₁ look very much alike, I mistook it for some kind of typo at first when I saw them in the expression qᵢ i1 ≡ q₁
    – Potato44
    Nov 9 at 18:11


















A note on readability, qᵢ and q₁ look very much alike, I mistook it for some kind of typo at first when I saw them in the expression qᵢ i1 ≡ q₁
– Potato44
Nov 9 at 18:11






A note on readability, qᵢ and q₁ look very much alike, I mistook it for some kind of typo at first when I saw them in the expression qᵢ i1 ≡ q₁
– Potato44
Nov 9 at 18:11














2 Answers
2






active

oldest

votes

















up vote
2
down vote



accepted










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:




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




  • A function q : A → A/R;


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


  • 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


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


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





share|improve this answer




























    up vote
    0
    down vote













    This is a partial answer, in the hope that it will lure someone into solving the next piece of this puzzle.



    So, I managed to prove right, and with it, that there is a continuous surface from left to right :



    right : qᵢ i1 ≡ q₁
    right i = comp
    (λ j → p j + A ≡ p j + A′)
    (λ { j (i = i0) → qᵢ j
    ; j (i = i1) → cong (λ ξ → quot {x} {y} {x′} {y′} eq₁ j + ξ) q
    }
    (inc (left i))

    surface : PathP (λ i → p₀ i ≡ p₁ i) q₀ q₁
    surface i = comp (λ j → p₀ i ≡ p₁ i)
    (λ { j (i = i0) → q₀
    ; j (i = i1) → right j
    })
    (inc (qᵢ i))

    Xᵢ+Aⱼ = surface i j


    This definition of Xᵢ+Aⱼ passes the typechecker, but fails during termination checking. Basically, all occurrences of _+_ are marked as problematic; in particular, the ones in the definition of right: both the p j + A and p j + A′ calls, and the congruence function in cong (λ ξ → quot {x} {y} {x′} {y′} eq₁ j + ξ) q.



    The first two don't make much sense to me: I have already defined _+- for the midpoint+point and the point+point cases, and the second argument in p j + A and p j + A′ are clearly points.



    The third one, I am looking for suggestions on.






    share|improve this answer





















      Your Answer






      StackExchange.ifUsing("editor", function () {
      StackExchange.using("externalEditor", function () {
      StackExchange.using("snippets", function () {
      StackExchange.snippets.init();
      });
      });
      }, "code-snippets");

      StackExchange.ready(function() {
      var channelOptions = {
      tags: "".split(" "),
      id: "1"
      };
      initTagRenderer("".split(" "), "".split(" "), channelOptions);

      StackExchange.using("externalEditor", function() {
      // Have to fire editor after snippets, if snippets enabled
      if (StackExchange.settings.snippets.snippetsEnabled) {
      StackExchange.using("snippets", function() {
      createEditor();
      });
      }
      else {
      createEditor();
      }
      });

      function createEditor() {
      StackExchange.prepareEditor({
      heartbeatType: 'answer',
      convertImagesToLinks: true,
      noModals: true,
      showLowRepImageUploadWarning: true,
      reputationToPostImages: 10,
      bindNavPrevention: true,
      postfix: "",
      imageUploader: {
      brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
      contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
      allowUrls: true
      },
      onDemand: true,
      discardSelector: ".discard-answer"
      ,immediatelyShowMarkdownHelp:true
      });


      }
      });














       

      draft saved


      draft discarded


















      StackExchange.ready(
      function () {
      StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53141417%2fdefining-non-unary-functions-in-cubical-mode%23new-answer', 'question_page');
      }
      );

      Post as a guest















      Required, but never shown

























      2 Answers
      2






      active

      oldest

      votes








      2 Answers
      2






      active

      oldest

      votes









      active

      oldest

      votes






      active

      oldest

      votes








      up vote
      2
      down vote



      accepted










      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:




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




      • A function q : A → A/R;


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


      • 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


      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


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





      share|improve this answer

























        up vote
        2
        down vote



        accepted










        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:




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




        • A function q : A → A/R;


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


        • 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


        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


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





        share|improve this answer























          up vote
          2
          down vote



          accepted







          up vote
          2
          down vote



          accepted






          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:




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




          • A function q : A → A/R;


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


          • 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


          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


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





          share|improve this answer












          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:




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




          • A function q : A → A/R;


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


          • 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


          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


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






          share|improve this answer












          share|improve this answer



          share|improve this answer










          answered Nov 11 at 7:44









          Cactus

          18.5k847109




          18.5k847109
























              up vote
              0
              down vote













              This is a partial answer, in the hope that it will lure someone into solving the next piece of this puzzle.



              So, I managed to prove right, and with it, that there is a continuous surface from left to right :



              right : qᵢ i1 ≡ q₁
              right i = comp
              (λ j → p j + A ≡ p j + A′)
              (λ { j (i = i0) → qᵢ j
              ; j (i = i1) → cong (λ ξ → quot {x} {y} {x′} {y′} eq₁ j + ξ) q
              }
              (inc (left i))

              surface : PathP (λ i → p₀ i ≡ p₁ i) q₀ q₁
              surface i = comp (λ j → p₀ i ≡ p₁ i)
              (λ { j (i = i0) → q₀
              ; j (i = i1) → right j
              })
              (inc (qᵢ i))

              Xᵢ+Aⱼ = surface i j


              This definition of Xᵢ+Aⱼ passes the typechecker, but fails during termination checking. Basically, all occurrences of _+_ are marked as problematic; in particular, the ones in the definition of right: both the p j + A and p j + A′ calls, and the congruence function in cong (λ ξ → quot {x} {y} {x′} {y′} eq₁ j + ξ) q.



              The first two don't make much sense to me: I have already defined _+- for the midpoint+point and the point+point cases, and the second argument in p j + A and p j + A′ are clearly points.



              The third one, I am looking for suggestions on.






              share|improve this answer

























                up vote
                0
                down vote













                This is a partial answer, in the hope that it will lure someone into solving the next piece of this puzzle.



                So, I managed to prove right, and with it, that there is a continuous surface from left to right :



                right : qᵢ i1 ≡ q₁
                right i = comp
                (λ j → p j + A ≡ p j + A′)
                (λ { j (i = i0) → qᵢ j
                ; j (i = i1) → cong (λ ξ → quot {x} {y} {x′} {y′} eq₁ j + ξ) q
                }
                (inc (left i))

                surface : PathP (λ i → p₀ i ≡ p₁ i) q₀ q₁
                surface i = comp (λ j → p₀ i ≡ p₁ i)
                (λ { j (i = i0) → q₀
                ; j (i = i1) → right j
                })
                (inc (qᵢ i))

                Xᵢ+Aⱼ = surface i j


                This definition of Xᵢ+Aⱼ passes the typechecker, but fails during termination checking. Basically, all occurrences of _+_ are marked as problematic; in particular, the ones in the definition of right: both the p j + A and p j + A′ calls, and the congruence function in cong (λ ξ → quot {x} {y} {x′} {y′} eq₁ j + ξ) q.



                The first two don't make much sense to me: I have already defined _+- for the midpoint+point and the point+point cases, and the second argument in p j + A and p j + A′ are clearly points.



                The third one, I am looking for suggestions on.






                share|improve this answer























                  up vote
                  0
                  down vote










                  up vote
                  0
                  down vote









                  This is a partial answer, in the hope that it will lure someone into solving the next piece of this puzzle.



                  So, I managed to prove right, and with it, that there is a continuous surface from left to right :



                  right : qᵢ i1 ≡ q₁
                  right i = comp
                  (λ j → p j + A ≡ p j + A′)
                  (λ { j (i = i0) → qᵢ j
                  ; j (i = i1) → cong (λ ξ → quot {x} {y} {x′} {y′} eq₁ j + ξ) q
                  }
                  (inc (left i))

                  surface : PathP (λ i → p₀ i ≡ p₁ i) q₀ q₁
                  surface i = comp (λ j → p₀ i ≡ p₁ i)
                  (λ { j (i = i0) → q₀
                  ; j (i = i1) → right j
                  })
                  (inc (qᵢ i))

                  Xᵢ+Aⱼ = surface i j


                  This definition of Xᵢ+Aⱼ passes the typechecker, but fails during termination checking. Basically, all occurrences of _+_ are marked as problematic; in particular, the ones in the definition of right: both the p j + A and p j + A′ calls, and the congruence function in cong (λ ξ → quot {x} {y} {x′} {y′} eq₁ j + ξ) q.



                  The first two don't make much sense to me: I have already defined _+- for the midpoint+point and the point+point cases, and the second argument in p j + A and p j + A′ are clearly points.



                  The third one, I am looking for suggestions on.






                  share|improve this answer












                  This is a partial answer, in the hope that it will lure someone into solving the next piece of this puzzle.



                  So, I managed to prove right, and with it, that there is a continuous surface from left to right :



                  right : qᵢ i1 ≡ q₁
                  right i = comp
                  (λ j → p j + A ≡ p j + A′)
                  (λ { j (i = i0) → qᵢ j
                  ; j (i = i1) → cong (λ ξ → quot {x} {y} {x′} {y′} eq₁ j + ξ) q
                  }
                  (inc (left i))

                  surface : PathP (λ i → p₀ i ≡ p₁ i) q₀ q₁
                  surface i = comp (λ j → p₀ i ≡ p₁ i)
                  (λ { j (i = i0) → q₀
                  ; j (i = i1) → right j
                  })
                  (inc (qᵢ i))

                  Xᵢ+Aⱼ = surface i j


                  This definition of Xᵢ+Aⱼ passes the typechecker, but fails during termination checking. Basically, all occurrences of _+_ are marked as problematic; in particular, the ones in the definition of right: both the p j + A and p j + A′ calls, and the congruence function in cong (λ ξ → quot {x} {y} {x′} {y′} eq₁ j + ξ) q.



                  The first two don't make much sense to me: I have already defined _+- for the midpoint+point and the point+point cases, and the second argument in p j + A and p j + A′ are clearly points.



                  The third one, I am looking for suggestions on.







                  share|improve this answer












                  share|improve this answer



                  share|improve this answer










                  answered Nov 8 at 13:18









                  Cactus

                  18.5k847109




                  18.5k847109






























                       

                      draft saved


                      draft discarded



















































                       


                      draft saved


                      draft discarded














                      StackExchange.ready(
                      function () {
                      StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53141417%2fdefining-non-unary-functions-in-cubical-mode%23new-answer', 'question_page');
                      }
                      );

                      Post as a guest















                      Required, but never shown





















































                      Required, but never shown














                      Required, but never shown












                      Required, but never shown







                      Required, but never shown

































                      Required, but never shown














                      Required, but never shown












                      Required, but never shown







                      Required, but never shown







                      Popular posts from this blog

                      Guess what letter conforming each word

                      Port of Spain

                      Run scheduled task as local user group (not BUILTIN)