{-# OPTIONS --cubical #-}

open import Agda.Builtin.Sigma using (Σ; _,_; fst; snd)

open import Cubical.Foundations.Prelude using (Type; ℓ-zero; _≡_; isProp→PathP; isPropIsProp)
open import Cubical.Foundations.HLevels using (hProp; isSet→SquareP; isSetHProp)

import Cubical.Data.Int.Base as ℤ using (_·_)
open import Cubical.Data.Int.Base using (ℤ)
import Cubical.Data.Int.Order as ℤ using (_<_; isProp<)
open import Cubical.Data.NatPlusOne using (ℕ₊₁)
open import Cubical.Data.Rationals.Base using (ℕ₊₁→ℤ; [_]; eq/; _∼_)
open import Cubical.Data.Rationals.Base using (ℚ; fromNat)
open import Cubical.Data.Sigma using (_×_)

open import Cubical.HITs.SetQuotients using (squash/)

postulate
  ANY : ∀{ℓ} {A : Type ℓ} → A

infix 4 _<'_

postulate
  lemma< : ((a , b) (c , d) (e , f) : (ℤ × ℕ₊₁))
        → (c ℤ.· ℕ₊₁→ℤ f ) ≡ (e ℤ.· ℕ₊₁→ℤ d)
        → ((a ℤ.· ℕ₊₁→ℤ d) ℤ.< (c ℤ.· ℕ₊₁→ℤ b))
        ≡ ((a ℤ.· ℕ₊₁→ℤ f) ℤ.< (e ℤ.· ℕ₊₁→ℤ b))

-- Internal error disappears if I make fun₀ a postulate
fun₀ : ℤ × ℕ₊₁ → ℚ → hProp ℓ-zero
fun₀ (a , b) [ c , d ] .fst = a ℤ.· ℕ₊₁→ℤ d ℤ.< c ℤ.· ℕ₊₁→ℤ b
fun₀ _       [ _ ]     .snd = ℤ.isProp<
fun₀ a/b (eq/ c/d e/f cf≡ed i) = record
  { fst = lemma< a/b c/d e/f cf≡ed i
  ; snd = isProp→PathP (λ i → isPropIsProp {A = lemma< a/b c/d e/f cf≡ed i}) ℤ.isProp< ℤ.isProp< i
  }
fun₀ a/b (squash/ x y p q i j) =
  isSet→SquareP (λ _ _ → isSetHProp)
    (λ _ → fun₀ a/b x)
    (λ _ → fun₀ a/b y)
    (λ i → fun₀ a/b (p i))
    (λ i → fun₀ a/b (q i)) j i

postulate
  toPath : ∀ a/b c/d (x : a/b ∼ c/d) (y : ℚ) → fun₀ a/b y ≡ fun₀ c/d y

_<'_ : ℚ → ℚ → hProp ℓ-zero
_<'_ [ a/b ] y = fun₀ a/b y
_<'_ (eq/ a/b c/d ad≡cb i) y = toPath a/b c/d ad≡cb y i
_<'_ (squash/ x y p q i j) z =
  isSet→SquareP (λ _ _ → isSetHProp)
    (λ _ → x <' z) (λ _ → y <' z) (λ i → p i <' z) (λ i → q i <' z) j i

test : Σ ℚ (λ q → fst (0 <' q)) → Type
test (q , q+) = {!q!} -- C-c C-c case split on q

-- __IMPOSSIBLE__ at Agda/TypeChecking/Substitute.hs:139:33