----------------------------------------------------------------------------------------------------
-- Translation between covered marked EWOs and Aczel's V
----------------------------------------------------------------------------------------------------

{-# OPTIONS --cubical --safe --lossy-unification #-}

module MEWO.TranslationV where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
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 Cubical.HITs.CumulativeHierarchy.Base as V

open import PropTrunc
open import Cubical.HITs.PropositionalTruncation.Base

open import Iff
open import General-Properties

open import MEWO.Base
open import MEWO.Covered
open import MEWO.Constructions


{- V as an extensional, wellfounded order -}

_∈₀_ : V   V   Type (ℓ-suc )
A ∈₀ B = typ (A  B)

isEWO⟨∈₀⟩ : isEWO (_∈₀_ { = })
isEWO⟨∈₀⟩ { = } =  A B  str (A  B)) , e , w
  where
    e : isExtensional _∈₀_
    e = V.elimProp
          {Z = λ a  (b : V )  ((c : V )  (c ∈₀ a  c ∈₀ b))  a  b}
           a  isPropΠ2  b _  setIsSet a b))
           A f ihAf  V.elimProp {Z = λ b  ((c : V )  (c ∈₀ sett A f  c ∈₀ b))  sett A f  b}
                                    b  isProp→ (setIsSet (sett A f) b))
                                    B g ihBg ext  seteq A B f g
                                       ((λ a  fst (ext (f a))  a , refl ∣₁) ,
                                         b  snd (ext (g b))  b , refl ∣₁))))
    w : isWellFounded _∈₀_
    w = V.elimProp isPropAcc
                    A f ih  acc  b b<a  ∥-∥rec (isPropAcc b)
                                                     (a , fa≡b)  subst (Acc _∈₀_)
                                                                          fa≡b
                                                                          (ih a))
                                                    (fromLib∥-∥ b<a)))

V-as-MEWO : ( : Level)  MEWO (ℓ-suc )
V-as-MEWO  = (V  , (_∈₀_ , λ _  Unit* , isPropUnit*) , isEWO⟨∈₀⟩)

{- V to MEWOcov -}

ψ : V   MEWOcov 
ψ { = } = V.elim {isSetZ = λ _  isSet⟨MEWOcov⟩} (record { ElimSett = pt ; ElimEq = eq })
  where
   pt :  {} (A : Type ) (f : A  V )  (ih : (a : A)  MEWOcov )  MEWOcov 
   pt A f ih =  A  a  fst (csucc (ih a))) , ⋃-covered A _  a  snd (csucc (ih a)))
   eq :  {} (A B : Type ) (f : A  V ) (g : B  V ) 
        eqImage f g  (ihf : (a : A)  MEWOcov )  (ihg : (b : B)  MEWOcov ) 
        ((a : A)   Σ (fiber g (f a))  y  ihg (fst y)  ihf a) ∥₁) 
        ((b : B)   Σ (fiber f (g b))  y  ihf (fst y)  ihg b) ∥₁) 
        pt A f ihf  pt B g ihg
   eq A B f g f~g ihf ihg p q =
     Σ≡Prop isProp⟨isCovered⟩
            (≤Antisymmetry (fst (pt A f ihf))
                           (fst (pt B g ihg))
                           (lemma A B f g ihf ihg p)
                           (lemma B A g f ihg ihf q))
     where
       lemma :  A B f g ihf ihg  ((a : A)   Σ (fiber g (f a))  y  ihg (fst y)  ihf a) ∥₁) 
               fst (pt A f ihf)  fst (pt B g ihg)
       lemma A B f g ihf ihg p =
         ⋃-isLeastUpperBound A _ (fst (pt B g ihg))
                              a  ∥-∥rec (isProp⟨≤⟩ (fst (csucc (ihf a))) (fst (pt B g ihg)))
                                           ((b , gb=fa) , ihgb=ihfa) 
                                            subst  z  fst (csucc z)  fst (pt B g ihg))
                                                  ihgb=ihfa
                                                  (⋃-isUpperBound B  b  fst (csucc (ihg b))) b))
                                          (fromLib∥-∥ (p a)))

{-
-- With `--lossy-unification`, the following typechecks
-- quickly. Without it, it takes seemingly forever.
ψ-comp : (A : Type ℓ) → (f : A → V ℓ) →
         ψ (sett A f) ≡ (⋃ A (λ a → fst (csucc (ψ (f a)))) ,
                         ⋃-covered A (λ a → fst (csucc (ψ (f a)))) λ a → snd (csucc (ψ (f a))))
ψ-comp A f = refl
-}

ψ-simulation : isSimulation (V-as-MEWO ) (MEWOcov-as-MEWO ) ψ
ψ-simulation { = } = existsSimulationsAreSimulations (V-as-MEWO ) (MEWOcov-as-MEWO ) ψ
                         (((λ {x} {y}  monotone x y) ,  p  p)) ,
                           {B} {A}  simul (fst B) (snd B) A))
  where
    ψgb<ψsBg-lemma :  B g b  fst (ψ (g b)) < fst (ψ (sett B g))
    ψgb<ψsBg-lemma B g b = [ b , inr tt ] ,
                            b , inr tt , refl , tt*  ,
                           sym (⋃↓[] B  b  fst (csucc (ψ (g b)))) b (inr tt) 
                                ↓+inr (fst (ψ (g b))) (snd (ψ (g b))))

    monotone : (x y : V )  x ∈₀ y  ψ x <c ψ y
    monotone =
      V.elimProp
         x  isPropΠ2  y _  isProp⟨<⟩ (fst (ψ x)) (fst (ψ y))))
         A f ihf  V.elimProp
                        y  isProp→ (isProp⟨<⟩ (fst (ψ _)) (fst (ψ y))))
                        B g ihg x<y  ∥-∥rec (isProp⟨<⟩ _ _)
                                               (b , gb≡x) 
                                                   subst  z  fst (ψ z) < fst (ψ (sett B g)))
                                                         gb≡x
                                                         (ψgb<ψsBg-lemma B g b))
                                              (fromLib∥-∥ x<y)))

    simul : (B : MEWO )  (covB : isCovered B)  (A : V )  B < fst (ψ A) 
             Σ[ A'  V  ] (A' ∈₀ A × (ψ A'  (B , covB))) 
    simul B covB =
      V.elimProp
         A  isProp→ isPropPropTrunc)
         { A f ih (b , mb , eq) 
               Q.elimProp
                  {P = λ b  marked (fst (ψ (sett A f))) b 
                             B  (fst (ψ (sett A f)) ↓+ b) 
                              Σ (V )  A'  (A' ∈₀ sett A f) × (ψ A'  (B , covB))) }
                   b  isPropΠ2  _ _  isPropPropTrunc))
                   { (a , p) mb eq 
                    ∥-∥map  { (a' , inr tt , qq , tt*) 
                                 f a' ,
                                  a' , refl ∣₁ ,
                                 Σ≡Prop isProp⟨isCovered⟩
                                        (sym (eq 
                                              ⋃↓[] A  a  fst (csucc (ψ (f a)))) a p 
                                              ~-effective A  a  fst (csucc (ψ (f a))))
                                                          a a' p (inr tt) qq 
                                              ↓+inr (fst (ψ (f a')))
                                                    (snd (ψ (f a'))))) }) mb }) b mb eq })

{- MEWOcov to V -}

φ-wf : (A : MEWO )  (covA : isCovered A)  Acc _<c_ (A , covA)  V 
φ-wf A covA (acc s) =
  sett (Σ[ a   A  ] marked A a)
        (a , ma)  φ-wf (A ↓+ a) (initialSegmentsCovered A a) (s _ (a , ma , refl)))

φ : MEWOcov   V 
φ { = } (A , covA) = φ-wf A covA (wellfounded (MEWOcov-as-MEWO ) (A , covA))

φ-wf-comp : (A : MEWO )  (covA : isCovered A)  (a : Acc _<c_ (A , covA)) 
            φ-wf A covA a  φ (A , covA)
φ-wf-comp A covA (acc s) =
  cong (sett (Σ[ a   A  ] marked A a))
       (funExt λ { (a , ma)  cong (φ-wf (A ↓+ a) (initialSegmentsCovered A a))
                                   (isPropAcc ((A ↓+ a) , initialSegmentsCovered A a) _ _) })

φ-comp : (A : MEWO )  (covA : isCovered A) 
         φ (A , covA)  sett (Σ[ a   A  ] marked A a)
                              (a , ma)  φ ((A ↓+ a) , initialSegmentsCovered A a))
φ-comp A covA = cong (sett (Σ[ a   A  ] marked A a))
                     (funExt  (a , ma)  φ-wf-comp (A ↓+ a) (initialSegmentsCovered A a) _))

φ-simulation : isSimulation (MEWOcov-as-MEWO ) (V-as-MEWO ) φ
φ-simulation { = } =
  existsSimulationsAreSimulations (MEWOcov-as-MEWO )
                                  (V-as-MEWO )
                                  φ
                                  (((λ {(A , cA)} {(B , cB)}  monotone A cA B cB) ,  p  p)) ,
                                    {B} {A}  simul B (fst A) (snd A)))
  where
    monotone : (A : MEWO )  (covA : isCovered A)  (B : MEWO )  (covB : isCovered B) 
               A < B  φ (A , covA) ∈₀ φ (B , covB)
    monotone A covA B covB (b , mb , A≡B↓b) =
      subst  z  φ (A , covA) ∈₀ z)
            (sym (φ-comp B covB))
             (b , mb) , cong φ (Σ≡Prop isProp⟨isCovered⟩ (sym A≡B↓b)) ∣₁

    simul : (B : V )  (A : MEWO )  (covA : isCovered A)  B ∈₀ φ (A , covA) 
             Σ[ A'  MEWOcov  ] (A' <c (A , covA) × (φ A'  B)) 
    simul B A covA B∈φA =
      ∥-∥map  ((a , ma) , φA↓a≡B)  (A ↓+ a ,
                                      initialSegmentsCovered A a) ,
                                      (a , ma , refl) ,
                                      sym (φ-wf-comp (A ↓+ a) (initialSegmentsCovered A a) _) 
                                      φA↓a≡B)
            (fromLib∥-∥ B∈φA)

{- MEWOcov equals V -}

MEWOcov≡V : MEWOcov-as-MEWO   V-as-MEWO 
MEWOcov≡V { = } = ≤Antisymmetry (MEWOcov-as-MEWO )
                                 (V-as-MEWO )
                                 (φ , φ-simulation)
                                 (ψ , ψ-simulation)

V≡MEWOcov : V-as-MEWO   MEWOcov-as-MEWO 
V≡MEWOcov = sym MEWOcov≡V