Sign for integers and rationals about cubical HOT 10 CLOSED

data Sign : Set where
  pos neg zero : Sign

data ℤ-has-sign : Sign → ℤ → Set where
  ℤ-pos : ∀ n → ℤ-has-sign pos (pos (suc n))
  ℤ-zero : ℤ-has-sign zero (pos zero)
  ℤ-neg : ∀ n → ℤ-has-sign neg (neg (suc n))

ℤ₊ : Set
ℤ₊ = Σ ℤ (ℤ-has-sign pos)

ℤ₋ : Set
ℤ₋ = Σ ℤ (ℤ-has-sign neg)

sign-ℤ : (z : ℤ) → Σ[ s ∈ Sign ] (ℤ-has-sign s z)
sign-ℤ (pos zero) = zero , ℤ-zero
sign-ℤ (pos (suc n)) = pos , ℤ-pos n
sign-ℤ (neg zero) = zero , subst (ℤ-has-sign zero) posneg ℤ-zero
sign-ℤ (neg (suc n)) = neg , ℤ-neg n
sign-ℤ (posneg i) = zero , {!!} -- no idea

data ℚ-has-sign : Sign → ℚ → Set where
  ℚ-pos₁ : ∀ {u a x} → ℤ-has-sign pos u → ℤ-has-sign pos a → ℚ-has-sign pos (con u a x)
  ℚ-pos₂ : ∀ {u a x} → ℤ-has-sign neg u → ℤ-has-sign neg a → ℚ-has-sign pos (con u a x)
  ℚ-zero : ∀ {u a x} → ℤ-has-sign zero u → ℚ-has-sign zero (con u a x)
  ℚ-neg₁ : ∀ {u a x} → ℤ-has-sign pos u → ℤ-has-sign neg a → ℚ-has-sign neg (con u a x)
  ℚ-neg₂ : ∀ {u a x} → ℤ-has-sign neg u → ℤ-has-sign pos a → ℚ-has-sign neg (con u a x)

ℚ₊ : Set
ℚ₊ = Σ ℚ (ℚ-has-sign pos)

ℚ₋ : Set
ℚ₋ = Σ ℚ (ℚ-has-sign neg)

sign-ℚ : (q : ℚ) → Σ[ s ∈ Sign ] (ℚ-has-sign s q)
sign-ℚ (con u a x) = case sign-ℤ u , sign-ℤ a of λ
  { ((pos , u-pos) , pos , a-pos) → pos , ℚ-pos₁ u-pos a-pos
  ; ((pos , u-pos) , neg , a-neg) → neg , ℚ-neg₁ u-pos a-neg
  ; ((pos , u-pos) , zero , ℤ-zero) → ⊥-elim (x refl)
  ; ((neg , u-neg) , pos , a-pos) → neg , ℚ-neg₂ u-neg a-pos
  ; ((neg , u-neg) , neg , a-neg) → pos , ℚ-pos₂ u-neg a-neg
  ; ((neg , u-neg) , zero , ℤ-zero) → ⊥-elim (x refl)
  ; ((zero , u-zero) , _) → zero , ℚ-zero u-zero
  }
sign-ℚ (path u a v b x i) = {!!} -- no idea
sign-ℚ (trunc q q₁ x y i i₁) = {!!} -- no idea

_*S_ : Sign → Sign → Sign
pos *S x = x
x *S pos = x
neg *S neg = pos
_  *S zero = zero
zero *S x = zero

isSetSign : isSet Sign
isSetSign = { }0
-- should have a proof similar to the one for Bool

lemma0 : ∀ u a → sign-ℤ (u *ℤ a) ≡ sign-ℤ u *S sign-ℤ a

-- probably want some other lemmas to finish this proof.
lemma : ∀ u a v b → u *S b ≡ v *S a → u *S a ≡ v *S b
lemma pos a pos b eq = sym eq
lemma pos a neg b eq = { }1
lemma pos a zero b eq = { }2
lemma neg a pos b eq = { }3
lemma neg a neg b eq = sym eq
lemma neg a zero b eq = { }4
lemma zero a pos b eq = { }5
lemma zero a neg b eq = { }6
lemma zero a zero b eq = sym eq

sign-ℚ : ℚ → Sign
sign-ℚ (con u a x) = sign-ℤ u *S sign-ℤ a
sign-ℚ (path u a v b x i) = lemma (sign-ℤ u) (sign-ℤ a) (sign-ℤ v) (sign-ℤ b)
                                  (sym (lemma0 u b) ∙ cong sign-ℤ x ∙ lemma0 v a) i
sign-ℚ (trunc q q₁ x y i i₁) = isSetSign (sign-ℚ q) (sign-ℚ q₁) (cong sign-ℚ x) (cong sign-ℚ y) i i₁