----------------------------------------------------------------------------------------------------
-- An order-preserving embedding from Brouwer trees to Extensional Wellfounded orders
----------------------------------------------------------------------------------------------------

{-# OPTIONS --cubical #-}

module Interpretations.BrwToOrd where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function

open import Cubical.Data.Sigma
open import Cubical.Data.Empty as ⊥
open import Cubical.Induction.WellFounded
  renaming (WellFounded to isWellFounded)

open import BrouwerTree.Everything as B
open import ExtensionalWellfoundedOrder.Everything as O

open Ord
open isSimulation

{- The interpretation -}

BtoO : Brw → Ord
Carrier (BtoO a) = Σ[ y ∈ Brw ] (y B.< a)
_≺_ (BtoO a) (y , p) (y' , p') = y B.< y'
truncated (BtoO a) x x' = <-trunc
wellfounded (BtoO a) (y , p) = helper y p (<-is-wellfounded y) where
  helper : ∀ y p → Acc (B._<_) y → Acc (_≺_ (BtoO a)) (y , p)
  helper y p (acc q) = acc (λ { (z , z<a) z<y → helper z z<a (q z z<y) })
Ord.extensional (BtoO a) (y , y<a) (y' , y'<a) ext =
  Σ≡Prop {B = λ y → y B.< a} (λ x → <-trunc)
         (B.<-extensional y y' λ c → (λ c<y → fst (ext (c , <-trans _ _ _ c<y y<a)) c<y) ,
                                   λ c<y' → snd (ext (c , <-trans _ _ _ c<y' y'<a)) c<y')
transitive (BtoO a) (x , _) (y , _) (z , _) x<y y<z = <-trans x y z x<y y<z

{- BtoO is monotone wrt both < and ≤ -}

BtoO-≤-monotone : (a b : Brw) → a B.≤ b → BtoO a O.≤ BtoO b
_≤_.f (BtoO-≤-monotone a b a≤b) (y , y<a) = y , <∘≤-in-< y<a a≤b
monotone (_≤_.f-simulation (BtoO-≤-monotone a b a≤b)) y≤y' = y≤y'
simulation (_≤_.f-simulation (BtoO-≤-monotone a b a≤b)) {y , y<b} {x , x<a} y<x
  = (y , <-trans _ _ _ y<x x<a) , y<x ,  Σ≡Prop (λ x → <-trunc) refl

BtoO-<-monotone : (a b : Brw) → a B.< b → BtoO a O.< BtoO b
_<_.sim (BtoO-<-monotone a b a<b) = BtoO-≤-monotone a b (<-in-≤ a<b)
_<_.bound (BtoO-<-monotone a b a<b) = a , a<b
_<_.bounded (BtoO-<-monotone a b a<b) (y , y<a) = y<a
equiv-proof (_<_.equiv (BtoO-<-monotone a b a<b)) ((y , y<b) , y<a) =
  (((y , y<a) , (Σ≡Prop (λ x → <-trunc) (Σ≡Prop (λ x → <-trunc) refl))) ,
   (λ ((y' , y'<a) , p) → Σ≡Prop (λ x → isSetCarrier (initial-segment (BtoO b) (a , a<b)) _ _)
                                 (Σ≡Prop (λ x → <-trunc) (sym (cong (fst ∘ fst) p)))))