Todd Waugh Ambridge, January 2024

# Ternary Boehm encodings of real numbers

\begin{code}
{-# OPTIONS --without-K --safe #-}

open import Integers.Addition renaming (_+_ to _β„€+_;  _-_ to _β„€-_)
open import Integers.Negation renaming (-_ to β„€-_ )
open import Integers.Order
open import Integers.Type
open import MLTT.Spartan
open import Notation.Order
open import UF.FunExt
open import UF.Powerset hiding (𝕋)
open import UF.PropTrunc
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.SubtypeClassifier

open import TWA.Thesis.Chapter5.BoehmStructure
 hiding (downLeft; downMid; downRight; upRight; upLeft; _below_)
open import TWA.Thesis.AndrewSneap.DyadicRationals
 renaming (normalise to ΞΉ)
open import TWA.Thesis.Chapter5.Integers
open import TWA.Thesis.Chapter5.SignedDigit

module TWA.Thesis.Chapter5.BoehmVerification
  (pt : propositional-truncations-exist)
  (fe : FunExt)
  (pe : PropExt)
  (dy : Dyadics)
  where

open PropositionalTruncation pt
open Dyadics dy
  renaming ( _β„€[1/2]+_ to _+𝔻_ ; β„€[1/2]-_ to -_ ; _β„€[1/2]-_ to _-_
           ; _β„€[1/2]*_ to _*_ )

open import TWA.Thesis.AndrewSneap.DyadicReals pe pt fe dy
open import TWA.Thesis.Chapter3.ClosenessSpaces fe hiding (⟨_⟩ ; ι)
open import TWA.Thesis.Chapter3.ClosenessSpaces-Examples fe
\end{code}

## Structural operations and properties

\begin{code}
downLeft downMid downRight : β„€ β†’ β„€
downLeft  k = (k β„€+ k)
downMid   k = (k β„€+ k) +pos 1
downRight k = (k β„€+ k) +pos 2

upRight upLeft : β„€ β†’ β„€
upRight k = sign k (num k /2)
upLeft  k = upRight (predβ„€ k)

_below_ : β„€ β†’ β„€ β†’ 𝓀₀ Μ‡
a below b = downLeft b ≀ a ≀ downRight b

ternary : (β„€ β†’ β„€) β†’ 𝓀₀  Μ‡
ternary x = (Ξ΄ : β„€) β†’ x (succβ„€ Ξ΄) below x Ξ΄

𝕋 : 𝓀₀ Μ‡ 
𝕋 = Ξ£ x κž‰ (β„€ β†’ β„€) , ternary x

β„€[1/2]α΄΅ : 𝓀₀ Μ‡
β„€[1/2]α΄΅ = Ξ£ (l , r) κž‰ (β„€[1/2] Γ— β„€[1/2]) , l ≀ r

ld rd : β„€[1/2]α΄΅ β†’ β„€[1/2]
ld ((l , r) , _) = l
rd ((l , r) , _) = r

ld≀rd : (p : β„€[1/2]α΄΅) β†’ ld p ≀ rd p
ld≀rd ((l , r) , l≀r) = l≀r

_covers_ : β„€[1/2]α΄΅ β†’ β„€[1/2]α΄΅ β†’ 𝓀₀ Μ‡
a covers b = (ld a ≀ ld b) Γ— (rd b ≀ rd a)

covers-refl : (ab : β„€[1/2]α΄΅) β†’ ab covers ab
covers-refl ab = ≀-refl (ld ab) , ≀-refl (rd ab)

covers-trans : (a b c : β„€[1/2]α΄΅) β†’ a covers b β†’ b covers c β†’ a covers c
covers-trans a b c (l≀₁ , r≀₁) (l≀₂ , r≀₂)
 = trans' (ld a) (ld b) (ld c) l≀₁ l≀₂
 , trans' (rd c ) (rd b) (rd a) r≀₂ r≀₁

nested positioned : (β„€ β†’ β„€[1/2]α΄΅) β†’ 𝓀₀ Μ‡
nested      ΞΆ = (n : β„€) β†’ (ΞΆ n) covers (ΞΆ (succβ„€ n))
positioned     ΞΆ = (Ο΅ : β„€[1/2]) β†’ is-positive Ο΅
              β†’ Ξ£ n κž‰ β„€ , (rd (ΞΆ n) - ld (ΞΆ n)) ≀ Ο΅

fully-nested' : (β„€ β†’ β„€[1/2]α΄΅) β†’ β„• β†’ 𝓀₀ Μ‡
fully-nested' ΞΆ k = (n : β„€) β†’ (ΞΆ n) covers (ΞΆ (n +pos k))

fully-nested : (β„€ β†’ β„€[1/2]α΄΅) β†’ 𝓀₀ Μ‡
fully-nested ΞΆ = (n m : β„€) β†’ n ≀ m β†’ (ΞΆ n) covers (ΞΆ m)

nested-implies-fully-nested'
 : (ΞΆ : β„€ β†’ β„€[1/2]α΄΅) β†’ nested ΞΆ β†’ Ξ  (fully-nested' ΞΆ)
nested-implies-fully-nested' ΢ ρ 0 n = (0 , refl) , (0 , refl)
nested-implies-fully-nested' ΢ ρ (succ k) n
 = covers-trans (ΞΆ n) (ΞΆ (succβ„€ n)) (ΞΆ (succβ„€ (n +pos k))) (ρ n)
     (nested-implies-fully-nested' (ΞΆ ∘ succβ„€) (ρ ∘ succβ„€) k n)

nested-implies-fully-nested
 : (ΞΆ : β„€ β†’ β„€[1/2]α΄΅) β†’ nested ΞΆ β†’ fully-nested ΞΆ
nested-implies-fully-nested ΢ ρ n m (k , refl)
 = nested-implies-fully-nested' ΢ ρ k n
\end{code}

## Verification of the structure of ternary Boehm encodings

\begin{code}
-- By Andrew Sneap
β¦…_⦆ : (Ο‡ : β„€ β†’ β„€[1/2]α΄΅) β†’ nested Ο‡ β†’ positioned Ο‡ β†’ ℝ-d
β¦…_⦆ Ο‡ Ο„ Ο€ = (L , R)
          , inhabited-l , inhabited-r
          , rounded-l   , rounded-r
          , is-disjoint , is-located
 where
  L R : β„€[1/2] β†’ Ξ© 𝓀₀
  L p = (βˆƒ n κž‰ β„€ , p < ld (Ο‡ n)) , βˆƒ-is-prop
  R q = (βˆƒ n κž‰ β„€ , rd (Ο‡ n) < q) , βˆƒ-is-prop

  
  inhabited-l : inhabited-left L
  inhabited-l = ∣ ld (Ο‡ (pos 0)) - 1β„€[1/2]
              , ∣ (pos 0)
                  , (β„€[1/2]<-neg (ld (Ο‡ (pos 0))) 1β„€[1/2] 0<1β„€[1/2]) ∣ ∣
  
  inhabited-r : inhabited-right R
  inhabited-r = ∣ (rd (Ο‡ (pos 0)) +𝔻 1β„€[1/2])
              , ∣ pos 0
                  , β„€[1/2]<-+ (rd (Ο‡ (pos 0))) 1β„€[1/2] 0<1β„€[1/2] ∣ ∣
  
  rounded-l : rounded-left L
  rounded-l p = ltr , rtl
   where
    ltr : βˆƒ n κž‰ β„€ , (p <β„€[1/2] ld (Ο‡ n))
        β†’ βˆƒ p' κž‰ β„€[1/2] , p < p' Γ— (βˆƒ n' κž‰ β„€ , (p' <β„€[1/2] ld (Ο‡ n')))
    ltr = βˆ₯βˆ₯-functor I
     where
      I : Ξ£ n κž‰ β„€ , (p <β„€[1/2] ld (Ο‡ n))
        β†’ Ξ£ p' κž‰ β„€[1/2] , p < p' Γ— (βˆƒ n' κž‰ β„€ , (p' <β„€[1/2] ld (Ο‡ n')))
      I (n , p<ΞΆn) = let (p' , p<p' , p'<ΞΆn) = dense p (ld (Ο‡ n)) p<ΞΆn
                     in p' , (p<p' , ∣ n , p'<΢n ∣)
    rtl : βˆƒ p' κž‰ β„€[1/2] , p < p' Γ— (βˆƒ n κž‰ β„€ , (p' <β„€[1/2] ld (Ο‡ n)))
        β†’ βˆƒ n κž‰ β„€ , (p <β„€[1/2] ld (Ο‡ n))
    rtl = βˆ₯βˆ₯-rec βˆƒ-is-prop I
     where
      I : Ξ£ p' κž‰ β„€[1/2] , p < p' Γ— (βˆƒ n κž‰ β„€ , (p' <β„€[1/2] ld (Ο‡ n)))
        β†’ βˆƒ n κž‰ β„€ , (p <β„€[1/2] ld (Ο‡ n))
      I (p' , p<p' , te) = βˆ₯βˆ₯-functor II te
       where
        II : Ξ£ n κž‰ β„€ , (p' <β„€[1/2] ld (Ο‡ n))
           β†’ Ξ£ n κž‰ β„€ , (p <β„€[1/2] ld (Ο‡ n))
        II (n  , p'<ΞΆn) = n , (trans p p' (ld (Ο‡ n)) p<p' p'<ΞΆn)
      
  rounded-r : rounded-right R
  rounded-r q = ltr , rtl
   where
    ltr : βˆƒ n κž‰ β„€ , rd (Ο‡ n) < q β†’ βˆƒ q' κž‰ β„€[1/2] , q' < q Γ— q' ∈ R
    ltr = βˆ₯βˆ₯-functor I
     where
      I : Ξ£ n κž‰ β„€ , rd (Ο‡ n) < q β†’ Ξ£ q' κž‰ β„€[1/2] , q' < q Γ— q' ∈ R
      I (n , ΞΆn<q) = let (q' , ΞΆn<q' , q'<q) = dense (rd (Ο‡ n)) q ΞΆn<q
                     in q' , (q'<q , ∣ n , ΢n<q' ∣)
    rtl : βˆƒ q' κž‰ β„€[1/2] , q' < q Γ— (R q' holds) β†’ R q holds
    rtl = βˆ₯βˆ₯-rec βˆƒ-is-prop I
     where
      I : Ξ£ q' κž‰ β„€[1/2] , q' < q Γ— (R q' holds) β†’ R q holds
      I (q' , q'<q , te) = βˆ₯βˆ₯-functor II te
       where
        II : Ξ£ n κž‰ β„€ , (rd (Ο‡ n) < q') β†’ Ξ£ n κž‰ β„€ , (rd (Ο‡ n) <β„€[1/2] q)
        II (n , ΞΆ<q') = n , (trans (rd (Ο‡ n)) q' q ΞΆ<q' q'<q)
  
  is-disjoint : disjoint L R
  is-disjoint p q (tp<x , tx<q)
   = βˆ₯βˆ₯-rec (<β„€[1/2]-is-prop p q)
       (Ξ» ((n , p<l) , (n' , r<q))
        β†’ I n n' p<l r<q (β„€-dichotomous n n'))
       (binary-choice tp<x tx<q)
   where
    I : (n n' : β„€)
      β†’ p <β„€[1/2] ld (Ο‡ n)
      β†’ rd (Ο‡ n') <β„€[1/2] q
      β†’ (n ≀ n') + (n' ≀ n)
      β†’ p <β„€[1/2] q
    I n n' p<l r<q (inl n≀n')
      = let p<l' = β„€[1/2]<-≀ p (ld (Ο‡ n)) (ld (Ο‡ n')) p<l
                     (pr₁ (nested-implies-fully-nested
                             Ο‡ Ο„ n n' n≀n'))
            l<q' = β„€[1/2]≀-< (ld (Ο‡ n')) (rd (Ο‡ n')) q
                     (ld≀rd (Ο‡ n')) r<q 
      in trans p (ld (Ο‡ n')) q p<l' l<q'
    I n n' p<l r<q (inr n'≀n)
      = let p<r' = β„€[1/2]<-≀ p (ld (Ο‡ n)) (rd (Ο‡ n)) p<l
                     (ld≀rd (Ο‡ n))
            r<q' = β„€[1/2]≀-< (rd (Ο‡ n)) (rd (Ο‡ n')) q
                     (prβ‚‚ (nested-implies-fully-nested
                        Ο‡ Ο„ n' n n'≀n)) r<q
      in trans p (rd (Ο‡ n)) q p<r' r<q'
 
  is-located : located L R
  is-located p q p<q
   = I (Ο€ (1/2β„€[1/2] * (q - p))
         (β„€[1/2]<-positive-mult 1/2β„€[1/2] (q - p)
            0<1/2β„€[1/2] (diff-positive p q p<q)))
   where
    0<Ξ΅ : 0β„€[1/2] < (1/2β„€[1/2] * (q - p))
    0<Ξ΅ = <-pos-mult' 1/2β„€[1/2] (q - p) 0<1/2β„€[1/2]
            (diff-positive p q p<q)
    I : (Ξ£ n κž‰ β„€ , ((rd (Ο‡ n) - ld (Ο‡ n))
                     ≀℀[1/2] (1/2β„€[1/2] * (q - p))))
      β†’ (L p holds) ∨ (R q holds)
    I (n , l₁) = II (β„€[1/2]-ordering-property (rd (Ο‡ n))
                       (ld (Ο‡ n)) q p lβ‚‚)
     where
      lβ‚‚ :(rd (Ο‡ n) - ld (Ο‡ n)) < (q - p)
      lβ‚‚ = β„€[1/2]≀-< (rd (Ο‡ n) - ld (Ο‡ n)) (1/2β„€[1/2] * (q - p))
             (q - p) l₁ (β„€[1/2]-1/2-< (q - p) (diff-positive p q p<q))
      II : (rd (Ο‡ n) < q) + (p < ld (Ο‡ n)) β†’ (L p holds) ∨ (R q holds) 
      II (inl ΢<q) = ∣ inr ∣ n , ΢<q ∣ ∣
      II (inr p<΢) = ∣ inl ∣ n , p<΢ ∣ ∣
  
β„€Β³ : 𝓀₀ Μ‡
β„€Β³ = Ξ£ ((l , r) , p) κž‰ ((β„€ Γ— β„€) Γ— β„€) , l ≀ r

β„€Β³-to-β„€[1/2]α΄΅ : β„€Β³ β†’ β„€[1/2]α΄΅
β„€Β³-to-β„€[1/2]α΄΅ (((l , r) , p) , i)
 = ((ΞΉ (l , p)) , ΞΉ (r , p)) , normalise-≀2 l r p i

β¦…_⦆' : (Ο‡ : β„€ β†’ β„€Β³)
      β†’ nested (β„€Β³-to-β„€[1/2]α΄΅ ∘ Ο‡) β†’ positioned (β„€Β³-to-β„€[1/2]α΄΅ ∘ Ο‡)
      β†’ ℝ-d
β¦… Ο‡ ⦆' = β¦… β„€Β³-to-β„€[1/2]α΄΅ ∘ Ο‡ ⦆

β„€Β² : 𝓀₀ Μ‡ 
β„€Β² = β„€ Γ— β„€

β„€Β²-to-β„€Β³ : β„€Β² β†’ β„€Β³
β„€Β²-to-β„€Β³ (k , p)
 = (((k , k +pos 2) , p)
 , ℀≀-trans k (succβ„€ k) (succβ„€ (succβ„€ k))
     (≀-incrβ„€ k) (≀-incrβ„€ (succβ„€ k)))

β„€Β²-to-β„€[1/2]α΄΅ : β„€Β² β†’ β„€[1/2]α΄΅
β„€Β²-to-β„€[1/2]α΄΅ = β„€Β³-to-β„€[1/2]α΄΅ ∘ β„€Β²-to-β„€Β³

β¦…_⦆'' : (Ο‡ : β„€ β†’ β„€Β²)
      β†’ nested  (β„€Β²-to-β„€[1/2]α΄΅ ∘ Ο‡)
      β†’ positioned (β„€Β²-to-β„€[1/2]α΄΅ ∘ Ο‡)
      β†’ ℝ-d
β¦…_⦆'' = β¦…_⦆' ∘ (β„€Β²-to-β„€Β³ ∘_)

normalised : (β„€ β†’ β„€Β²) β†’ 𝓀₀ Μ‡ 
normalised Ο‡ = (n : β„€) β†’ prβ‚‚ (Ο‡ n) ＝ n

β„€Β²-width : ((k , p) : β„€Β²)
         β†’ (ΞΉ (k +pos 2 , p) - ΞΉ (k , p)) ＝ ΞΉ (pos 2 , p)
β„€Β²-width (k , p)
 = normalise-negation (k +pos 2) k p
 βˆ™ ap (Ξ» - β†’ ΞΉ (- , p))
     (β„€-left-succ (succβ„€ k) (β„€- k)
     βˆ™ ap succβ„€ (β„€-left-succ k (β„€- k))
     βˆ™ ap (succβ„€ ∘ succβ„€) (β„€-sum-of-inverse-is-zero k))

normalised-positioned : (Ο‡ : β„€ β†’ β„€Β²)
                   β†’ normalised Ο‡
                   β†’ positioned (β„€Β²-to-β„€[1/2]α΄΅ ∘ Ο‡)
normalised-positioned Ο‡ Ξ· Ο΅ ϡ⁺
 = q , transport (_≀ Ο΅) (β„€Β²-width (Ο‡ q) ⁻¹)
         (transport (Ξ» - β†’ ΞΉ (pos 2 , -) ≀ Ο΅) (Ξ· q ⁻¹) Ξ³)
 where
  q : β„€
  q = pr₁ (β„€[1/2]-find-lower Ο΅ ϡ⁺)
  f : pr₁ (β„€[1/2]-find-lower Ο΅ ϡ⁺) ＝
        prβ‚‚ (Ο‡ (pr₁ (β„€[1/2]-find-lower Ο΅ ϡ⁺)))
  f = η q ⁻¹
  Ξ³ : ΞΉ (pos 2 , q) ≀ Ο΅
  Ξ³ = <-is-≀℀[1/2] (ΞΉ (pos 2 , q)) Ο΅ (prβ‚‚ (β„€[1/2]-find-lower Ο΅ ϡ⁺))

℀≀-succ' : (a : β„€) (n : β„•) β†’ succβ„€ a ≀ succβ„€ (a +pos n)
℀≀-succ' a zero = zero , refl
℀≀-succ' a (succ n) = ℀≀-trans _ _ _ (℀≀-succ' a n) (1 , refl)

℀≀-succ : (a b : β„€) β†’ a ≀ b β†’ succβ„€ a ≀ succβ„€ b
℀≀-succ a b (n , refl) = ℀≀-succ' a n

℀≀-pred'
 : (a : β„€) (n : β„•) β†’ a ≀ (a +pos n)
℀≀-pred' a n = n , refl

℀≀-pred : (a b : β„€) β†’ succβ„€ a ≀ succβ„€ b β†’ a ≀ b
℀≀-pred a b (n , e)
  = transport (a ≀_)
      (succβ„€-lc (β„€-left-succ-pos a n ⁻¹ βˆ™ e))
      (℀≀-pred' a n)

downLeft-downRight-2
 : (a : β„€) β†’ downLeft (a +pos 2) ＝ downRight a +pos 2
downLeft-downRight-2 a
 = β„€-left-succ (succβ„€ a) (succβ„€ (succβ„€ a))
 βˆ™ ap succβ„€ (β„€-left-succ a (succβ„€ (succβ„€ a)))
 βˆ™ ap (succβ„€ ^ 2)
     (β„€-right-succ a (succβ„€ a)
     βˆ™ ap succβ„€ (β„€-right-succ a a))

β„€Β³-width : ((((l , r) , p) , _) : β„€Β³)
         β†’ (ΞΉ (r , p) - ΞΉ (l , p)) ＝ ΞΉ (r β„€- l , p)
β„€Β³-width (((l , r) , p) , _) = normalise-negation r l p

ternary-nested : (Ο‡ : β„€ β†’ β„€Β²)
               β†’ normalised Ο‡
               β†’ ternary (pr₁ ∘ Ο‡)
               ↔ nested (β„€Β²-to-β„€[1/2]α΄΅ ∘ Ο‡)
pr₁ (pr₁ (ternary-nested Ο‡ Ξ·) f n) = Ξ³
 where
  Ξ³' : ΞΉ (pr₁ (Ο‡ n) , n) ≀ ΞΉ (pr₁ (Ο‡ (succβ„€ n)) , succβ„€ n)
  Ξ³' = transport (_≀ ΞΉ (pr₁ (Ο‡ (succβ„€ n)) , succβ„€ n))
         (normalise-succ' (pr₁ (Ο‡ n)) n ⁻¹)
         (normalise-≀2
           (pr₁ (Ο‡ n) β„€+ pr₁ (Ο‡ n))
           (pr₁ (Ο‡ (succβ„€ n)))
           (succβ„€ n)
           (pr₁ (f n)))
  Ξ³ : ΞΉ (Ο‡ n) ≀ ΞΉ (Ο‡ (succβ„€ n))
  Ξ³ = transport (Ξ» - β†’ ΞΉ (pr₁ (Ο‡ n) , -)
                 ≀ ΞΉ (Ο‡ (succβ„€ n)))
        (η n ⁻¹)
        (transport (Ξ» - β†’ ΞΉ (pr₁ (Ο‡ n) , n)
                        ≀ ΞΉ (pr₁ (Ο‡ (succβ„€ n)) , -))
          (Ξ· (succβ„€ n) ⁻¹)
          Ξ³')
prβ‚‚ (pr₁ (ternary-nested Ο‡ Ξ·) f n) 
 = transport (Ξ» - β†’ ΞΉ ((pr₁ (Ο‡ (succβ„€ n)) +pos 2) , -)
                  ≀ ΞΉ ((pr₁ (Ο‡ n) +pos 2) , prβ‚‚ (Ο‡ n)))
     (Ξ· (succβ„€ n) ⁻¹)
     (transport (Ξ» - β†’ ΞΉ ((pr₁ (Ο‡ (succβ„€ n)) +pos 2) , succβ„€ n)
                     ≀ ΞΉ ((pr₁ (Ο‡ n) +pos 2) , -))
        (η n ⁻¹)
        (transport (ΞΉ ((pr₁ (Ο‡ (succβ„€ n)) +pos 2) , succβ„€ n) ≀_)
          (normalise-succ' (pr₁ (Ο‡ n) +pos 2) n ⁻¹)
          (normalise-≀2
            (pr₁ (Ο‡ (succβ„€ n)) +pos 2)
            ((pr₁ (Ο‡ n) +pos 2) β„€+ (pr₁ (Ο‡ n) +pos 2))
            (succβ„€ n)
            (transport ((pr₁ (Ο‡ (succβ„€ n)) +pos 2) ≀_)
              (downLeft-downRight-2 (pr₁ (Ο‡ n)) ⁻¹)
              (℀≀-succ _ _ (℀≀-succ _ _ (prβ‚‚ (f n))))))))
pr₁ (prβ‚‚ (ternary-nested Ο‡ Ξ·) f n)
 = from-normalise-≀-same-denom _ _ (succβ„€ n) Ξ³
 where
  Ξ³' : ΞΉ (pr₁ (Ο‡ n) , n) ≀ ΞΉ (pr₁ (Ο‡ (succβ„€ n)) , succβ„€ n)
  Ξ³' = transport (Ξ» - β†’ ΞΉ (pr₁ (Ο‡ n) , -)
                      ≀ ΞΉ (pr₁ (Ο‡ (succβ„€ n)) , succβ„€ n))
         (Ξ· n)
         (transport (Ξ» - β†’ ΞΉ (Ο‡ n) ≀ ΞΉ (pr₁ (Ο‡ (succβ„€ n)) , -))
           (Ξ· (succβ„€ n))
           (pr₁ (f n)))
  Ξ³ : ΞΉ (downLeft (pr₁ (Ο‡ n)) , succβ„€ n)
    ≀ ΞΉ (pr₁ (Ο‡ (succβ„€ n)) , succβ„€ n)
  Ξ³ = transport (_≀ ΞΉ (pr₁ (Ο‡ (succβ„€ n)) , succβ„€ n))
        (normalise-succ' (pr₁ (Ο‡ n)) n)
        Ξ³'
prβ‚‚ (prβ‚‚ (ternary-nested Ο‡ Ξ·) f n)
 = ℀≀-pred _ _ (℀≀-pred _ _
     (from-normalise-≀-same-denom _ _ (succβ„€ n) Ξ³))
 where
  Ξ³'' : ΞΉ (pr₁ (Ο‡ (succβ„€ n)) +pos 2 , succβ„€ n)
      ≀ ΞΉ (pr₁ (Ο‡ n) +pos 2 , n)
  Ξ³'' = transport (Ξ» - β†’ ΞΉ (pr₁ (Ο‡ (succβ„€ n)) +pos 2 , -)
                       ≀ ΞΉ (pr₁ (Ο‡ n) +pos 2 , n))
          (Ξ· (succβ„€ n))
          (transport (Ξ» - β†’ ΞΉ (pr₁ (Ο‡ (succβ„€ n)) +pos 2
                             , prβ‚‚ (Ο‡ (succβ„€ n)))
                          ≀ ΞΉ (pr₁ (Ο‡ n) +pos 2 , -))
            (Ξ· n)
            (prβ‚‚ (f n)))
  Ξ³' : ΞΉ (pr₁ (Ο‡ (succβ„€ n)) +pos 2 , succβ„€ n)
     ≀ ΞΉ (downLeft (pr₁ (Ο‡ n) +pos 2) , succβ„€ n)
  Ξ³' = transport (ΞΉ (pr₁ (Ο‡ (succβ„€ n)) +pos 2 , succβ„€ n) ≀_)
        (normalise-succ' (pr₁ (Ο‡ n) +pos 2) n)
        Ξ³''
  Ξ³ : ΞΉ (pr₁ (Ο‡ (succβ„€ n)) +pos 2 , succβ„€ n)
    ≀ ΞΉ (downRight (pr₁ (Ο‡ n)) +pos 2 , succβ„€ n)
  Ξ³ = transport (Ξ» - β†’ ΞΉ (pr₁ (Ο‡ (succβ„€ n)) +pos 2 , succβ„€ n)
                     ≀ ΞΉ (- , succβ„€ n))
        (downLeft-downRight-2 (pr₁ (Ο‡ n)))
        Ξ³'

to-interval-seq : 𝕋 β†’ (β„€ β†’ β„€Β²)
to-interval-seq Ο‡ n = (pr₁ Ο‡ n) , n

𝕋→nested-normalised
 : 𝕋 β†’ Ξ£ Ο‡ κž‰ (β„€ β†’ β„€Β²) , (nested (β„€Β²-to-β„€[1/2]α΄΅ ∘ Ο‡) Γ— normalised Ο‡)
𝕋→nested-normalised Ο‡
 = to-interval-seq Ο‡
 , pr₁ (ternary-nested _ i) (prβ‚‚ Ο‡)
 , i
 where
   i : normalised (to-interval-seq Ο‡)
   i n = refl

ternary-normalised→𝕋
 : Ξ£ Ο‡ κž‰ (β„€ β†’ β„€Β²) , (nested (β„€Β²-to-β„€[1/2]α΄΅ ∘ Ο‡) Γ— normalised Ο‡) β†’ 𝕋
ternary-normalised→𝕋 (Ο‡ , Ο„ , Ο€)
 = (pr₁ ∘ Ο‡) , prβ‚‚ (ternary-nested Ο‡ Ο€) Ο„

open import UF.Equiv

covers-is-prop : (a b : β„€[1/2]α΄΅) β†’ is-prop (a covers b)
covers-is-prop ((l₁ , r₁) , _) ((lβ‚‚ , rβ‚‚) , _)
 = Γ—-is-prop (≀℀[1/2]-is-prop l₁ lβ‚‚) (≀℀[1/2]-is-prop rβ‚‚ r₁)

nested-is-prop : (Ο‡ : β„€ β†’ β„€[1/2]α΄΅) β†’ is-prop (nested Ο‡)
nested-is-prop Ο‡
 = Ξ -is-prop (fe _ _) (Ξ» n β†’ covers-is-prop (Ο‡ n) (Ο‡ (succβ„€ n)))

normalised-is-prop : (Ο‡ : β„€ β†’ β„€Β²) β†’ is-prop (normalised Ο‡)
normalised-is-prop Ο‡ = Ξ -is-prop (fe _ _) (Ξ» _ β†’ β„€-is-set)

nested-Γ—-normalised-is-prop
 : (Ο‡ : β„€ β†’ β„€Β²)
 β†’ is-prop (nested (β„€Β²-to-β„€[1/2]α΄΅ ∘ Ο‡) Γ— normalised Ο‡)
nested-Γ—-normalised-is-prop Ο‡
 = Γ—-is-prop (nested-is-prop (β„€Β²-to-β„€[1/2]α΄΅ ∘ Ο‡))
             (normalised-is-prop Ο‡)

below-is-prop : (a b : β„€) β†’ is-prop (a below b)
below-is-prop a b
 = Γ—-is-prop (℀≀-is-prop (downLeft b) a)
             (℀≀-is-prop a (downRight b))

ternary-is-prop : (Ο‡ : β„€ β†’ β„€) β†’ is-prop (ternary Ο‡)
ternary-is-prop Ο‡
 = Ξ -is-prop (fe _ _) (Ξ» n β†’ below-is-prop (Ο‡ (succβ„€ n)) (Ο‡ n)) 

ternary-normalised≃𝕋 : (Ξ£ Ο‡ κž‰ (β„€ β†’ β„€Β²)
                     , (nested (β„€Β²-to-β„€[1/2]α΄΅ ∘ Ο‡)
                     Γ— normalised Ο‡))
                     ≃ 𝕋
ternary-normalised≃𝕋
 = qinveq ternary-normalised→𝕋 (𝕋→nested-normalised , ρ , ΞΌ)
 where
  ρ : 𝕋→nested-normalised ∘ ternary-normalised→𝕋 ∼ id
  ρ (Ο‡ , Ο„ , Ο€)
   = to-subtype-＝ nested-Γ—-normalised-is-prop (dfunext (fe _ _) Ξ³)
   where
    Ξ³ : to-interval-seq (ternary-normalised→𝕋 (Ο‡ , Ο„ , Ο€)) ∼ Ο‡
    Ξ³ i = ap (pr₁ (Ο‡ i) ,_) (Ο€ i ⁻¹)
  ΞΌ : (ternary-normalised→𝕋 ∘ 𝕋→nested-normalised) ∼ id
  ΞΌ (Ο‡ , b) = to-subtype-＝ ternary-is-prop (dfunext (fe _ _) Ξ³)
   where
    Ξ³ : (Ξ» x β†’ pr₁ (pr₁ (𝕋→nested-normalised (Ο‡ , b)) x)) ∼ Ο‡
    Ξ³ i = refl

𝕋→nested-positioned
 : 𝕋
 β†’ Ξ£ Ο‡ κž‰ (β„€ β†’ β„€Β²) , (nested (β„€Β²-to-β„€[1/2]α΄΅ ∘ Ο‡)
                  Γ— positioned (β„€Β²-to-β„€[1/2]α΄΅ ∘ Ο‡))
𝕋→nested-positioned Ο‡
 = Ο‡' , Ο„ , normalised-positioned Ο‡' Ο€
 where
  Ξ³ = 𝕋→nested-normalised Ο‡
  Ο‡' = pr₁ Ξ³ 
  Ο„  = pr₁ (prβ‚‚ Ξ³)
  Ο€  = prβ‚‚ (prβ‚‚ Ξ³)

⟦_⟧ : 𝕋 β†’ ℝ-d
⟦ Ο‡ ⟧ = β¦… Ο‡' ⦆'' Ο„ Ο€
 where
  Ξ³ = 𝕋→nested-positioned Ο‡
  Ο‡' = pr₁ Ξ³ 
  Ο„  = pr₁ (prβ‚‚ Ξ³)
  Ο€  = prβ‚‚ (prβ‚‚ Ξ³)
\end{code}

## Representing compact intervals

\begin{code} 
CompactInterval : β„€ Γ— β„€ β†’ 𝓀₀ Μ‡
CompactInterval (k , Ξ΄) = Ξ£ (x , _) κž‰ 𝕋 , x(Ξ΄) ＝ k

CompactInterval2 : β„€ Γ— β„€ β†’ 𝓀₀ Μ‡
CompactInterval2 (k , Ξ΄)
 = Ξ£ Ο‡ κž‰ (β„• β†’ β„€) , (Ο‡ 0 below k)
                 Γ— ((n : β„•) β†’ Ο‡ (succ n) below Ο‡ n)

CompactInterval-1-to-2 : ((k , Ξ΄) : β„€ Γ— β„€)
                       β†’ CompactInterval  (k , Ξ΄)
                       β†’ CompactInterval2 (k , Ξ΄)
CompactInterval-1-to-2 (k , Ξ΄) ((Ο‡' , b') , e')
 = Ο‡ , transport (Ο‡' (succβ„€ Ξ΄) below_) e' (b' Ξ΄) , bβ‚›
 where
  Ο‡ : β„• β†’ β„€
  Ο‡ n =  Ο‡' (succβ„€ (Ξ΄ +pos n))
  bβ‚€ : Ο‡ 0 below Ο‡' Ξ΄
  bβ‚€ = b' Ξ΄
  bβ‚› : (n : β„•) β†’ Ο‡ (succ n) below Ο‡ n
  bβ‚› n = b' (succβ„€ (Ξ΄ +pos n))

replace-right''
 : ((k , Ξ΄) : β„€ Γ— β„€) β†’ (β„• β†’ β„€) β†’ (n : β„€) β†’ trich-locate n Ξ΄ β†’ β„€
replace-right'' (k , Ξ΄) Ο‡ n (inl (i , n+si＝δ))
 = (upRight ^ succ i) k
replace-right'' (k , Ξ΄) Ο‡ n (inr (inl refl))
 = k
replace-right'' (k , Ξ΄) Ο‡ n (inr (inr (i , Ξ΄+si＝n)))
 = Ο‡ i

replace-right''-correct
 : ((k , Ξ΄) : β„€ Γ— β„€)
 β†’ (Ο‡ : β„• β†’ β„€)
 β†’ Ο‡ 0 below k
 β†’ ((n : β„•) β†’ Ο‡ (succ n) below Ο‡ n) 
 β†’ (n : β„€)
 β†’ (Ξ· : trich-locate n Ξ΄)
 β†’       replace-right'' (k , Ξ΄) Ο‡ (succβ„€ n) (β„€-trich-succ n Ξ΄ Ξ·)
   below replace-right'' (k , Ξ΄) Ο‡ n Ξ·
replace-right''-correct (k , Ξ΄) Ο‡ bβ‚€ bβ‚› n (inl (0      , refl))
 = above-implies-below _ _ (upRight-above _)
replace-right''-correct (k , Ξ΄) Ο‡ bβ‚€ bβ‚› n (inl (succ i , refl))
 = above-implies-below _ _ (upRight-above _)
replace-right''-correct (k , Ξ΄) Ο‡ bβ‚€ bβ‚› n (inr (inl refl))
 = bβ‚€
replace-right''-correct (k , Ξ΄) Ο‡ bβ‚€ bβ‚› n (inr (inr (i , refl)))
 = bβ‚› i

CompactInterval-2-to-1 : ((k , Ξ΄) : β„€ Γ— β„€)
                       β†’ CompactInterval2 (k , Ξ΄)
                       β†’ CompactInterval  (k , Ξ΄)
CompactInterval-2-to-1 (k , Ξ΄) (Ο‡' , b'β‚€ , b'β‚›)
 = (Ο‡ , b) , e
 where
  Ο‡ : β„€ β†’ β„€
  Ο‡ n = replace-right'' (k , Ξ΄) Ο‡' n (β„€-trichotomous n Ξ΄)
  b' : (n : β„€) β†’ replace-right'' (k , Ξ΄) Ο‡' (succβ„€ n)
                   (β„€-trich-succ n Ξ΄ (β„€-trichotomous n Ξ΄))
                 below
                 replace-right'' (k , Ξ΄) Ο‡' n (β„€-trichotomous n Ξ΄)
  b' n = replace-right''-correct (k , Ξ΄) Ο‡' b'β‚€ b'β‚› n
           (β„€-trichotomous n Ξ΄)
  b : (n : β„€) β†’ Ο‡ (succβ„€ n) below Ο‡ n
  b n = transport (Ξ» - β†’ replace-right'' (k , Ξ΄) Ο‡' (succβ„€ n) -
                         below Ο‡ n)
          (β„€-trichotomous-is-prop _ _
            (β„€-trich-succ n Ξ΄ (β„€-trichotomous n Ξ΄))
            (β„€-trichotomous (succβ„€ n) Ξ΄))
          (b' n)
  e : Ο‡ Ξ΄ ＝ k
  e = ap (replace-right'' (k , Ξ΄) Ο‡' Ξ΄)
        (β„€-trichotomous-is-prop _ _ (β„€-trichotomous Ξ΄ Ξ΄)
        (inr (inl refl)))

_β‰ˆ_ : 𝕋 β†’ 𝕋 β†’ 𝓀₀ Μ‡
(χ₁ , _) β‰ˆ (Ο‡β‚‚ , _) = Ξ£ Ξ΄ κž‰ β„€ , ((n : β„€) β†’ Ξ΄ ≀ n β†’ χ₁ n ＝ Ο‡β‚‚ n)

CompactInterval-β‰ˆ
 : ((k , Ξ΄) : β„€ Γ— β„€)
 β†’ ((Ο‡ , b) : CompactInterval (k , Ξ΄))
 β†’ Ο‡ β‰ˆ pr₁ (CompactInterval-2-to-1 (k , Ξ΄)
             (CompactInterval-1-to-2 (k , Ξ΄) (Ο‡ , b)))
CompactInterval-β‰ˆ (k , Ξ΄) ((Ο‡' , b') , e') = Ξ΄ , Ξ³
 where
  Ο‡ = pr₁ (CompactInterval-2-to-1 (k , Ξ΄)
             (CompactInterval-1-to-2 (k , Ξ΄) ((Ο‡' , b') , e')))
  Ξ³ : (n : β„€) β†’ Ξ΄ ≀ n β†’ Ο‡' n ＝ pr₁ Ο‡ n
  Ξ³ n (0 , refl)
   = e'
   βˆ™ ap (replace-right'' (k , Ξ΄)
       (pr₁ (CompactInterval-1-to-2 (k , Ξ΄) ((Ο‡' , b') , e'))) Ξ΄)
       (β„€-trichotomous-is-prop _ _
         (β„€-trichotomous Ξ΄ Ξ΄)
         (inr (inl refl))) ⁻¹
  Ξ³ n (succ i , refl)
   = ap (replace-right'' (k , Ξ΄)
       (pr₁ (CompactInterval-1-to-2 (k , Ξ΄) ((Ο‡' , b') , e')))
       (Ξ΄ +pos succ i))
       (β„€-trichotomous-is-prop _ _
         (β„€-trichotomous (Ξ΄ +pos succ i) Ξ΄)
         (inr (inr (i , β„€-left-succ-pos Ξ΄ i)))) ⁻¹

down-to-πŸ› : (a b : β„€) β†’ a below' b β†’ πŸ›
down-to-πŸ› a b (inl      dL ) = βˆ’1
down-to-πŸ› a b (inr (inl dM)) =  O
down-to-πŸ› a b (inr (inr dR)) = +1

πŸ›-to-down : (a : πŸ›) β†’ (β„€ β†’ β„€)
πŸ›-to-down βˆ’1 = downLeft
πŸ›-to-down  O = downMid
πŸ›-to-down +1 = downRight

πŸ›-down-eq : (a b : β„€) (d : a below' b)
          β†’ πŸ›-to-down (down-to-πŸ› a b d) b ＝ a 
πŸ›-down-eq a b (inl      dL ) = dL ⁻¹
πŸ›-down-eq a b (inr (inl dM)) = dM ⁻¹
πŸ›-down-eq a b (inr (inr dR)) = dR ⁻¹

down-πŸ›-eq : (a : πŸ›) (b : β„€)
          β†’ (e : πŸ›-to-down a b below' b)
          β†’ down-to-πŸ› (πŸ›-to-down a b) b e ＝ a 
down-πŸ›-eq βˆ’1 b (inl e) = refl
down-πŸ›-eq  O b (inl e)
 = 𝟘-elim (downLeftβ‰ downMid b b refl (e ⁻¹))
down-πŸ›-eq +1 b (inl e)
 = 𝟘-elim (downLeftβ‰ downRight b b refl (e ⁻¹))
down-πŸ›-eq βˆ’1 b (inr (inl e))
 = 𝟘-elim (downLeftβ‰ downMid b b refl e)
down-πŸ›-eq  O b (inr (inl e)) = refl
down-πŸ›-eq +1 b (inr (inl e))
 = 𝟘-elim (downMidβ‰ downRight b b refl (e ⁻¹))
down-πŸ›-eq βˆ’1 b (inr (inr e))
 = 𝟘-elim (downLeftβ‰ downRight b b refl e)
down-πŸ›-eq  O b (inr (inr e))
 = 𝟘-elim (downMidβ‰ downRight b b refl e)
down-πŸ›-eq +1 b (inr (inr e)) = refl

CI2-to-πŸ›α΄Ί  : ((k , i) : β„€ Γ— β„€) β†’ CompactInterval2 (k , i) β†’ πŸ›α΄Ί
CI2-to-πŸ›α΄Ί (k , i) (Ο‡ , bβ‚€ , bβ‚›) 0
 = down-to-πŸ› (Ο‡ 0) k (below-implies-below' (Ο‡ 0) k bβ‚€)
CI2-to-πŸ›α΄Ί (k , i) (Ο‡ , bβ‚€ , bβ‚›) (succ n)
 = down-to-πŸ› (Ο‡ (succ n)) (Ο‡ n)
    (below-implies-below' (Ο‡ (succ n)) (Ο‡ n) (bβ‚› n))

πŸ›-to-down-is-below : (a : πŸ›) (k : β„€) β†’ πŸ›-to-down a k below k
πŸ›-to-down-is-below βˆ’1 k = downLeft-below  k
πŸ›-to-down-is-below  O k = downMid-below   k
πŸ›-to-down-is-below +1 k = downRight-below k

πŸ›α΄Ί-to-CI2 : ((k , i) : β„€ Γ— β„€) β†’ πŸ›α΄Ί β†’ CompactInterval2 (k , i)
πŸ›α΄Ί-to-CI2 (k , i) Ξ± = Ο‡ , bβ‚€ , bβ‚›
 where
  Ο‡  : β„• β†’ β„€
  Ο‡ 0        = πŸ›-to-down (Ξ± 0) k
  Ο‡ (succ n) = πŸ›-to-down (Ξ± (succ n)) (Ο‡ n)
  bβ‚€ : Ο‡ 0 below k
  bβ‚€ = πŸ›-to-down-is-below (Ξ± 0) k
  bβ‚› : (n : β„•) β†’ Ο‡ (succ n) below Ο‡ n
  bβ‚› n = πŸ›-to-down-is-below (Ξ± (succ n)) (Ο‡ n)

integer-approx : πŸ›α΄Ί β†’ (β„• β†’ β„€)
integer-approx Ξ± = pr₁ (πŸ›α΄Ί-to-CI2 (negsucc 0 , pos 0) Ξ±)

πŸ›-possibilities : (a : πŸ›) β†’ (a ＝ βˆ’1) + (a ＝ O) + (a ＝ +1)
πŸ›-possibilities βˆ’1 = inl refl
πŸ›-possibilities  O = inr (inl refl)
πŸ›-possibilities +1 = inr (inr refl)

CI2-criteria : ((k , i) : β„€ Γ— β„€) β†’ (β„• β†’ β„€) β†’ 𝓀₀ Μ‡
CI2-criteria (k , i) Ο‡ = (Ο‡ 0 below k)
                       Γ— ((n : β„•) β†’ Ο‡ (succ n) below Ο‡ n)

CI2-prop
 : ((k , i) : β„€ Γ— β„€)
 β†’ (Ο‡ : β„• β†’ β„€)
 β†’ is-prop (CI2-criteria (k , i) Ο‡)
CI2-prop (k , i) Ο‡
 = Γ—-is-prop (below-is-prop (Ο‡ 0) k)
     (Ξ -is-prop (fe _ _) (Ξ» n β†’ below-is-prop (Ο‡ (succ n)) (Ο‡ n)))

CompactInterval2-ternary
 : ((k , i) : β„€ Γ— β„€) β†’ CompactInterval2 (k , i) ≃ πŸ›α΄Ί
CompactInterval2-ternary (k , i)
 = qinveq (CI2-to-πŸ›α΄Ί (k , i)) (πŸ›α΄Ί-to-CI2 (k , i) , Ξ· , ΞΌ)
 where
  Ξ· : (πŸ›α΄Ί-to-CI2 (k , i)) ∘ (CI2-to-πŸ›α΄Ί (k , i)) ∼ id
  Ξ· (Ο‡ , bβ‚€ , bβ‚›)
   = to-subtype-＝ (CI2-prop (k , i)) (dfunext (fe _ _) γ)
   where
    Ο‡' = pr₁ (πŸ›α΄Ί-to-CI2 (k , i) (CI2-to-πŸ›α΄Ί (k , i) (Ο‡ , bβ‚€ , bβ‚›))) 
    Ξ³ : Ο‡' ∼ Ο‡
    Ξ³ zero = πŸ›-down-eq (Ο‡ 0) k (below-implies-below' (Ο‡ 0) k bβ‚€)
    Ξ³ (succ n)
     = ap (πŸ›-to-down (down-to-πŸ› (Ο‡ (succ n)) (Ο‡ n)
            (below-implies-below' (Ο‡ (succ n)) (Ο‡ n) (bβ‚› n))))
          (Ξ³ n)
     βˆ™ πŸ›-down-eq (Ο‡ (succ n)) (Ο‡ n)
         (below-implies-below' (Ο‡ (succ n)) (Ο‡ n) (bβ‚› n))
  ΞΌ : (CI2-to-πŸ›α΄Ί (k , i)) ∘ (πŸ›α΄Ί-to-CI2 (k , i)) ∼ id
  ΞΌ Ξ± = dfunext (fe _ _) Ξ³
   where
    Ξ±' = πŸ›α΄Ί-to-CI2 (k , i) Ξ±
    Ξ³ : CI2-to-πŸ›α΄Ί (k , i) Ξ±' ∼ Ξ±
    Ξ³ 0 = down-πŸ›-eq (Ξ± 0) k _
    Ξ³ (succ n) = down-πŸ›-eq (Ξ± (succ n)) _ _

CI2-ClosenessSpace
 : ((k , i) : β„€ Γ— β„€)
 β†’ is-closeness-space (CompactInterval2 (k , i))
CI2-ClosenessSpace (k , i)
 = Ξ£-clospace (CI2-criteria (k , i)) (CI2-prop (k , i))
     (discrete-seq-clospace (Ξ» _ β†’ β„€-is-discrete))

_split-below_ : β„€ β†’ β„€ β†’ 𝓀₀ Μ‡
n split-below m = (n ＝ downLeft m) + (n ＝ downRight m)

split-below-is-prop : (n m : β„€) β†’ is-prop (n split-below m)
split-below-is-prop n m
 = +-is-prop β„€-is-set β„€-is-set
     (Ξ» l r β†’ downLeftβ‰ downRight m m refl (l ⁻¹ βˆ™ r))

CI3-criteria : ((k , i) : β„€ Γ— β„€) β†’ (β„• β†’ β„€) β†’ 𝓀₀ Μ‡
CI3-criteria (k , i) Ο‡ = (Ο‡ 0 split-below k)
                       Γ— ((n : β„•) β†’ Ο‡ (succ n) split-below Ο‡ n)

CI3-prop : ((k , i) : β„€ Γ— β„€)
         β†’ (Ο‡ : β„• β†’ β„€)
         β†’ is-prop (CI3-criteria (k , i) Ο‡)
CI3-prop (k , i) Ο‡
 = Γ—-is-prop (split-below-is-prop (Ο‡ 0) k)
     (Ξ -is-prop (fe _ _)
       (Ξ» n β†’ split-below-is-prop (Ο‡ (succ n)) (Ο‡ n)))

CompactInterval3 : β„€ Γ— β„€ β†’ 𝓀₀ Μ‡
CompactInterval3 (k , i) = Ξ£ (CI3-criteria (k , i))

split-below-implies-below : (n m : β„€) β†’ n split-below m β†’ n below m
split-below-implies-below n m (inl refl) = (0 , refl) , (2 , refl)
split-below-implies-below n m (inr refl) = (2 , refl) , (0 , refl)

CI3-to-CI2 : ((k , i) : β„€ Γ— β„€)
           β†’ CompactInterval3 (k , i)
           β†’ CompactInterval2 (k , i)
CI3-to-CI2 (k , i) (Ο‡ , bβ‚€ , bβ‚›)
 = Ο‡ , split-below-implies-below (Ο‡ 0) k bβ‚€
 , Ξ» n β†’ split-below-implies-below (Ο‡ (succ n)) (Ο‡ n) (bβ‚› n)

CI3-ClosenessSpace
 : ((k , i) : β„€ Γ— β„€) β†’ is-closeness-space (CompactInterval3 (k , i))
CI3-ClosenessSpace (k , i) 
 = Ξ£-clospace (CI3-criteria (k , i)) (CI3-prop (k , i))
     (discrete-seq-clospace (Ξ» _ β†’ β„€-is-discrete))

𝟚ᴺ = β„• β†’ 𝟚

down-to-𝟚 : (a b : β„€) β†’ a split-below b β†’ 𝟚
down-to-𝟚 a b (inl dL) = β‚€
down-to-𝟚 a b (inr dR) = ₁

𝟚-to-down : (a : 𝟚) β†’ (β„€ β†’ β„€)
𝟚-to-down β‚€ = downLeft
𝟚-to-down ₁ = downRight

𝟚-to-down-is-below : (a : 𝟚) (k : β„€) β†’ 𝟚-to-down a k split-below k
𝟚-to-down-is-below β‚€ k = inl refl
𝟚-to-down-is-below ₁ k = inr refl

𝟚-down-eq : (a b : β„€) (d : a split-below b)
          β†’ 𝟚-to-down (down-to-𝟚 a b d) b ＝ a 
𝟚-down-eq a b (inl dL) = dL ⁻¹
𝟚-down-eq a b (inr dR) = dR ⁻¹

down-𝟚-eq : (a : 𝟚) (b : β„€) (e : 𝟚-to-down a b split-below b)
          β†’ down-to-𝟚 (𝟚-to-down a b) b e ＝ a 
down-𝟚-eq β‚€ b (inl e) = refl
down-𝟚-eq ₁ b (inl e) = 𝟘-elim (downLeftβ‰ downRight b b refl (e ⁻¹))
down-𝟚-eq β‚€ b (inr e) = 𝟘-elim (downLeftβ‰ downRight b b refl e)
down-𝟚-eq ₁ b (inr e) = refl

CI3-to-𝟚ᴺ
 : ((k , i) : β„€ Γ— β„€) β†’ CompactInterval3 (k , i) β†’ 𝟚ᴺ
CI3-to-𝟚ᴺ (k , i) (Ο‡ , bβ‚€ , bβ‚›) 0
 = down-to-𝟚 (Ο‡ 0) k bβ‚€
CI3-to-𝟚ᴺ (k , i) (Ο‡ , bβ‚€ , bβ‚›) (succ n)
 = down-to-𝟚 (Ο‡ (succ n)) (Ο‡ n) (bβ‚› n)

𝟚ᴺ-to-CI3 : ((k , i) : β„€ Γ— β„€) β†’ 𝟚ᴺ β†’ CompactInterval3 (k , i)
𝟚ᴺ-to-CI3 (k , i) Ξ± = Ο‡ , bβ‚€ , bβ‚›
 where
  Ο‡  : β„• β†’ β„€
  Ο‡ 0        = 𝟚-to-down (Ξ± 0) k
  Ο‡ (succ n) = 𝟚-to-down (Ξ± (succ n)) (Ο‡ n)
  bβ‚€ : Ο‡ 0 split-below k
  bβ‚€ = 𝟚-to-down-is-below (Ξ± 0) k
  bβ‚› : (n : β„•) β†’ Ο‡ (succ n) split-below Ο‡ n
  bβ‚› n = 𝟚-to-down-is-below (Ξ± (succ n)) (Ο‡ n)

CompactInterval3-cantor
 : ((k , i) : β„€ Γ— β„€) β†’ CompactInterval3 (k , i) ≃ 𝟚ᴺ
CompactInterval3-cantor (k , i)
 = qinveq (CI3-to-𝟚ᴺ (k , i)) (𝟚ᴺ-to-CI3 (k , i) , η , μ)
 where
  η : (𝟚ᴺ-to-CI3 (k , i)) ∘ (CI3-to-𝟚ᴺ (k , i)) ∼ id
  Ξ· (Ο‡ , bβ‚€ , bβ‚›)
   = to-subtype-＝ (CI3-prop (k , i)) (dfunext (fe _ _) γ)
   where
    Ο‡' = pr₁ (𝟚ᴺ-to-CI3 (k , i) (CI3-to-𝟚ᴺ (k , i) (Ο‡ , bβ‚€ , bβ‚›))) 
    Ξ³ : Ο‡' ∼ Ο‡
    Ξ³ 0 = 𝟚-down-eq (Ο‡ 0) k bβ‚€
    Ξ³ (succ n)
     = ap (𝟚-to-down (down-to-𝟚 (Ο‡ (succ n)) (Ο‡ n) (bβ‚› n))) (Ξ³ n)
     βˆ™ 𝟚-down-eq (Ο‡ (succ n)) (Ο‡ n) (bβ‚› n)
  μ : (CI3-to-𝟚ᴺ (k , i)) ∘ (𝟚ᴺ-to-CI3 (k , i)) ∼ id
  ΞΌ Ξ± = dfunext (fe _ _) Ξ³
   where
    α' = 𝟚ᴺ-to-CI3 (k , i) α
    γ : CI3-to-𝟚ᴺ (k , i) α' ∼ α
    γ 0 = down-𝟚-eq (α 0) k (𝟚-to-down-is-below (α 0) k)
    γ (succ n) = down-𝟚-eq (α (succ n)) _ _
\end{code}