----------------------------------------------------------------------------------------------------
-- Brouwer trees as a quotient inductive-inductive type
----------------------------------------------------------------------------------------------------

{- Brouwer trees consisting of zero, succ, and limits of strictly
   increasing sequences.  The path constructor of the ordinal type
   says that bisimilar sequences give equal limits.  The type of
   Brouwer trees with this definition will not be a set automatically.
   Therefore, a truncation constructor is added. -}

{-# OPTIONS --cubical #-}

module BrouwerTree.Base where

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

open import Cubical.Data.Nat

import Simulations
  renaming (_simulated-by_ to _≲_ ; _bisimilar-to_ to _≈_)


{- Quotient inductive-inductive type of Brouwer trees -}

mutual
  data Brw : Type
  data _≤_ : Brw → Brw → Type

  open Simulations Brw _≤_ public

  data Brw where
    zero  : Brw
    succ  : Brw → Brw
    limit : (f : ℕ → Brw) → {f↑ : increasing f} → Brw
    bisim : ∀ f {f↑} g {g↑} →
            f ≈ g →
            limit f {f↑} ≡ limit g {g↑}
    trunc : isSet Brw

  data _≤_ where
    ≤-zero      : ∀ {x} → zero ≤ x
    ≤-trans     : ∀ {x y z} → x ≤ y → y ≤ z → x ≤ z
    ≤-succ-mono : ∀ {x y} → x ≤ y → succ x ≤ succ y
    ≤-cocone    : ∀ {x} f {f↑ k} → (x ≤ f k) → (x ≤ limit f {f↑})
    ≤-limiting  : ∀ f {f↑ x} → ((k : ℕ) → f k ≤ x) → limit f {f↑} ≤ x
    ≤-trunc     : ∀ {x y} → isProp (x ≤ y)

  _<_ : Brw → Brw → Type
  x < y = succ x ≤ y

  increasing : (ℕ → Brw) → Type
  increasing f = ∀ k → f k < f (suc k)

one : Brw
one = succ zero

{- Simple induction principles

   We show two simple special cases of the general induction principle:
   One for propositional propertier of ordinals, and one for propositional
   properties of inequalities.
-}

{- The first one is called Brw-ind: -}

Brw-ind : ∀ {a} →
            (P : Brw → Type a) →
            (P-prop : (x : Brw) → isProp (P x)) →
            (z : P zero) →
            (s : {x : Brw} → P x → P (succ x)) →
            (l : ∀ {f f↑} → ((k : ℕ) → P (f k)) → P (limit f {f↑})) →
            (x : Brw) → P x
Brw-ind P isProp⟨P⟩ z s l zero = z
Brw-ind P isProp⟨P⟩ z s l (succ x) = s (Brw-ind P isProp⟨P⟩ z s l x)
Brw-ind P isProp⟨P⟩ z s l (limit f {f↑}) = l λ k → Brw-ind P isProp⟨P⟩ z s l (f k)
Brw-ind P isProp⟨P⟩ z s l (bisim f {f↑} g {g↑} f∼g i) =
  isProp→PathP (λ j → isProp⟨P⟩ (bisim f g f∼g j))
               (l λ k → Brw-ind P isProp⟨P⟩ z s l (f k))
               (l λ k → Brw-ind P isProp⟨P⟩ z s l (g k)) i
Brw-ind P isProp⟨P⟩ z s l (trunc x y p q i j) =
  isProp→SquareP (λ i j → isProp⟨P⟩ (trunc x y p q i j))
                 (λ j → Brw-ind P isProp⟨P⟩ z s l x)
                 (λ j → Brw-ind P isProp⟨P⟩ z s l y)
                 (λ j → Brw-ind P isProp⟨P⟩ z s l (p j))
                 (λ j → Brw-ind P isProp⟨P⟩ z s l (q j)) i j

{- The second principle is called ≤-ind.-}

-- At the time of writing this code, Agda issue #4725
-- <https://github.com/agda/agda/issues/4725> means that the following
-- definition is not seen as terminating, because the "dot patterns"
-- have been moved from the implicit x and y to the smaller arguments
-- of the proof x ≤ y, and --cubical does not take decrease in dot
-- patterns into account for termination checking. This would be okay
-- for us, if only the dot patterns were reconstructed as written!
-- Issue #4725 is that they are not, and to work around this bug, we
-- mark the definition as terminating.
{-# TERMINATING #-}
≤-ind : ∀ {a} →
        (P : ∀ {x y} → x ≤ y → Type a) →
        (∀ {x y} x≤y → isProp (P {x} {y} x≤y)) →
        (∀ {x} → P (≤-zero {x})) →
        (∀ {x y z} {x≤y : x ≤ y} {y≤z : y ≤ z} → P x≤y → P y≤z → P (≤-trans x≤y y≤z)) →
        (∀ {x y} (x≤y : x ≤ y) → P x≤y → P (≤-succ-mono x≤y)) →
        (∀ {x} f {f↑} {k} → (x≤fk : x ≤ f k) → P (x≤fk) → P (≤-cocone {x} f {f↑} {k} x≤fk)) →
        (∀ f {f↑} {y} f≤y → (∀ k → P (f≤y k)) → (∀ k → P (f↑ k)) → P (≤-limiting f {f↑} {y} f≤y)) →
        {x y : Brw} → (x≤y : x ≤ y) → P x≤y
≤-ind P prop z t s c l {.zero} {y} ≤-zero = z
≤-ind P prop z t s c l {x} {y} (≤-trans x≤x₁ x₁≤y) =
    t (≤-ind P prop z t s c l x≤x₁) (≤-ind P prop z t s c l x₁≤y)
≤-ind P prop z t s c l {.(succ x)} {.(succ y)} (≤-succ-mono {x} {y} x≤y) =
    s x≤y (≤-ind P prop z t s c l x≤y)
≤-ind P prop z t s c l {x} {.(limit f)} (≤-cocone f {k = k} x≤fk) =
    c f {k = k} x≤fk (≤-ind P prop z t s c l x≤fk)
≤-ind P prop z t s c l {.(limit f)} {y} (≤-limiting f {f↑} {x} f≤y) =
    l f {f↑} {y} f≤y (λ k → ≤-ind P prop z t s c l (f≤y k)) (λ k → ≤-ind P prop z t s c l (f↑ k))
≤-ind P prop z t s c l {x} {y} (≤-trunc x≤y x≤y' i) =
    isProp→PathP (λ j → prop (≤-trunc x≤y x≤y' j)) (≤-ind P prop z t s c l x≤y)
                 (≤-ind P prop z t s c l x≤y') i

{- The more general induction principle into Sets and Propositions -}

module _ {ℓ ℓ' : Level} (P : Brw → Type ℓ) (Q : (x y : Brw) → x ≤ y → P x → P y → Type ℓ')
         (isSet⟨P⟩ : (x : Brw) → isSet (P x))
         (isProp⟨Q⟩ : (x y : Brw) (x≤y : x ≤ y) (px : P x) (py : P y) → isProp (Q x y x≤y px py))
         (z : P zero)
         (s : {x : Brw} → P x → P (succ x))
         (l : ∀ {f f↑} (pf : (k : ℕ) → P (f k)) →
                ((k : ℕ) → Q (succ (f k)) (f (suc k)) (f↑ k) (s (pf k)) (pf (suc k))) →
                P (limit f {f↑}))
         (bs : ∀ {f f↑ g g↑ f≈g} →
                 (pf : (k : ℕ) → P (f k)) →
                 (pf↑ : (k : ℕ) → Q (succ (f k)) (f (suc k)) (f↑ k) (s (pf k)) (pf (suc k))) →
                 (pg : (k : ℕ) → P (g k)) →
                 (pg↑ : (k : ℕ) → Q (succ (g k)) (g (suc k)) (g↑ k) (s (pg k)) (pg (suc k))) →
                 PathP (λ i → P (bisim f {f↑} g {g↑} f≈g i)) (l pf pf↑) (l pg pg↑))
         (z≤ : ∀ {y} → (py : P y) → Q zero y (≤-zero {y}) z py)
         (t≤ : ∀ {x y z} {x≤y : x ≤ y} {y≤z : y ≤ z} (px : P x) (py : P y) (pz : P z) →
                 Q x y x≤y px py → Q y z y≤z py pz → Q x z (≤-trans x≤y y≤z) px pz)
         (s≤ : ∀ {x y} (x≤y : x ≤ y) (px : P x) (py : P y) →
                 Q x y x≤y px py → Q (succ x) (succ y) (≤-succ-mono x≤y) (s px) (s py))
         (c≤ : ∀ {x} f {f↑} {k} (x≤fk : x ≤ f k)
                 (px : P x) →
                 (pf : (k : ℕ) → P (f k)) →
                 (pf↑ : (k : ℕ) → Q (succ (f k)) (f (suc k)) (f↑ k) (s (pf k)) (pf (suc k))) →
                 (qx≤fk : Q x (f k) x≤fk px (pf k)) →
                 Q x (limit f) (≤-cocone {x} f {f↑} {k} x≤fk) px (l pf pf↑))
         (l≤ : ∀ f {f↑} {y} f≤y →
                 (pf : (k : ℕ) → P (f k)) →
                 (pf↑ : (k : ℕ) → Q (succ (f k)) (f (suc k)) (f↑ k) (s (pf k)) (pf (suc k))) →
                 (py : P y) →
                 Q (limit f) y (≤-limiting f {f↑} {y} f≤y) (l pf pf↑) py)
  where

  mutual
    -- Agda issue #4725, see the discussion above
    {-# TERMINATING #-}
    Brw-elim : (x : Brw) → P x
    Brw-elim zero = z
    Brw-elim (succ x) = s (Brw-elim x)
    Brw-elim (limit f {f↑}) = l (Brw-elim ∘ f) (≤-elim ∘ f↑)
    Brw-elim (bisim f {f↑} g {g↑} f≈g i) = bs (Brw-elim ∘ f) (≤-elim ∘ f↑)
                                              (Brw-elim ∘ g) (≤-elim ∘ g↑) i
    Brw-elim (trunc x y p q i j) = isSet→SquareP {A = λ i j → P (trunc x y p q i j)}
                                                 (λ i j → isSet⟨P⟩ (trunc x y p q i j))
                                                 (λ j → Brw-elim (p j))
                                                 (λ j → Brw-elim (q j))
                                                 (λ _ → Brw-elim x)
                                                 (λ _ → Brw-elim y) i j

    ≤-elim : {x y : Brw} → (x≤y : x ≤ y) → Q x y x≤y (Brw-elim x) (Brw-elim y)
    ≤-elim {.zero} {y} ≤-zero = z≤ (Brw-elim y)
    ≤-elim {x} {y} (≤-trans {y = z} x≤z z≤y) = t≤ (Brw-elim x) (Brw-elim z) (Brw-elim y)
                                                  (≤-elim x≤z) (≤-elim z≤y)
    ≤-elim {.(succ x)} {.(succ y)} (≤-succ-mono {x} {y} x≤y) = s≤ x≤y (Brw-elim x) (Brw-elim y)
                                                                  (≤-elim x≤y)
    ≤-elim {x} {.(limit f)} (≤-cocone f {f↑} x≤fk) = c≤ f x≤fk (Brw-elim x)
                                                        (Brw-elim ∘ f) (≤-elim ∘ f↑) (≤-elim x≤fk)
    ≤-elim {.(limit f)} {y} (≤-limiting f {f↑} x) = l≤ f x (Brw-elim ∘ f) (≤-elim ∘ f↑) (Brw-elim y)
    ≤-elim {x} {y} (≤-trunc p q i) =
        isProp→PathP {B = λ i → Q x y (≤-trunc p q i) (Brw-elim x) (Brw-elim y)}
                     (λ i → isProp⟨Q⟩ x y (≤-trunc p q i) (Brw-elim x) (Brw-elim y))
                     (≤-elim p) (≤-elim q) i