open import Relation.Binary.PropositionalEquality using (_≑_)
open import Data.Product

postulate

  β–Έ : Set β†’ Set
  K : Set

π•Œ : Set₁
π•Œ = Set

β„™ : Set₁
β„™ = Set

record Preorder : Set₁ where
  field
    X   : π•Œ
    _βŠ‘_ : X β†’ X β†’ β„™
    refl : βˆ€ (x : X) β†’ x βŠ‘ x
    trans : βˆ€ {x y z : X} β†’ x βŠ‘ y β†’ y βŠ‘ z β†’ x βŠ‘ z

infixr 20 _⇨_
infixr 20 _β‡’_

record _⇨_ (X : Preorder) (Y : Preorder) : Set where
  module X = Preorder X
  module Y = Preorder Y
  field
    f   : X.X β†’ Y.X
    mon : βˆ€ {x y} β†’ X._βŠ‘_ x y β†’ Y._βŠ‘_ (f x) (f y)

app : βˆ€ {X Y} β†’ (X ⇨ Y) β†’ Preorder.X X β†’ Preorder.X Y
app = _⇨_.f

_$_ = app

_β‡’_ : Preorder β†’ Preorder β†’ Preorder
X β‡’ Y = record { X = X ⇨ Y
               ; _βŠ‘_ = Ξ» f g β†’ (x : X.X) β†’ _⇨_.f f x βŠ‘y _⇨_.f g x
               ; refl = Ξ» x x₁ β†’ _⇨_.mon x (X.refl x₁)
               ; trans = Ξ» p1 p2 x β†’ Y.trans (p1 x) (p2 x) }
  where
    module X = Preorder X
    module Y = Preorder Y
    _βŠ‘y_ = Y._βŠ‘_

_⊨_βŠ‘_ : (X : Preorder) β†’ Preorder.X X β†’ Preorder.X X β†’ Set
X ⊨ x βŠ‘ x' = Preorder._βŠ‘_ X x x'

record _⊨_≣_ (X : Preorder) (x y : Preorder.X X) : Set where
  module X = Preorder X
  _βŠ‘_ = X._βŠ‘_
  field
    to  : x βŠ‘ y
    fro : y βŠ‘ x

record _⇔_ (X : Preorder) (Y : Preorder) : Set where
  field
    to  : X ⇨ Y
    fro : Y ⇨ X
    eqX : βˆ€ x β†’ X ⊨ app fro (app to x) ≣ x
    eqY : βˆ€ y β†’ Y ⊨ app to (app fro y) ≣ y

record _β—ƒ_ (X Y : Preorder) : Set where
  _βŠ‘y_ = Preorder._βŠ‘_ Y
  field
    emb  : X ⇨ Y
    prj  : Y ⇨ X
    projection : βˆ€ y β†’ Y ⊨ app emb (app prj y) βŠ‘ y
    retraction : βˆ€ x β†’ X ⊨ x ≣ app prj (app emb x)

op : Preorder β†’ Preorder
op X = record
         { X = X.X
         ; _βŠ‘_ = Ξ» x y β†’ y X.βŠ‘ x
         ; refl = X.refl
         ; trans = Ξ» p1 p2 β†’ X.trans p2 p1
         }
  where module X = Preorder X

opF : βˆ€ {X Y} β†’ (X ⇨ Y) β†’ op X ⇨ op Y
opF {X}{Y} f = record { f = f.f ; mon = _⇨_.mon f }
  where module X = Preorder X
        module Y = Preorder Y
        module f = _⇨_ f

product : Preorder β†’ Preorder β†’ Preorder
product X Y = record { X = X.X Γ— Y.X
                     ; _βŠ‘_ = Ξ» p1 p2 β†’ (proj₁ p1 βŠ‘x proj₁ p2) Γ— (projβ‚‚ p1 βŠ‘y projβ‚‚ p2)
                     ; refl = Ξ» x β†’ (X.refl (proj₁ x)) , (Y.refl (projβ‚‚ x))
                     ; trans = Ξ» leq1 leq2 β†’ (X.trans (proj₁ leq1) (proj₁ leq2)) , Y.trans (projβ‚‚ leq1) (projβ‚‚ leq2)
                     }
  where module X = Preorder X
        _βŠ‘x_ = X._βŠ‘_
        module Y = Preorder Y
        _βŠ‘y_ = Y._βŠ‘_

record FiberPts {X : Preorder}{Y : Preorder} (f : X ⇨ Y) (y : Preorder.X Y) : Set where
  field
    pt : Preorder.X X
    over : _⇨_.f f pt ≑ y

Fiber : {X : Preorder}{Y : Preorder} (f : X ⇨ Y) (y : Preorder.X Y) β†’ Preorder
Fiber {X}{Y} f y = record { X = FiberPts f y
                   ; _βŠ‘_ = Ξ» x x' β†’ FiberPts.pt x βŠ‘x FiberPts.pt x'
                   ; refl = Ξ» x β†’ X.refl (FiberPts.pt x)
                   ; trans = Ξ» p1 p2 β†’ X.trans p1 p2 }
 where module X = Preorder X
       _βŠ‘x_ = X._βŠ‘_
       module Y = Preorder Y

record fibration {X : Preorder} {Y : Preorder} (f : X ⇨ Y) : Set where
  module X = Preorder X
  module Y = Preorder Y
  _βŠ‘x_ = X._βŠ‘_
  _βŠ‘y_ = Y._βŠ‘_
  module f = _⇨_ f
  field
    -- A < B -> tm B -> tm A (downcast)
    pull : βˆ€ (x : X.X) {y : Y.X} β†’ (y βŠ‘y app f x) β†’ X.X

    -- the downcast is a lower bound
    -- dncast (A < B) N <= N
    pullLB : βˆ€ {x : X.X} {y : Y.X} β†’ (c : y βŠ‘y app f x) β†’ pull x c βŠ‘x x

    -- the downcast is the *greatest* lower bound over a type at least as low
    -- Given N : B
    -- and M' : A' where A' <= A <= B
    -- and M' <= N over A' <= A <= B
    -- then M' <= dncast (A <= B) N over A' <= A
    pullGLB : βˆ€ {x : X.X} {y : Y.X} {x' : X.X} β†’ (c : y βŠ‘y app f x) β†’ (app f x' βŠ‘y y) β†’ (x' βŠ‘x x) β†’ x' βŠ‘x pull x c

opfibration : βˆ€ {X Y} (f : X ⇨ Y) β†’ Set
opfibration f = fibration (opF f)

record GLTC : Set₁ where
  field
    type : Preorder
  module type = Preorder type
  _βŠ‘ty_ = type._βŠ‘_

  field
    term : Preorder
    type-of : term ⇨ type

    dncasts : fibration   type-of
    upcasts : opfibration type-of

    -- need that the dncast of an upcast is the identity(!)
    -- projection : {!!}

  module term = Preorder term
  module type-of = _⇨_ type-of
  _βŠ‘tm_ = term._βŠ‘_

  -- dynamic type
  field
    dyn : type.X
    dynT : βˆ€ A β†’ A βŠ‘ty dyn

  of-ty : type.X β†’ Preorder
  of-ty A = Fiber type-of A

  -- errors
  field
    err : βˆ€ A β†’ Preorder.X (of-ty A)
    -- errβŠ₯ : βˆ€ M β†’
    -- can we define err to be the least element of type dyn which then is then
    -- err <= up (M) so dn(err) <= dn(up(M))
    

  -- function types
  field
    arr : type ⇨ type β‡’ type
  arr' : type.X β†’ type.X β†’ type.X
  arr' A B = app (app arr A) B
  field
    lam : βˆ€ {A B} β†’ (of-ty A β‡’ of-ty B) ⇔ of-ty (arr' A B)
    

  -- can we *prove* that application preserves error, i.e., that (err{A -> B} N = err{B})?
  -- doubtful... seems like we need to add it in as an axiom, i.e., that the above is an iso of *pointed* preorders

  -- boolean types
  field
    bool : type.X
     -- this doesn't satisfy the UMP because
     -- there are terms that are not strict in their input (x |- x) 
    if : βˆ€ {A} β†’ product (of-ty A) (of-ty A) β—ƒ (of-ty bool β‡’ of-ty A)
    
    
--     -- terms are more interesting because they are "clocked"
--     term : type β†’ K β†’ Set
--     _||_⊨_βŠ‘β‚_ : βˆ€ {A B : type} β†’ (A βŠ‘β‚€ B) β†’ (k : K) β†’ term A k β†’ term B k β†’ β„™
--     -- reflexivity is "approximation-wise"
--     refl₁   : βˆ€ {A}{M : βˆ€ k β†’ term A k} β†’ (k : K) β†’ reflβ‚€ || k ⊨ (M k) βŠ‘β‚ (M k)
--     -- transitivity is only "in the limit"
--     trans₁  : βˆ€ {A B C}{M : βˆ€ k β†’ term A k}{N : βˆ€ k β†’ term B k}{P : βˆ€ k β†’ term C k}
--             {AB : A βŠ‘β‚€ B}{BC : B βŠ‘β‚€ C}
--             β†’ (βˆ€ k β†’ AB || k ⊨ (M k) βŠ‘β‚ (N k))
--             β†’ (βˆ€ k β†’ BC || k ⊨ (N k) βŠ‘β‚ (P k))
--             β†’ βˆ€ k β†’ transβ‚€ AB BC || k ⊨ (M k) βŠ‘β‚ (P k)

--     -- the above defines a kind of "guarded functor" ty : term -> type

--     -- upcasts/downcasts ask that that functor be an/a opfibration/fibration
--     up : βˆ€ {A B} β†’ A βŠ‘β‚€ B β†’ βˆ€ k β†’ term A k β†’ term B k
    
  
--     dn : βˆ€ {A B} β†’ A βŠ‘β‚€ B β†’ βˆ€ k β†’ term B k β†’ term A k

-- postulate
--   ▸₁ : Set₁ β†’ Set₁
--   fix : (▸₁ π•Œ β†’ π•Œ) β†’ π•Œ
--   ΞΈπ•Œ : ▸₁ π•Œ β†’  π•Œ

-- infixl 30 _+_
-- data _+_ (A B : Set) : Set where
--   inl_ : A β†’ A + B
--   inr_ : B β†’ A + B

-- record One : Set where
--   constructor ⟨⟩

-- Two : Set
-- Two = One + One

-- L℧ : Set β†’ Set
-- L℧ X = fix (Ξ» L℧X β†’ One + X + ΞΈπ•Œ L℧X)

-- dyn℧ : Set
-- dyn℧ = fix Ξ» dyn℧ β†’ L℧ ((Two + (ΞΈπ•Œ dyn℧ β†’ ΞΈπ•Œ dyn℧)))

record GTLC-CBV : Set₁ where
  field
    type : Preorder
    valu : Preorder
    comp : Preorder
    ty-ofv : valu ⇨ type
    ty-ofc : comp ⇨ type

  module type = Preorder type

  val-of-ty : type.X β†’ Preorder
  val-of-ty A = Fiber ty-ofv A
  comp-of-ty : type.X β†’ Preorder
  comp-of-ty A = Fiber ty-ofc A

  field
    -- not quite right, need the rhs to be some kind of strict morphisms.
    -- should probably have a third sort of ev ctxts from A to B
    lett : βˆ€ {A B} β†’ (val-of-ty A β‡’ comp-of-ty B) ⇔ (comp-of-ty A β‡’ comp-of-ty B)
    
    upcasts : opfibration ty-ofv
    dncasts :   fibration ty-ofc -- problem this doesn't imply that downcasts are linear, maybe we add this as a separate prop?
    -- something for projection property

    -- dynamic type
    dyn : type.X
    dyn⊀ : βˆ€ A β†’ type ⊨ A βŠ‘ dyn

    -- errors...

    -- functions
    arr : type ⇨ type β‡’ type
  arr' : type.X β†’ type.X β†’ type.X
  arr' A B = app (app arr A) B
  field
    lam : βˆ€ {A B} β†’ (val-of-ty A β‡’ comp-of-ty B) ⇔ val-of-ty (arr' A B)

    -- bools
    bool : type.X
    if :  βˆ€ {A} β†’ product (comp-of-ty A) (comp-of-ty A) ⇔ (val-of-ty bool β‡’ comp-of-ty A)