----------------------------------------------------------------------------------------------------
-- Constructions on (Covered) Marked Extensional and Wellfounded Orders
----------------------------------------------------------------------------------------------------

{-# OPTIONS --cubical --safe #-}

module MEWO.Constructions where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure using (typ; str)

open import Cubical.Data.Unit
open import Cubical.Data.Empty as 
open import Cubical.Data.Sum
open import Cubical.Data.Sigma
open import Cubical.Induction.WellFounded
  renaming (WellFounded to isWellFounded)
open import Cubical.Relation.Binary
open BinaryRelation

open import Cubical.HITs.SetQuotients as Q

open import PropTrunc

open import Iff
open import General-Properties
open import Relation.Closure

open import MEWO.Base
open import MEWO.Covered

open import Abstract.ZerSucLim

{- Successor -}

succ-< : (A : MEWO )   A   Unit   A   Unit  Type 
succ-< A (inl x) (inl y) = x ≺⟨ A  y
succ-< A (inl x) (inr _) = marked A x
succ-< A (inr _) y = ⊥*

isProp⟨succ-<⟩ : (A : MEWO )  isPropValued (succ-< A)
isProp⟨succ-<⟩ A (inl x) (inl y) = truncated A x y
isProp⟨succ-<⟩ A (inl x) (inr _) = isPropMarked A x
isProp⟨succ-<⟩ A (inr x) y = isProp⊥*

isExtensional⟨succ-<⟩ : (A : MEWO )  isCovered A  isExtensional (succ-< A)
isExtensional⟨succ-<⟩ A cov (inl x) (inl y) ext
  = cong inl (extensional A x y λ c  ext (inl c))
isExtensional⟨succ-<⟩ A cov (inl x) (inr tt) ext
  = ∥-∥rec (isSet⊎ (isSetCarrier A) isSetUnit _ _)
           (p , mp , x<*p)  ⊥.rec (wellfounded→irreflexive (TransClWellfounded _ (wellfounded A)) _
                                                              (stepT _ (snd (ext (inl p)) mp) x<*p)))
          (cov x)
isExtensional⟨succ-<⟩ A cov (inr tt) (inl y) ext
  = ∥-∥rec (isSet⊎ (isSetCarrier A) isSetUnit _ _)
           (p , mp , y<*p)  ⊥.rec (wellfounded→irreflexive (TransClWellfounded _ (wellfounded A)) _
                                                              (stepT _ (fst (ext (inl p)) mp) y<*p)))
          (cov y)
isExtensional⟨succ-<⟩ A cov (inr tt) (inr tt) ext = refl

isWellFounded⟨succ-<⟩ : (A : MEWO )  isWellFounded (succ-< A)
isWellFounded⟨succ-<⟩ A (inl y) = acc-lemma y (wellfounded A y)
  where
    acc-lemma :  y  Acc (underlyingOrder A) y  Acc (succ-< A) (inl y)
    acc-lemma y (acc s) = acc λ { (inl z) z<y  acc-lemma z (s z z<y) }
isWellFounded⟨succ-<⟩ A (inr x) = acc λ { (inl y) my  acc-lemma y (wellfounded A y) }
  where
    acc-lemma :  y  Acc (underlyingOrder A) y  Acc (succ-< A) (inl y)
    acc-lemma y (acc s) = acc λ { (inl z) z<y  acc-lemma z (s z z<y) }

succ-marking : (A : MEWO )   A   Unit  hProp 
succ-marking A (inl x) = ⊥* , isProp⊥*
succ-marking A (inr _) = Unit* , isPropUnit*

succ : (A : MEWO )  isCovered A  MEWO 
succ A cov = ( A   Unit) ,
             (succ-< A , succ-marking A) ,
             isProp⟨succ-<⟩ A , isExtensional⟨succ-<⟩ A cov , isWellFounded⟨succ-<⟩ A

inl<inr-lemma : (A : MEWO )  (cov : isCovered A)  (a :  A )   inl a ≺⁺⟨ succ A cov  inr tt 
inl<inr-lemma A cov a
  = ∥-∥map  (p , mp , a<*p)  ReflTransTransCl-trans _
                                                      (ReflTransCl-map inl (idfun _) a<*p) (emb mp))
          (cov a)

succCovered : (A : MEWO )  (cov : isCovered A)  isCovered (succ A cov)
succCovered A cov (inr tt) =  inr tt , tt* , done 
succCovered A cov (inl x)
  = ∥-∥map  inlx<+inrtt  inr tt , tt* , Trans→ReflTrans _ inlx<+inrtt) (inl<inr-lemma A cov x)


csucc : MEWOcov   MEWOcov 
csucc (A , cov) = (succ A cov , succCovered A cov)

↓+inr : (A : MEWO )  (cov : isCovered A)  succ A cov ↓+ inr tt  A
↓+inr A cov = ≤Antisymmetry _ _ sA↓inr≤A A≤sA↓inr
  where
   A≤sA↓inr : A  (succ A cov ↓+ inr tt)
   A≤sA↓inr =  a  inl a ,
              inl<inr-lemma A cov a) ,
              ((λ p  p) , λ p  p) ,
               { {inl a , p} {b} a<b  a , a<b , Σ≡Prop  x  isPropPropTrunc) refl })

   sA↓inr≤A : (succ A cov ↓+ inr tt)  A
   sA↓inr≤A = f , ((λ {x} {y}  mono {x} {y}) , λ {x}  mark {x}) , sim
    where
     f :  succ A cov ↓+ inr tt    A 
     f (inl a , p) = a
     f (inr x , p) =
       ⊥.rec (wellfounded→irreflexive (∥TransCl∥-wellfounded (isWellFounded⟨succ-<⟩ A)) _ p)

     mono : isMonotone (succ A cov ↓+ inr tt) A f
     mono {inl x , p} {inl y , q} x<y = x<y
     mono {inl x , p} {inr tt , q} x<y =
       ⊥.rec (wellfounded→irreflexive (∥TransCl∥-wellfounded (isWellFounded⟨succ-<⟩ A)) _ q)

     mark : isMarkingPreserving (succ A cov ↓+ inr tt) A f
     mark {inl x , p} mx = mx

     sim : {b :  A } {a :  succ A cov ↓+ inr tt }  b ≺⟨ A  (f a) 
           Σ  succ A cov ↓+ inr tt   a'  a' ≺⟨ succ A cov ↓+ inr tt  a × (f a'  b))
     sim {b} {inl a , p} b<a = (inl b , ∥-∥map  p  TransCl-trans _ (emb b<a) p) p) , b<a , refl
     sim {b} {inr tt , p} =
       ⊥.rec (wellfounded→irreflexive (∥TransCl∥-wellfounded (isWellFounded⟨succ-<⟩ A)) _ p)

¬inr<+inl : (A : MEWO )  (a :  A )  TransCl (succ-< A) (inr tt) (inl a)  
¬inr<+inl A a (emb ())
¬inr<+inl A a (step () ps)


↓+inl : (A : MEWO )  (cov : isCovered A)  (a :  A )  succ A cov ↓+ inl a  A ↓+ a
↓+inl A cov a = ≤Antisymmetry _ _ sA↓inla≤A↓a A↓a≤sA↓inla
  where
    cast :  {x y}  (inl x) ≺⁺⟨ succ A cov  (inl y)  x ≺⁺⟨ A  y
    cast (emb p) = emb p
    cast (step {y = inl y} p ps) = step p (cast ps)
    cast (step {y = inr tt} p ps) = ⊥.rec (¬inr<+inl A _ ps)

    sA↓inla≤A↓a : (succ A cov ↓+ inl a)  (A ↓+ a)
    sA↓inla≤A↓a = f , ((λ {x} {y}  mono {x} {y}) , λ {x}  mark {x}) , sim
      where
        f :  succ A cov ↓+ inl a    A ↓+ a 
        f (inl x , p) = x , ∥-∥map cast p
        f (inr tt , p) = ⊥.rec (∥-∥rec isProp⊥ (¬inr<+inl A a) p)

        mono : isMonotone (succ A cov ↓+ inl a) (A ↓+ a) f
        mono {inl x , p} {inl y , q} x<y = x<y
        mono {inl x , p} {inr tt , q} x<y = ⊥.rec (∥-∥rec isProp⊥ (¬inr<+inl A a) q)

        mark : isMarkingPreserving (succ A cov ↓+ inl a) (A ↓+ a) f
        mark {inl x , p} mx = mx

        sim : {b :  A ↓+ a } {x :  succ A cov ↓+ inl a }  b ≺⟨ A ↓+ a  (f x) 
              Σ  succ A cov ↓+ inl a   x'  x' ≺⟨ succ A cov ↓+ inl a  x × (f x'  b))
        sim {b , p} {inl x , q} b<x =
          (inl b , ∥-∥map  q  step b<x q) q) , b<x , Σ≡Prop  x  isPropPropTrunc) refl
        sim {b , p} {inr tt , q} b<x = ⊥.rec (∥-∥rec isProp⊥ (¬inr<+inl A a) q)

    A↓a≤sA↓inla : (A ↓+ a)  (succ A cov ↓+ inl a)
    A↓a≤sA↓inla =  (x , p)  inl x ,
                  ∥-∥map (TransCl-map inl (idfun _)) p) ,
                  ((λ p  p) ,  p  p)) ,
                   { {inl b , p} b<a  (b , ∥-∥map cast p) , b<a , Σ≡Prop  x  isPropPropTrunc)
                                                                           refl })

A<succA : (X : MEWOcov )  X <c csucc X
A<succA (A , cov) = (inr tt) , tt* , sym (↓+inr A cov)

X<Y→sX≤Y : (X Y : MEWOcov )  X <c Y  csucc X ≤c Y
X<Y→sX≤Y (A , covA) (B , covB) (b , mb , A≡B↓b)
 = f , ((λ {x} {y}  mono-f {x} {y}) , λ {x}  mark-f {x}) , sim-f
   where
    tr :  A    B ↓+ b 
    tr = fst (idtoeqₒ A (B ↓+ b) A≡B↓b)

    tr⁻¹ :  B ↓+ b    A 
    tr⁻¹ = invIsEq (fst (snd (snd (idtoeqₒ A (B ↓+ b) A≡B↓b))))

    tr⁻¹tr≡id :  y  tr⁻¹ (tr y)  y
    tr⁻¹tr≡id = retIsEq (fst (snd (snd (idtoeqₒ A (B ↓+ b) A≡B↓b))))

    trtr⁻¹≡id :  y  tr (tr⁻¹ y)  y
    trtr⁻¹≡id = secIsEq (fst (snd (snd (idtoeqₒ A (B ↓+ b) A≡B↓b))))

    f :  succ A covA    B 
    f (inl x) = fst (tr x)
    f (inr x) = b

    mono-f : isMonotone (succ A covA) B f
    mono-f {inl x} {inl y} x<y = fst (fst (snd (idtoeqₒ A (B ↓+ b) A≡B↓b))) x<y
    mono-f {inl x} {inr tt} mx = snd (fst (snd (idtoeqₒ A (B ↓+ b) A≡B↓b))) mx

    mark-f : isMarkingPreserving (succ A covA) B f
    mark-f {inr x} tt* = mb

    sim-f : {y :  B }{a :  succ A covA }  y ≺⟨ B  f a 
            Σ  succ A covA   a'  a' ≺⟨ succ A covA  a × (f a'  y))
    sim-f {y} {inl a} b<fa = inl (tr⁻¹ (y , ∥-∥map  q  step b<fa q) (snd (tr a)))) ,
                             subst  z  tr⁻¹ (y , ∥-∥map  q  step b<fa q) (snd (tr a))) ≺⟨ A  z)
                                   (tr⁻¹tr≡id a)
                                   (fst (snd (snd (snd (idtoeqₒ A (B ↓+ b) A≡B↓b)))) b<fa) ,
                             cong fst (trtr⁻¹≡id (y , _))
    sim-f {y} {inr tt} b<fa = inl (tr⁻¹ (y ,  emb b<fa )) ,
                              snd (snd (snd (snd (idtoeqₒ A (B ↓+ b) A≡B↓b)))) b<fa ,
                              cong fst (trtr⁻¹≡id (y ,  emb b<fa ))

X<sY→X≤Y : (X Y : MEWOcov )  X <c csucc Y  X ≤c Y
X<sY→X≤Y (A , cA) (B , cB) (inr tt , mb , A≡sB↓b) = subst (A ≤_) (A≡sB↓b  ↓+inr B cB) (≤Refl A)

MEWOcov-has-succ : calc-strong-suc (_<c_ { = }) _≤c_ csucc
MEWOcov-has-succ b = ((A<succA b) , X<Y→sX≤Y b) , λ Y  X<sY→X≤Y Y b

{- Union -}

module _ (A : Type )(F : A  MEWO ) where

  private
    ΣAF = Σ[ a  A ]  F a 

  -- In order to stay in the same universe with the union, we use the
  -- small characterisations of ≡ and < here
  ~∪ : ΣAF  ΣAF  Type 
  ~∪ (a , x) (b , y) = (F a ↓+ x) ≃ₒ (F b ↓+ y)

  <∪ : ΣAF  ΣAF  Type 
  <∪ (a , x) (b , y) = (F a ↓+ x) <⁻ (F b ↓+ y)

  isWellFounded⟨<∪⟩ : isWellFounded <∪
  isWellFounded⟨<∪⟩ (a , x) = acc-lemma a x  (<Wellfounded (F a ↓+ x))
    where
      acc-lemma :  b y  Acc _<_ (F b ↓+ y)  Acc <∪ (b , y)
      acc-lemma b y (acc s) = acc  (c , z) p  acc-lemma c z (s (F c ↓+ z) (<⁻To< _ _ p)))

  <∪-extensionalUpto-~ : (p q : ΣAF) 
                          ((r : ΣAF)  <∪ r p  <∪ r q) 
                          ~∪ p q
  <∪-extensionalUpto-~ (a , x) (b , y) ext = idtoeqₒ _ _ Fa↓+x≡Fb↓+y
    where
      ext' : (C : MEWO )  C < (F a ↓+ x)  C < (F b ↓+ y)
      ext' C =
         ((z , q) , mz , p)  subst (_< (F b ↓+ y))
                                      (sym (p  iterated↓+ (F a) x z q))
                                      (<⁻To< _ _ (fst (ext (a , z))
                                                      (<To<⁻ _ _ (↓+Monotone< (F a) z x mz))))) ,
         ((z , q) , mz , p)  subst (_< (F a ↓+ x))
                                      (sym (p  iterated↓+ (F b) y z q))
                                      (<⁻To< _ _ (snd (ext (b , z))
                                                      (<To<⁻ _ _ (↓+Monotone< (F b) z y mz)))))

      Fa↓+x≡Fb↓+y : F a ↓+ x  F b ↓+ y
      Fa↓+x≡Fb↓+y = cong fst (coveredExtensional (F a ↓+ x , initialSegmentsCovered (F a) x)
                                                 (F b ↓+ y , initialSegmentsCovered (F b) y)
                                                  (C , covC)  ext' C))

  <∪/~P : ΣAF / ~∪  ΣAF / ~∪  hProp 
  <∪/~P = rec2 isSetHProp
             (a , x) (b , y)  <∪ _ _ , isProp⟨<⁻⟩ (F a ↓+ x) (F b ↓+ y))
             (a , x) (b , y) (c , z) p  Σ≡Prop  x  isPropIsProp)
                                                  (hPropExt
                                                    (isProp⟨<⁻⟩ (F a ↓+ x) (F c ↓+ z))
                                                    (isProp⟨<⁻⟩ (F b ↓+ y) (F c ↓+ z))
                                                    (subst (_<⁻ (F c ↓+ z))
                                                           (eqtoidₒ (F a ↓+ x) (F b ↓+ y) p))
                                                    (subst (_<⁻ (F c ↓+ z))
                                                           (sym (eqtoidₒ (F a ↓+ x) (F b ↓+ y) p)))))
             (a , x) (b , y) (c , z) p  Σ≡Prop  x  isPropIsProp)
                                                  (hPropExt
                                                    (isProp⟨<⁻⟩ (F a ↓+ x) (F b ↓+ y))
                                                    (isProp⟨<⁻⟩ (F a ↓+ x) (F c ↓+ z))
                                                    (subst ((F a ↓+ x) <⁻_)
                                                           (eqtoidₒ (F b ↓+ y) (F c ↓+ z) p))
                                                    (subst ((F a ↓+ x) <⁻_)
                                                           (sym (eqtoidₒ (F b ↓+ y) (F c ↓+ z) p)))))

  <∪/~ : ΣAF / ~∪  ΣAF / ~∪  Type 
  <∪/~ x y = typ (<∪/~P x y)

  isProp⟨<∪/~⟩ : isPropValued <∪/~
  isProp⟨<∪/~⟩ x y = str (<∪/~P x y)

  ⋃-marking : ΣAF / ~∪  hProp 
  ⋃-marking s =  (Σ[ a  A ] (Σ[ x   F a  ] (s  [ a , x ]) × marked (F a) x))  , isPropPropTrunc

  Acc-<∪/~-lemma : (x : ΣAF)  Acc <∪ x  Acc <∪/~ [ x ]
  Acc-<∪/~-lemma x (acc s) = acc (elimProp  y  isProp→ (isPropAcc _))
                                            y y<x  Acc-<∪/~-lemma y (s y y<x)))

   : MEWO 
   = ((ΣAF / ~∪) ,
      (<∪/~ , ⋃-marking) ,
       x y  str (<∪/~P x y)) ,
      elimProp2
         x y  isProp→ (squash/ x y))
         p q ext  eq/ p q (<∪-extensionalUpto-~ p q
                                 r  elimProp {P = λ c  <∪/~ c [ p ]  <∪/~ c [ q ]}
                                                 c  isProp× (isProp→ (isProp⟨<∪/~⟩ c [ q ]))
                                                               (isProp→ (isProp⟨<∪/~⟩ c [ p ])))
                                                 c  ext [ c ]) [ r ]))) ,
      elimProp  x  isPropAcc _) λ { x  Acc-<∪/~-lemma x (isWellFounded⟨<∪⟩ x) })

  ~-equivRel : isEquivRel ~∪
  isEquivRel.reflexive ~-equivRel (a , x) = idtoeqₒ (F a ↓+ x) _ refl
  isEquivRel.symmetric ~-equivRel (a , x) (b , y) p
    = idtoeqₒ _ _ (sym (eqtoidₒ (F a ↓+ x) (F b ↓+ y) p))
  isEquivRel.transitive ~-equivRel (a , x) (b , y) (c , z) p q
    = idtoeqₒ _ _ (eqtoidₒ (F a ↓+ x) (F b ↓+ y) p  eqtoidₒ (F b ↓+ y) (F c ↓+ z) q)

  ~-effective : (a b : A)  (x :  F a )(y :  F b )  [ a , x ]  [ b , y ]  F a ↓+ x  F b ↓+ y
  ~-effective a b x y eq
    = eqtoidₒ _ _ (effective  (a , x) (b , y)  isProp⟨≃ₒ⟩ (F a ↓+ x) (F b ↓+ y))
                             ~-equivRel
                             (a , x) (b , y) eq)

  ⋃-isUpperBound : (a : A)  F a  
  ⋃-isUpperBound a =  x  [ a , x ]) ,
                     ((λ {x} {y} x<y  <To<⁻ _ (F a ↓+ y)
                                               (↓+Monotone< _ _ _ x<y)) ,
                       {x} mx   a , x , refl , mx )) ,
                      {b} {x}  elimProp {P = P x} (isPropP x) (d x) b)
    where
      P : (x :  F a )  ΣAF / ~∪  Type 
      P x = λ b  b ≺⟨   [ a , x ]  Σ[ x'   F a  ] (x' ≺⟨ F a  x × ([ a , x' ]  b))

      isPropP : (x :  F a )  (y : ΣAF / ~∪)  isProp (P x y)
      isPropP x y = isProp→ (injective→simulationConclusionIsProp (F a)   x  [ a , x ])
                               {x} {y} eq  ↓+Injective (F a) x y (~-effective a a x y eq)))

      d : (x :  F a )  (y : ΣAF)  P x [ y ]
      d x (b , y) ((b' , b'<+x) , mb' , eq)
        = (b' ,
           mb' ,
           eq/ _ _ (idtoeqₒ _ _ (sym (eqtoidₒ (F b ↓+ y) _ eq  iterated↓+ (F a) x b' b'<+x))))

  ⋃-covered : ((a : A)  isCovered (F a))  isCovered 
  ⋃-covered covF = elimProp  x  isPropPropTrunc)
                             (a , x)  ∥-∥map (cov a x) (covF a x))
    where
      cov : (a : A)  (x :  F a ) 
            Σ[ y   F a  ] marked (F a) y × x ≺̂*⟨ F a  y 
            Σ[ y     ] marked  y × [ a , x ] ≺̂*⟨   y
      cov a x (p , mp , x<*p) = [ a , p ] ,
                                 a , p , refl , mp  ,
                                ReflTransCl-map  x  [ a , x ])
                                                 x<y  <To<⁻ _ _ (↓+Monotone< (F a) _ _ x<y)) x<*p

  ⋃↓[] : (a : A)  (x :  F a )   ↓+ [ a , x ]  F a ↓+ x
  ⋃↓[] a x = acc-helper a x (wellfounded  [ a , x ])
    where
      acc-helper : (a : A)  (x :  F a )  Acc <∪/~ [ a , x ]   ↓+ [ a , x ]  F a ↓+ x
      acc-helper a x (acc s) = ≤Antisymmetry _ _ f g
       where
        f : ( ↓+ [ a , x ])  (F a ↓+ x)
        f = covered→principal ( ↓+ [ a , x ])
                              (initialSegmentsCovered () [ a , x ])
                              (F a ↓+ x)
                              (≤ₚCharacterisationFrom ( ↓+ [ a , x ])
                                                      (F a ↓+ x)
                                                       (y , p)  lem y p))
          where
            lem : (y :   )  (p :  y ≺⁺⟨   [ a , x ] )  marked ( ↓+ [ a , x ]) (y , p) 
                   Σ[ z   F a ↓+ x  ] (( ↓+ [ a , x ]) ↓+ (y , p)  (F a ↓+ x) ↓+ z) ×
                                           marked (F a ↓+ x) z 
            lem = elimProp  y  isPropΠ2  p _  isPropPropTrunc))
                            (b , y) p my@(b' , mb' , q)   b' ,
                                                              iterated↓+  [ a , x ] [ b , y ] p 
                                                              acc-helper b y (s [ b , y ] my) 
                                                              eqtoidₒ (F b ↓+ y) _ q , mb' )

        g : (F a ↓+ x)  ( ↓+ [ a , x ])
        g = covered→principal
              (F a ↓+ x)
              (initialSegmentsCovered (F a) x)
              ( ↓+ [ a , x ])
              (≤ₚCharacterisationFrom
                (F a ↓+ x)
                ( ↓+ [ a , x ])
                 (y , p) my   ([ a , y ] ,
                                   ∥-∥map (TransCl-map  x  [ a , x ])
                                          {x} {y} x<y  <To<⁻ _ _
                                                                (↓+Monotone< (F a) x y x<y))) p) ,
                                  iterated↓+ (F a) x y p 
                                  sym
                                    (iterated↓+ 
                                                [ a , x ]
                                                [ a , y ]
                                                (∥-∥map
                                                  (TransCl-map
                                                     x  [ a , x ])
                                                     {x} {y} x<y 
                                                       <To<⁻ _ _ (↓+Monotone< (F a) x y x<y))) p) 
                                    (acc-helper a y (s [ a , y ]
                                                       (<To<⁻ (F a ↓+ y) (F a ↓+ x)
                                                              (↓+Monotone< (F a) y x my)))))                                                           ,
                                  <To<⁻ (F a ↓+ y) (F a ↓+ x) (↓+Monotone< (F a) y x my) ))

  ⋃-isLeastUpperBound : (X : MEWO )  ((a : A)  F a  X)    X
  ⋃-isLeastUpperBound X ub =
    ≤CharacterisationFrom  X
      (elimProp  x  isPropPropTrunc)
                 (a , x)   f a x ,
                               ⋃↓[] a x  f-preserves-↓ a x ,
                               ∥-∥rec (isPropMarked X (f a x))
                                      (a' , x' , ax=a'x' , mx') 
                                         subst (marked X)
                                               (↓+Injective X (f a' x')
                                                              (f a x)
                                                              (sym (f-preserves-↓ a' x') 
                                                               ~-effective a' a x' x (sym ax=a'x') 
                                                               f-preserves-↓ a x))
                                               (f-preserves-marking a' x' mx')) ))
    where
      f : (a : A)   F a    X 
      f a x = fst (ub a) x

      f-preserves-↓ : (a : A)  (x :  F a )  F a ↓+ x  X ↓+ (f a x)
      f-preserves-↓ a x = simulationsPreserve↓ (F a) X (f a) (snd (ub a)) x

      f-preserves-marking : (a : A)  (x :  F a )  marked (F a) x  marked X (f a x)
      f-preserves-marking a x = snd (fst (snd (ub a)))