{-

What we do here is set up a universe which is closed under an
operation assigning to each of a rather wide class of predicate
transformers its greatest fixed point.

A predicate transformer over a set S can be given by a function  
from S to quantifiers over S, that is, to predicates
of predicates over S. (Just swap the arguments.) 
So we can delimit a class of predicate transformers by 
delimiting a class of quantifiers.

There are really two classes of quantifiers here:

 - the first is given inductively: we have 
   * the "quantifier" which applies a predicate to a given 
     value in its domain
   * the constant "quantifier" which maps all predicates to a given 
     proposition
   and we close these under Pi and Sigma.
   So we have certain quantifier codes.
   See the definition QuanCode.

 - the second is given explicitly: a quantifier is
   given in "disjunctive normal form" (DNF) by a
   family of families.  

In fact, the second class is more general. 
We can express each of the inductively defined
class QuanCode in DNF. 


-}

Pow (A :: Type) :: Type = A -> Set
N0 :: Set = data
N1 :: Set = data zo
starN1 :: N1 = zo@_

Pi (A :: Set) (B :: Pow A) :: Set 
         = (x :: A) -> B x

Si (A :: Set) (B :: Pow A) :: Set 
         = sig { fst :: A ; snd :: B fst; }

package Coalg where
  mutual

    U :: Set 
          = data pi   (Ah :: U) (Bh :: pow (T Ah))
               | si   (Ah :: U) (Bh :: pow (T Ah))
               | n0
               | n1
               | gfix (Sh  :: U) 
                      (phi :: T Sh -> Quancode Sh) 
                      (s   :: T Sh)
               | path (Sh  :: U) 
                      (phi :: T Sh -> Quancode Sh) 
                      (s   :: T Sh) 
                      (a   :: GFix Sh phi s)

    pow (A :: Set) :: Set = A -> U

    T (u :: U) :: Set 
          = case u of 
              (pi Ah Bh) -> Pi (T Ah) (\(a :: T Ah) -> T (Bh a))
              (si Ah Bh) -> Si (T Ah) (\(a :: T Ah) -> T (Bh a))
              (n0)       -> N0
              (n1)       -> N1
              (gfix Sh phi s)   -> GFix Sh phi s
              (path Sh phi s a) -> Path Sh phi s a

  
    n1 :: U  = n1@_
    n0 :: U  = n0@_

    pi (Ah :: U) (Bh :: pow (T Ah)) :: U =  pi@U Ah Bh
    si (Ah :: U) (Bh :: pow (T Ah)) :: U =  si@U Ah Bh 
    

    Quancode (Sh :: U) :: Set 
        = data star   (a  :: T Sh)
             | pi     (Bh :: U) (f :: T Bh -> Quancode Sh)
             | sigma  (Bh :: U) (f :: T Bh -> Quancode Sh)
             | const  (Bh :: U) 

    gfix  (Sh  :: U)
          (phi :: T Sh -> Quancode Sh)
          (a   :: T Sh)
      :: U
      = gfix@_ Sh phi a

    {------------- A quantifier is a predicate of predicates ---------------}

    Quantifier (A :: Set) :: Set = pow (pow A)

    {- We can directly interpret a quantifier code as a quantifier -}
    Quancode2Quantifier (Sh :: U)                        
                        (cd :: Quancode Sh) 
      :: Quantifier (T Sh)
      = \(Xh :: pow (T Sh)) ->
        case cd of 
         (star a)     -> Xh a
         (pi Bh f)    -> pi Bh (\(b :: T Bh) -> Quancode2Quantifier Sh (f b) Xh)
         (sigma Bh f) -> si Bh (\(b :: T Bh) -> Quancode2Quantifier Sh (f b) Xh)
         (const Bh)   -> Bh
    
    Quantify 
         (Sh :: U)
         (cd :: Quancode Sh) 
         (Xh :: pow (T Sh))
       :: Set
       = T (Quancode2Quantifier Sh cd Xh)
    
    Pt (X :: Set) :: Set = pow X -> pow X      -- predicate transformer

    {- This is how a function to quantifiers from their domain 
       determines a predicate transformer. (Swap the arguments.) -}
    IQuantifier2Pt (X :: Set) 
                   (f :: X -> Quantifier X)    -- indexed quantifier
       :: Pt X
       = \(Ph :: pow X) -> \(x :: X) -> f x Ph

    {---------------------------------------------------------------------}

    fam    (A :: Set) :: Set = Si U (\(Xh :: U) -> T Xh -> A)

    famfam (A :: Set) :: Set = fam (fam A)

    famfam2Quantifier (A :: Set) 
                      (ff :: famfam A) 
       :: Quantifier A
       = let C  :: U                       = ff.fst 
             C' :: T C -> fam A            = ff.snd
             R (c :: T C) :: U             = (C' c).fst 
             n (c :: T C) :: T (R c) -> A  = (C' c).snd 
         in  \(Xh :: pow A) ->    
             si C (\(c :: T C) -> 
                pi (R c) (\(r :: T (R c)) -> 
                   Xh (n c r)))

    Ifamfam2Pt (A :: Set) 
               (f :: A -> famfam A)     -- "code" of a pt.
       :: Pt A
       = IQuantifier2Pt A (\(a :: A) -> famfam2Quantifier A (f a))

    cmd' (Sh :: U)
         (cd :: famfam (T Sh))
       :: U
       = cd.fst
    
    Cmd' (Sh :: U)
         (cd :: famfam (T Sh))
       :: Set
       = T cd.fst

    rsp' (Sh :: U)
         (cd :: famfam (T Sh))
         (r  :: Cmd' Sh cd)
       :: U
       = (cd.snd r).fst

    Rsp' (Sh :: U)
         (cd :: famfam (T Sh))
         (c  :: Cmd' Sh cd)
       :: Set
       = T (rsp' Sh cd c)

    nxt' (Sh :: U) 
        (cd :: famfam (T Sh))
        (c  :: Cmd' Sh cd) 
        (r  :: Rsp' Sh cd c)
      :: T Sh
      = (cd.snd c).snd r
    
    {-----------------------------------------------------------------------}
    {- Express each of the inductively defined class of quantifiers in DNF -}

    cmd (Sh :: U)
        (cd :: Quancode Sh) 
      :: U
      = case cd of 
          (star a)     -> n1
          (pi Bh f)    -> pi Bh (\(h :: T Bh) -> cmd  Sh (f h))
          (sigma Bh f) -> si Bh (\(h :: T Bh) -> cmd  Sh (f h))
          (const Bh)   -> Bh 

    Cmd (Sh :: U)
        (cd :: Quancode Sh) 
      :: Set
      = T (cmd Sh cd)
        
    rsp (Sh :: U)
        (cd :: Quancode Sh)
        (r  :: Cmd Sh cd)
      :: U
      = case cd of 
          (star a)     -> n1 
          (pi Bh f)    -> si Bh (\(b :: T Bh) ->  rsp Sh (f b) (r b))
          (sigma Bh f) -> rsp Sh (f r.fst) r.snd 
          (const Bh)   -> n0

    Rsp (Sh :: U)
        (cd :: Quancode Sh)
        (r  :: Cmd Sh cd)
      :: Set
      = T (rsp Sh cd r)

    nxt (Sh :: U) 
        (cd :: Quancode Sh) 
        (c  :: Cmd Sh cd) 
        (r  :: Rsp Sh cd c)
      :: T Sh
      = case cd of 
          (star a)     -> a
          (pi Bh f)    -> nxt Sh (f r.fst) (c r.fst) r.snd 
          (sigma Bh f) -> nxt Sh (f c.fst) c.snd r         
          (const Bh)   -> case r of { }

    Quancode2famfam (Sh :: U)
                    (cd :: Quancode Sh) 
      :: famfam (T Sh)
      = struct 
          fst = cmd Sh cd
          snd = \(c :: T fst) -> 
                struct  fst = rsp Sh cd c
                        snd = nxt Sh cd c

    {- This gives us another (indirect) way of interpreting 
       quantifier codes as quantifiers. -}
    Quancode2Quantifier' 
         (Sh :: U)
         (cd :: Quancode Sh) 
      :: Quantifier (T Sh)
      = famfam2Quantifier (T Sh) (Quancode2famfam Sh cd)

    {-----------------------------------------------------------------------}

    {- To each code for a predicate transformer, we associate
       its greatest fixed point. 

       In fact, everything here here and below works via
       the DNF form of a quantifier, given above. 
    -}
    GFix (Sh  :: U)
         (phi :: T Sh -> Quancode Sh)
         (s   :: T Sh)
      :: Set
      = sig pos :: pow (T Sh)
            c   :: (a :: T Sh) -> 
                   T (pos a) -> Cmd Sh (phi a)
            n   :: (a :: T Sh) ->
                   (b :: T (pos a)) -> 
                   (r :: Rsp Sh (phi a) (c a b)) -> 
                   T (pos (nxt Sh (phi a) (c a b) r))
            b   :: T (pos s)  


    {- Extract the carrier predicate. -}
    GFix2pos (Sh  :: U)
             (phi :: T Sh -> Quancode Sh)
             (s   :: T Sh)
             (a   :: GFix Sh phi s)
             (s'  :: T Sh)
      :: U
      = a.pos s'

    Coalg  (Sh  :: U)        
           (phi :: T Sh -> famfam (T Sh))  
      :: Set 
      = sig carrier :: pow (T Sh)
            morph   :: (a :: T Sh) -> 
                       T (carrier a) -> 
                       T (Ifamfam2Pt (T Sh) phi carrier a)    

    GFix'  (Sh  :: U)                          -- GFix, rereformulated
           (phi :: T Sh -> famfam (T Sh))  
      :: Pow (T Sh)   
      = \(a :: T Sh) -> 
        sig ca      :: Coalg Sh phi 
            b       :: T (ca.carrier a)  

    GFix'2pos (Sh  :: U)
              (phi :: T Sh -> famfam (T Sh))
              (s   :: T Sh)
              (a   :: GFix' Sh phi s)
              (s'  :: T Sh)
      :: U
      = a.ca.carrier s'

    {-----------------------------------------------------------------------}

    Path (Sh  :: U)
         (phi :: T Sh -> Quancode Sh)
         (s   :: T Sh)
         (a   :: GFix Sh phi s)
         :: Set
      = data root
           | cons (p :: Path Sh phi s a) 
                  (r :: Rsp Sh (phi (path2state Sh phi s a p)) 
                               (path2cmd Sh phi s a p))              

    path2state 
         (Sh  :: U)
         (phi :: T Sh -> Quancode Sh)
         (s   :: T Sh)
         (a   :: GFix Sh phi s)
         (p   :: Path Sh phi s a)
         :: T Sh
      = case p of 
          (root)      -> s
          (cons p' r) -> nxt 
                         Sh 
                         (phi (path2state Sh phi s a p')) 
                         (path2cmd Sh phi s a p')
                         r

    path2cmd 
         (Sh  :: U)
         (phi :: T Sh -> Quancode Sh)
         (s   :: T Sh)
         (a   :: GFix Sh phi s)
         (p   :: Path Sh phi s a)
         :: Cmd Sh (phi (path2state Sh phi s a p))
      = a.c (path2state Sh phi s a p) 
            (path2pos   Sh phi s a p) 

    path2pos 
         (Sh  :: U)
         (phi :: T Sh -> Quancode Sh)
         (s   :: T Sh)
         (a   :: GFix Sh phi s)
         (p   :: Path Sh phi s a)
         :: T (GFix2pos Sh phi s a (path2state Sh phi s a p)) 
      = case p of 
          (root)      -> a.b
          (cons p' r) -> a.n (path2state Sh phi s a p') 
                             (path2pos   Sh phi s a p') r

    {-----------------------------------------------------------------------}
    {- Like the above, but a different coding of pt's. -}

    Path'
         (Sh  :: U)
         (phi :: T Sh -> famfam (T Sh))
         (s   :: T Sh)
         (a   :: GFix' Sh phi s)
         :: Set
      = data root
           | cons (p :: Path' Sh phi s a) 
                  (r :: Rsp' Sh (phi (path2state' Sh phi s a p)) 
                                (path2cmd' Sh phi s a p))              

    path2state'
         (Sh  :: U)
         (phi :: T Sh -> famfam (T Sh))
         (s   :: T Sh)
         (a   :: GFix' Sh phi s)
         (p   :: Path' Sh phi s a)
         :: T Sh
      = case p of 
          (root)      -> s
          (cons p' r) -> nxt' 
                         Sh 
                         (phi (path2state' Sh phi s a p')) 
                         (path2cmd' Sh phi s a p')
                         r

    path2cmd'
         (Sh  :: U)
         (phi :: T Sh -> famfam (T Sh))
         (s   :: T Sh)
         (a   :: GFix' Sh phi s)
         (p   :: Path' Sh phi s a)
         :: Cmd' Sh (phi (path2state' Sh phi s a p))
      = (a.ca.morph (path2state' Sh phi s a p) 
                    (path2pos'   Sh phi s a p)).fst 

    path2pos'
         (Sh  :: U)
         (phi :: T Sh -> famfam (T Sh))
         (s   :: T Sh)
         (a   :: GFix' Sh phi s)
         (p   :: Path' Sh phi s a)
         :: T (GFix'2pos Sh phi s a (path2state' Sh phi s a p)) 
      = case p of 
          (root)      -> a.b
          (cons p' r) -> (a.ca.morph (path2state' Sh phi s a p') 
                                     (path2pos' Sh phi s a p')).snd r 


  -- end of mutual


  

 
  

  quan'(Sh :: U)
       (cd :: Quancode Sh)
    :: Quantifier (T Sh)
    = Quancode2Quantifier' Sh cd

  Quan' (Sh :: U)
        (cd :: Quancode Sh) 
        (Xh :: pow (T Sh))
      :: Set
      = T (quan' Sh cd Xh)

  mutual

    Quan2Cmd
         (Sh :: U)
         (cd :: Quancode Sh) 
         (Xh :: pow (T Sh))
         (b  :: Quantify Sh cd Xh)
      :: Cmd Sh cd
      = case cd of 
          (star a)     ->  starN1
          (pi Bh f)    -> 
             \(x :: T Bh) -> Quan2Cmd Sh (f x) Xh (b x)
          (sigma Bh f) -> 
             struct 
               fst = b.fst
               snd = Quan2Cmd Sh (f b.fst) Xh b.snd
          (const Bh)   -> b

    Quan2Rsp
         (Sh :: U)
         (cd :: Quancode Sh) 
         (Xh :: pow (T Sh))
         (b  :: Quantify Sh cd Xh)
         (r  :: Rsp Sh cd (Quan2Cmd Sh cd Xh b))
      :: T (Xh (nxt Sh cd (Quan2Cmd Sh cd Xh b) r))
      = case cd of 
          (star a)     -> b
          (pi Bh f)    -> Quan2Rsp Sh (f r.fst) Xh (b r.fst) r.snd  
          (sigma Bh f) -> Quan2Rsp Sh (f b.fst) Xh b.snd r          
          (const Bh)   -> case r of { }

  -- end of mutual

  Quan2Quan'
         (Sh :: U)
         (cd :: Quancode Sh) 
         (Xh :: pow (T Sh))
         (b  :: Quantify Sh cd Xh)
      :: Quan' Sh cd Xh
      = struct 
          fst = Quan2Cmd Sh cd Xh b
          snd = Quan2Rsp Sh cd Xh b

  GFix2Cmd 
         (Sh  :: U)
         (phi :: T Sh -> Quancode Sh)
         (a   :: T Sh)
         (b   :: GFix Sh phi a)
      :: Cmd Sh (phi a)
      =  b.c a b.b

  GFix2nxt 
         (Sh  :: U)
         (phi :: T Sh -> Quancode Sh)
         (a   :: T Sh)
         (b'  :: GFix Sh phi a)
         (r   :: Rsp Sh (phi a) (GFix2Cmd Sh phi a b'))
      :: GFix Sh phi (nxt Sh (phi a) (GFix2Cmd Sh phi a b') r)
      = struct 
          pos = b'.pos 
          c   = b'.c 
          n   = b'.n 
          b   = b'.n a b'.b r 

  {--------------------------------------------------------}
  GFix'2Cmd 
         (Sh  :: U)
         (phi :: T Sh -> famfam (T Sh))
         (a   :: T Sh)
         (b   :: GFix' Sh phi a)
      :: Cmd' Sh (phi a)
      =  (b.ca.morph a b.b).fst

  GFix'2nxt 
         (Sh  :: U)
         (phi :: T Sh -> famfam (T Sh))
         (a   :: T Sh)
         (b'  :: GFix' Sh phi a)
         (r   :: Rsp' Sh (phi a) (GFix'2Cmd Sh phi a b'))
      :: GFix' Sh phi (nxt' Sh (phi a) (GFix'2Cmd Sh phi a b') r)
      = struct 
          ca = b'.ca;
          b = (b'.ca.morph a b'.b).snd r

  {--------------------------------------------------------}
  Quan'2Quanpre 
         (Sh :: U)
         (cd :: Quancode Sh) 
         (Xh :: pow (T Sh))
         (c  :: Cmd Sh cd)
         (h  :: (r :: Rsp Sh cd c) -> T (Xh (nxt Sh cd c r)))
      :: Quantify Sh cd Xh
      = case cd of 
          (star a)     -> h starN1
          (pi Bh f)    -> 
             \(x :: T Bh) ->
             Quan'2Quanpre Sh (f x) Xh (c x) 
                (\(r :: Rsp Sh (f x) (c x)) -> 
                 h (struct {fst = x ; snd = r }))
          (sigma Bh f) -> 
                struct
                  fst = c.fst
                  snd = Quan'2Quanpre Sh (f c.fst) Xh c.snd h 
          (const Bh)   -> c

  Quan'2Quan 
        (Sh :: U)
        (cd :: Quancode Sh) 
        (Xh :: pow (T Sh))
        (b  :: Quan' Sh cd Xh)
      :: Quantify Sh cd Xh
      = Quan'2Quanpre Sh cd Xh b.fst b.snd 


  GFix2Quan'GFix 
       (Sh  :: U)
       (phi :: T Sh -> Quancode Sh)
       (a   :: T Sh)
       (b   :: GFix Sh phi a)
    :: Quan' Sh (phi a) (gfix Sh phi)
    = struct 
        fst = GFix2Cmd Sh phi a b
        snd = GFix2nxt Sh phi a b

  GFix2QuanGFix 
       (Sh  :: U)
       (phi :: T Sh -> Quancode Sh)
       (a   :: T Sh)
       (b   :: GFix Sh phi a)
    :: Quantify Sh (phi a) (gfix Sh phi)
    = Quan'2Quan Sh (phi a) (gfix Sh phi) (GFix2Quan'GFix Sh phi a b)

  Quan'Coalg2Cmd 
            (Sh  :: U)
            (phi :: T Sh -> Quancode Sh)
            (Xh  :: pow (T Sh))
            (ar  :: (s' :: T Sh) -> 
                       T (Xh s') -> Quan' Sh (phi s') Xh)
            (a   :: T Sh)
            (h   :: T (Xh a))
    :: Cmd Sh (phi a)
    = (ar a h).fst 

  Quan'Coalg2X 
            (Sh  :: U)
            (phi :: T Sh -> Quancode Sh)
            (Xh  :: pow (T Sh))
            (ar  :: (s' :: T Sh) -> 
                       T (Xh s') -> Quan' Sh (phi s') Xh)
            (a   :: T Sh)
            (h   :: T (Xh a))
    :: (r :: Rsp Sh (phi a) (Quan'Coalg2Cmd Sh phi Xh ar a h)) ->
       T (Xh (nxt Sh (phi a) (Quan'Coalg2Cmd Sh phi Xh ar a h) r))
    =  (ar a h).snd

  Quan'Coalg2GFix 
            (Sh  :: U)
            (phi :: T Sh -> Quancode Sh)
            (Xh  :: pow (T Sh))
            (ar  :: (s' :: T Sh) -> 
                       T (Xh s') -> Quan' Sh (phi s') Xh)
            (s   :: T Sh)
            (x   :: T (Xh s))
    :: GFix Sh phi s
    = struct 
        pos = Xh
        c   = Quan'Coalg2Cmd Sh phi Xh ar 
        n   = Quan'Coalg2X Sh phi Xh ar 
        b   = x


  QuanCoalg2GFix 
            (Sh  :: U)
            (phi :: T Sh -> Quancode Sh)
            (Xh  :: pow (T Sh))
            (ar  :: (s' :: T Sh) -> 
                       T (Xh s') -> Quantify Sh (phi s') Xh)
            (s   :: T Sh)
            (x   :: T (Xh s))
    :: GFix Sh phi s
    = Quan'Coalg2GFix Sh phi Xh 
        (\(s' :: T Sh) -> 
         \(b  :: T (Xh s')) -> 
         Quan2Quan' Sh (phi s') Xh (ar s'  b)) 
        s 
        x