----------------------------------------------------------------------------------------------------
-- 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)))))