-- A partial inductive-recursive definition of the lifting
-- construction on ω-cpos, without path or truncation constructors, in
-- order to get the basics right

-- The code in this module is based on a suggestion from Paolo
-- Capriotti.

{-# OPTIONS --without-K #-}

open import Omega-cpo

module Lifting.Preliminary-sketch {} (cpo : ω-cpo  ) where

open import Prelude hiding ()

  module CPO = ω-cpo cpo

-- The carrier type (Carrier) and the information ordering (_⊑_) are
-- defined as a single inductive family D. A boolean index is used to
-- separate the two types. I (NAD) think that Conor McBride once
-- pointed out that inductive-inductive types can be encoded as
-- inductive-recursive types in (roughly) the following way.

I : Bool  Set 

data D : (b : Bool)  I b  Set 

infix 4 _⊑_

Carrier : Set 
_⊑_     : Carrier  Carrier  Set 

-- Carrier is not indexed, but _⊑_ is indexed by two values of type
-- Carrier.

I true  =  _ 
I false = Carrier × Carrier

Carrier = D true _

x  y = D false (x , y)

-- Increasing sequences.

Increasing-sequence : Set 
Increasing-sequence =  λ (f :   Carrier)   n  f n  f (suc n)

-- Projection functions for Increasing-sequence.

infix 30 _[_]

_[_] : Increasing-sequence    Carrier
_[_] = proj₁

increasing : (s : Increasing-sequence)   n  s [ n ]  s [ suc n ]
increasing = proj₂

-- Upper bounds.

Is-upper-bound : Increasing-sequence  Carrier  Set 
Is-upper-bound s x =  n  s [ n ]  x

-- _⊥ and _⊑_.

data D where
  never : Carrier
  now   : CPO.Carrier  Carrier
       : Increasing-sequence  Carrier

  ⊑-refl            :  x  x  x
  ⊑-trans           :  x y z  x  y  y  z  x  z
  never⊑            :  x  never  x
  upper-bound       :  s  Is-upper-bound s ( s)
  least-upper-bound :  s ub  (is-ub : Is-upper-bound s ub)   s  ub
  now-mono          :  {x y}  x CPO.⊑ y  now x  now y
  now-⨆′            :  s 
                      now (CPO.⨆ s)   (Σ-map (now ∘_) (now-mono ∘_) s)

-- Predicate transformer related to increasing sequences.

Inc :  {p q}
      (P : Carrier  Set p) 
      (∀ {x y}  P x  P y  x  y  Set q) 
      Increasing-sequence  Set (p  q)
Inc P Q s =
   λ (p :  n  P (s [ n ])) 
     n  Q (p n) (p (suc n)) (increasing s n)

-- Record wrapping up the eliminators' arguments.

record Rec-args
         {p q}
         (P : Carrier  Set p)
         (Q :  {x y}  P x  P y  x  y  Set q) :
         Set (  p  q) where
    pe : P never
    po :  x  P (now x)
    pl :  s (pq : Inc P Q s)  P ( s)
    qr :  x (p : P x)  Q p p (⊑-refl x)
    qt :  {x y z}
         (x⊑y : x  y) (y⊑z : y  z)
         (p-x : P x) (p-y : P y) (p-z : P z) 
         Q p-x p-y x⊑y  Q p-y p-z y⊑z 
         Q p-x p-z (⊑-trans x y z x⊑y y⊑z)
    qe :  x (p : P x)  Q pe p (never⊑ x)
    qu :  s (pq : Inc P Q s) n 
         Q (proj₁ pq n) (pl s pq) (upper-bound s n)
    ql :  s ub is-ub (pq : Inc P Q s) (pu : P ub)
         (qu :  n  Q (proj₁ pq n) pu (is-ub n)) 
         Q (pl s pq) pu (least-upper-bound s ub is-ub)
    qm :  {x y} (le : x CPO.⊑ y) 
         Q (po x) (po y) (now-mono le)
    q⨆ :  s 
         Q (po (CPO.⨆ s))
           (pl (Σ-map (now ∘_) (now-mono ∘_) s)
               (  n  po (s CPO.[ n ]))
               ,  n  qm (CPO.increasing s n))
           (now-⨆′ s)

-- Mutually defined dependent eliminators.

module _
  {p q}
  {P : Carrier  Set p}
  {Q :  {x y}  P x  P y  x  y  Set q}
  (args : Rec-args P Q)

  open Rec-args args

  ⊥-rec   : (x : Carrier)  P x
  inc-rec : (s : Increasing-sequence)  Inc P Q s
  ⊑-rec   :  {x y} (x⊑y : x  y)  Q (⊥-rec x) (⊥-rec y) x⊑y

  ⊥-rec never   = pe
  ⊥-rec (now x) = po x
  ⊥-rec ( s)   = pl s (inc-rec s)

  inc-rec (s , inc) = (  n  ⊥-rec (s   n))
                      ,  n  ⊑-rec (inc n))

  ⊑-rec (⊑-refl x)                     = qr x (⊥-rec x)
  ⊑-rec (⊑-trans x y z x⊑y y⊑z)        = qt x⊑y y⊑z
                                            (⊥-rec x) (⊥-rec y) (⊥-rec z)
                                            (⊑-rec x⊑y) (⊑-rec y⊑z)
  ⊑-rec (never⊑ x)                     = qe x (⊥-rec x)
  ⊑-rec (upper-bound s n)              = qu s (inc-rec s) n
  ⊑-rec (least-upper-bound s ub is-ub) = ql s ub is-ub
                                            (inc-rec s) (⊥-rec ub)
                                             n  ⊑-rec (is-ub n))
  ⊑-rec (now-mono le)                  = qm le
  ⊑-rec (now-⨆′ s)                     = q⨆ s