----------------------------------------------------------------------------------------------------
-- Classifiablility of Brouwer trees
----------------------------------------------------------------------------------------------------

{-# OPTIONS --cubical #-}

module BrouwerTree.Classifiability where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function

open import Cubical.Data.Sum
open import Cubical.Data.Sigma
open import Cubical.Data.Empty as 
open import Cubical.Data.Nat
  using ( ; zero ; suc)
open import Cubical.Relation.Nullary

open import BrouwerTree.Base
open import BrouwerTree.Properties
open import BrouwerTree.Code.Results

open import Abstract.ZerSucLim _<_ _≤_ public

open Properties
 isSetBrw
  _ _  <-trunc)
  _ _  ≤-trunc)
 <-irreflexive
  _  ≤-refl)
  _ _ _  ≤-trans)
 antisym
 <∘≤-in-<
 public

zero-is-zero : is-zero zero
zero-is-zero = λ b  ≤-zero

is-zero→≡zero : {a : Brw}  is-zero a  a  zero
is-zero→≡zero {a} za = x≤zero→x≡zero (za zero)

succ-calc-strong-suc : (a : Brw)  (succ a) is-strong-suc-of a
succ-calc-strong-suc a = (≤-refl ,  x a<x  a<x )) , λ x x<sa  ≤-succ-mono⁻¹ x<sa

succ-is-suc : (a : Brw)  (succ a) is-suc-of a
succ-is-suc a = fst (succ-calc-strong-suc a)

is-suc→≡succ :  {a b}  a is-suc-of b  a  succ b
is-suc→≡succ {a} {b} sa = cong fst (suc-unique b (a , sa) (succ b , fst (succ-calc-strong-suc b)))

limit-is-sup :  f (f↑ : increasing f)  limit f {f↑} is-sup-of f
limit-is-sup f f↑ =  i  ≤-cocone-simple f) , λ x  ≤-limiting f {x = x}

is-lim→≡limit :  {a f f↑}  a is-lim-of (f , f↑)  a  limit f {f↑}
is-lim→≡limit {a} {f} {f↑} a-is-lim = antisym (snd a-is-lim (limit f {f↑})  n  ≤-cocone-simple f))
                                              (≤-limiting f {f↑}  k  fst a-is-lim k))

is-sup-increasing→≡limit :  {a f}  (f↑ : increasing f)  a is-sup-of f  a  limit f {f↑}
is-sup-increasing→≡limit {a} {f} f↑ a-is-sup = is-lim→≡limit a-is-sup

Brw-is-classifiable : (a : Brw)  is-classifiable a
Brw-is-classifiable = Brw-ind  a  is-classifiable a) isProp⟨is-classifiable⟩
                        (inl zero-is-zero)
                         {a} _  inr (inl (a , succ-calc-strong-suc a)))
                        λ {f} {f↑} _  inr (inr  (f , f↑) , limit-is-sup f f↑ )

open ClassifiabilityInduction Brw-is-classifiable <-is-wellfounded public