--#include "amenities.agda"
--#include "naturals.agda"
--#include "ordinals.agda"
--#include "nextU.agda"

{- This file, together with the files mentioned
   above, contains a proof of accessibility for Gamma0, 
   hence a sequence of proofs of accessibility, one for
   each term in the fundamental sequence for Gamma0.

   Each proof can be expressed 
   in a type theory in which there is a next universe
   operator (ie. an external sequence of universes).
   mapping a family of sets to the least family containing
   it as an internal subfamily which is closed under certain 
   operations (pi, sigma, Nat). 
   (Admittedly it needs close inspection to see this.)

   Closer inspection should reveal that we can construct
   a proof of accessibility for all notations, and 
   with a number of universes depending on the 
   levels to which the veblen hierarchy is nested.
   (But this is a little complex to set up.)

   The main result is called Corollary and is the
   last definition of the file.
-}

open Ordinals use  
    Ord, zero, limit, succ, 
    C, pd, 
    OpIt, OpItw, OpLim, 
    Nabla, 
    w, wexp, epsilon0, 
    v, veb, Gamma0,
    deriv, derivl

open Amenities 
   use N1, star,
       N0, efq, 
       Si, and, 
       op, op2, 
       Pow, Fam

open Naturals 
   use Nat, Seq, 
       It, Rec

package small( FS :: Fam Set ) where 

  Ot :: Set = Ord

  Us :: Set = FS.I
  Ts :: Us -> Set = FS.i

  {- small sets -}
  open UniverseOver Ot Us Ts use 
      set, el, 
      otcode, 
      pi, arr, 
      pin, piot

  Next :: Fam Set = struct 
                      I = set
                      i = el

  {- large sets -}
  open UniverseOver Ot set el use
      SET = set, 
      EL = el, 
      OT  = otcode, 
      ARR = arr,
      PI  = pi,
      PIN = pin,
      PIOT= piot,
      SI  = si, 
      AND = and

{------------ predicates ------------------}

  {- The type of real predicates -} 
  Pred :: Type  = Ot -> Set

  {- The Set of small predicates -}
  pred :: Set   = Ot -> set

  {- The Set of big predicates -}
  PRED :: Set   = Ot -> SET

  {- the representation of pred
     in SET.  We
     have EL PRED = pred; so PRED 
     represents or reflects pred. -}

  predcode :: SET = otcode@SET `ARR` u@SET

  {- that X is a subset of Y -} 
  subset (X, Y :: pred) :: set 
      = piot (\(a :: Ot)-> X a `arr` Y a)

  {- That "is a subset of" is transitive -}
  subsetTrans (p, q, r :: pred) 
    :: el ((p `subset` q) `arr` 
          ((q `subset` r) `arr` (p `subset` r)))
    = \(pq :: el (p `subset` q)) -> 
      \(qr :: el (q `subset` r)) -> 
      \(a :: Ot) -> 
      \(pa :: el (p a)) -> 
      qr a (pq a pa)

  {- That "is a subset of" is reflexive -}
  subsetRefl (p :: pred) 
    :: el (p `subset` p)
    = \(a :: Ot) -> \(pa :: el (p a)) -> pa

  {- Intersection of a sequence of predicates. -}
  capn (Xs :: Seq pred) :: pred
      = \(a :: Ot) -> pin (\(n :: Nat) -> Xs n a)

  {- That capn gives a lower bound for 
     sequences of predicates 
  -}
  capnLemOut (ps :: Seq pred)
    :: el (pin (\(n :: Nat) -> capn ps `subset` (ps n)))
    = \(n :: Nat) -> 
      \(a :: Ot) -> 
      \(psa :: el (capn ps a)) -> psa n

  {- That capn is a greatest lower bound 
     for sequences of predicates 
  -}
  capnLemIn (ps :: Seq pred) (q :: pred) 
    :: el (pin (\(n :: Nat) -> q `subset` (ps n)) 
           `arr` (q `subset` capn ps))
    = \(qps :: el (pin (\(n :: Nat) -> q `subset` ps n))) -> 
      \(a :: Ot) -> 
      \(qa :: el (q a)) -> 
      \(n :: Nat) ->
        qps n a qa

  {- Operation on a predicate which precomposes it with 
     an operation. -}
  sub (X :: pred) (f :: op Ot) :: pred
      = \(a :: Ot) -> X (f a)

  {- Property of a predicate that it is closed 
     under an operation -}
  clunder (X :: pred) (f :: op Ot) :: set
      = X `subset` (X `sub` f)

  {- predicate transformer induced by 
     a family of operations 
     = a binary operation -}
  clunder2 (X :: pred) (f :: op2 Ot) :: pred
      = \(a :: Ot) -> X `clunder` f a  

  {- PT induced by transition structure -}
  B :: pred -> pred
    = \(X :: pred) -> 
      \(a :: Ot) -> 
      case a of 
         (O) -> n1code@set
         (S a') -> X a'
         (L ls) -> pin (\(n :: Nat) -> X (ls n))

  {- That B is monotone. -}
  BM (p :: pred) (q :: pred) 
    :: el ((p `subset` q) `arr` (B p `subset` B q))
    = \(pq :: el (p `subset` q)) -> 
      \(a :: Ot) ->
       case a of 
         (O)    -> \(x :: N1) -> x
         (S a') -> pq a'
         (L ls) -> \(a' :: el (B p (limit ls))) -> 
                   \(n :: Nat) -> pq (ls n) (a' n)

  {- Progressivity of a predicate -}
  prog (X :: pred) :: set
    = piot (\(a :: Ot) -> B X a `arr` X a)

  Prog (X :: pred) :: Set 
    = el (prog X)

  B' :: PRED -> PRED 
    = \(X :: PRED) -> 
      \(a :: Ot) -> 
      case a of 
         (O) -> n1code@SET     -- t@SET (n1code@set)
         (S a') -> X a'
         (L ls) -> PIN (\(n :: Nat) -> X (ls n)) 

  PROG (X :: PRED) :: SET
    = PIOT (\( a :: Ot ) -> B' X a `ARR` X a) 

  {- Accessibility of a notation. 
     Quantifies over pred. -}

  Acc (a :: Ot) :: Set
    = (X :: pred) -> 
         el (prog X `arr` X a)

  Acc0 :: Acc zero
    = \(X::pred) -> \(a::Prog X) -> a zero star 

  AccS (a :: Ot) :: Acc a -> Acc (succ a) 
    = \(h :: Acc a) -> 
      \(X :: pred) -> 
      \(pX :: Prog X) -> 
      pX (succ a) (h X pX) 

  AccL (fs :: Seq Ot) :: ((n :: Nat) -> Acc (fs n)) -> Acc (limit fs)
    = \(h :: (n::Nat) -> Acc (fs n)) -> 
      \(X :: pred) -> 
      \(pX :: Prog X) -> 
      pX (limit fs) (\(n::Nat) -> h n X pX) 

  acc_code (a :: Ot) :: SET
    = PI predcode (\(X :: pred) -> 
         t@SET (prog X `arr` X a))

  ACC (a :: Ot) :: Set
    = (X :: PRED)->  
         EL (PROG X `ARR` X a)

  {- That if a predicate is closed under an operation, then 
     it is also closed under all iterates of that operation. -}
  closureLemma (X :: pred) 
               (f :: op Ot) 
               (clf :: el (X `clunder` f))
    :: el (pin (\(n :: Nat) -> X `clunder` OpIt f n))
    = \(n :: Nat) -> 
      \(a :: Ot) -> 
      \(xa :: el (X a)) -> 
      Rec ( \(k :: Nat) -> 
            el (X (OpIt f k a)) )
          xa ( \(n' :: Nat) -> 
               \(h :: el (X (OpIt f n' a))) ->
                  clf (OpIt f n' a) h) n


  {- That the intersection of a sequence of progressive 
     predicates  is itself progressive.  -}
  capnProg (ps :: Seq pred) 
    :: el ((pin (\(n :: Nat) -> prog (ps n))) 
           `arr` prog (capn ps))
    =  \ (psp :: el (pin (\(n :: Nat) -> prog (ps n)) )) ->
       let L :: pred = B (capn ps) 
           body (n :: Nat) 
              :: el (B (capn ps) `subset` ps n) =
                let M :: pred = B (ps n) 
                    step1 :: el (capn ps `subset` ps n) 
                            = capnLemOut ps n 
                    step2 :: el (B (capn ps) `subset` B (ps n)) 
                            = BM (capn ps) (ps n) step1 
                in subsetTrans L M (ps n) step2 (psp n) 
       in capnLemIn ps L body  

{-------------- predicate transformers -----------}

  PT      :: Set          = op pred 
  PT'     :: SET          = predcode `ARR` predcode
  PTid    :: PT           = \(x :: pred) -> x

  {- composition of predicate transformers -}
  PTcomp  :: op2 PT       = \(f :: PT) -> \(g :: PT) -> 
                            \(x :: pred) -> f (g x) 

  {- iteration of predicate transformers. -}
  ItPT    :: PT -> Seq PT = It pred 

  {- pointwise intersection of sequences of PTs. -}
  PTlim   :: Seq PT -> PT
    = \(pts :: Seq PT) -> \(a :: pred) -> 
      capn (\(n :: Nat) -> pts n a)

  {- preservation of progressivity by a PT -}

  PProg (F :: pred -> pred) :: Set
    = (X :: pred) -> 
        Prog X -> Prog (F X) 

  {- same thing reflected as a SET -}
  PPROG(F :: pred -> pred) :: SET
    = PI predcode (\(X :: pred) -> 
         t@SET (prog X `arr` prog (F X)))

  {- Composition preserves preservation of progressivity -}

  PProgComp
      (F :: PT ) (pF :: PProg F)
      (G :: PT ) (pG :: PProg G)
      :: PProg (PTcomp F G)
    = \(X :: pred) -> 
      \(p :: Prog X) -> 
      pF (G X) (pG X p) 

  {- Identity PT preserves progressivity. -}

  PProgId ::  PProg PTid
    = \(X :: pred) -> \(h :: Prog X) -> h
      
  {- Iteration preserves preservation of progressivity. -}

  ItPProg (F :: PT) (pF :: PProg F)
          (n :: Nat)
      :: PProg (ItPT F n) 
    = \(X :: pred) -> \(pX :: Prog X) -> 
      Rec (\(k :: Nat) -> Prog (ItPT F k X)) 
          pX (\(k :: Nat) -> \(h' :: Prog (ItPT F k X)) -> 
          pF (ItPT F k X) h') n

  {- Given a sequence of predicate transformers, 
     if they each  preserve progressivity, 
     then so does their pointwise limit -}
  PProgLim ( pts :: Seq PT) 
           ( pp :: (n :: Nat)-> PProg (pts n) )
    :: PProg (PTlim pts)
    = \(X :: pred) -> 
      \(p :: Prog X) -> 
      capnProg (\(n :: Nat) -> pts n X) 
               (\(n :: Nat) -> pp n X p)

  {- Gentzen's PT -}
  G :: PT 
    = \(X :: pred) -> 
         X `clunder2` (\(a, b :: Ot) -> b `w` a)  

  GentzensLemma :: PProg G 
    = \(X :: pred) ->
      \(p :: Prog X) -> 
      \(x :: Ot) -> 
      \(h :: el (B (G X) x)) -> 
      \(a :: Ot) -> 
      \(xa :: el (X a)) -> 
      let arg ::  el (B X (a `w` x))
            = case x of 
              (O)    -> xa   
              (S a') -> 
               let  f   :: Ot -> Ot 
                         = \(x :: Ot) -> x `w` a' 
                    itf :: Nat -> Ot 
                         = \(k :: Nat)-> It Ot f k a 
               in Rec (\(n :: Nat) -> el (X (itf n)))
                       xa (\(n :: Nat) -> h (itf n))
              (L ls) -> (\(n :: Nat) -> h n a xa)   
      in p (a `w` x) arg

  LensLemmaG (a :: Ot) (acca :: Acc a) 
             (b :: Ot) (accb :: Acc b)
    :: Acc (w a b)
    = \(X::pred) -> 
      \(pX::el (prog X)) -> 
      accb (G X) (GentzensLemma X pX) a (acca X pX)

  {- A protolens is a predicate transformer that 
     preserves progressivity -}

  ProtoLens :: Set
    = Si PT PProg 

  {- Coded as a large set -}
  PROTOLENS :: SET    = si@SET PT' PPROG

  ProtoLensId :: ProtoLens 
    = struct 
        fst = PTid
        snd = PProgId 

  ProtoLensComp :: op2 ProtoLens 
    = \(f :: ProtoLens) -> 
      \(g :: ProtoLens) -> 
        struct 
          fst = PTcomp f.fst g.fst
          snd = PProgComp f.fst f.snd g.fst g.snd

  {- Finite iteration of proto-lenses -}
  ProtoLensIt :: ProtoLens -> Seq ProtoLens
    = \(pl :: ProtoLens) -> 
      \(n :: Nat) -> 
      It ProtoLens (ProtoLensComp pl) n pl

  {- The notion of Lens -}
  Lens  (f :: op Ot) :: Set
    = Si ProtoLens (\(pl :: ProtoLens) -> 
         (X :: pred) -> Prog X -> 
         el ((pl.fst X) `subset` (X `sub` f) ))

  {- Coded as a large set -} 
  LENS (f :: op Ot) :: SET
    = si@SET PROTOLENS (\(pl :: ProtoLens) -> 
          PI predcode (\(X :: pred) -> 
             t@SET (prog X `arr` (pl.fst X `subset` (X `sub` f))) ))

  {- The accessible notations are closed under any operation that
     possesses a lens. -}

  LensLemmaV (f :: op Ot) 
            (lf :: Lens f) 
            (a :: Ot) 
    :: Acc a -> Acc (f a)
    = \(h :: Acc a) -> 
      \(X :: pred) -> 
      \(pX :: Prog X) -> 
      lf.snd X pX a (h (lf.fst.fst X) (lf.fst.snd X pX))

  {- The identity function possesses a lens -}

  LensId :: Lens (\(x :: Ot) -> x)
    = struct 
        fst = ProtoLensId
        snd = \(X :: pred) -> 
              \(pX :: Prog X) -> 
              \(a :: Ot) -> 
              \(xa :: el (X a)) -> xa

  {- Closure of lenses under composition. -}

  LensComp (f :: op Ot) (lf :: Lens f) 
           (g :: op Ot) (lg :: Lens g) 
           :: Lens (\(a :: Ot) -> f (g a))
    = struct 
        fst = ProtoLensComp lg.fst lf.fst
        snd = \(X :: pred) -> \(pX :: Prog X) -> 
              \(a :: Ot) -> 
              \(a' :: el (fst.fst X a)) -> 
              lf.snd X pX 
                     (g a) (lg.snd (lf.fst.fst X) 
                                   (lf.fst.snd X pX) a a')

  GentzensProtoLens :: ProtoLens
    = struct 
        fst = G
        snd = GentzensLemma

  GentzenLens :: Lens wexp 
    = struct 
        fst = GentzensProtoLens
        snd = \(X :: pred) -> 
              \(p :: Prog X) -> 
              \(a :: Ot) -> 
              \(h :: el (G X a)) -> 
              h zero (p zero star)  

  {- A closure lens for an operator f is a protolens (F,..), 
     such that F X subset X on progressive 
     predicates X (i.e. a lens for the identity 
     function), and such that if X is a progressive 
     predicate, then F X is closed under f.  -}
     
  CLens (f :: op Ot) :: Set
    = Si  ProtoLens (\(pl :: ProtoLens) ->
        and ( (X :: pred) -> 
              el (prog X `arr` (pl.fst X `subset` X )))
            ( (X :: pred) -> 
              el (prog X `arr` (pl.fst X `clunder` f))))

  {- We can make a closure lens from a lens.
     The idea is fairly simple, though in a way
     the key to the whole construction. 
     Just take the limit-by-intersection of the finite
     iterates of the predicate transformer.
  -}
  MkClens ( f :: op Ot ) :: Lens f -> CLens f 
    = \(l :: Lens f) -> 
      let 
        pt  :: PT = l.fst.fst 
        pp  :: PProg pt = l.fst.snd 
        dr  :: (X :: pred) -> Prog X -> 
                  el (pt X `subset` sub X f) 
            = l.snd 
        pt' :: PT 
            = PTlim (ItPT pt)  
        pp' :: PProg pt'  
            = PProgLim (ItPT pt) (ItPProg pt pp)  
        cl1 :: (X :: pred) -> 
               (p :: Prog X) -> 
               el (pt' X `subset` X)  
            = \(X :: pred) -> 
              \(_ :: Prog X) -> 
              \(a :: Ot) -> 
              \(x :: el (pt' X a)) -> 
              x Naturals.zero  
        cl2 :: (X :: pred) -> 
               (_ :: Prog X) -> 
               el (pt' X `clunder` f)  
            = \(X :: pred) -> 
              \(pX :: Prog X) -> 
              \(a :: Ot) -> 
              \(x :: el (pt' X a)) ->
              \(n :: Nat) -> 
              dr (ItPT pt n X) 
                 (ItPProg pt pp n X pX) 
                 a 
                 (x (Naturals.succ n)) 
      in struct 
           fst = struct 
                  fst = pt'
                  snd = pp'
           snd = struct 
                  fst = cl1
                  snd = cl2

  {- Given a closure lens for an operator, 
     we can get another one for the omega-iteration 
     of that operator. This is where
     the word "closure" comes from. -}

  ItClens ( f :: op Ot ) 
    :: CLens f -> CLens (OpItw f)
    = \(cl  :: CLens f) -> 
      let   pl :: ProtoLens 
               = cl.fst 
            pt :: PT 
               = pl.fst 
            pp :: PProg pt 
               = pl.snd 
            pf :: (X :: pred) -> Prog X -> 
                  el (pt X `subset` X) 
                 = cl.snd.fst 
            cls :: (X :: pred) -> (p :: Prog X) -> 
                    el (clunder (pt X) f) 
                 = cl.snd.snd 
            cls' :: (X :: pred) -> (p :: Prog X) -> 
                    el (pt X `clunder` OpItw f) 
             = \(X :: pred) -> 
               \(pX :: Prog X) -> 
               \(a :: Ot) -> 
               \(x :: el (pt X a)) -> 
               pp X pX (OpItw f a) (\(n :: Nat) ->  
               closureLemma (pt X) f (cls X pX) n a x)
      in struct 
           fst = pl
           snd = struct 
                   fst = pf
                   snd = cls'

  {- Given a sequence of lenses for a sequence of functions,
     we can form a lens for their pointwise sup. -}

  {- Really uses only that progressive implies closed -}
  SupLens (fs :: Seq (op Ot)) 
          (ls :: (n :: Nat) -> Lens (fs n))
          :: Lens (OpLim fs)
    = let
        pts (n :: Nat) :: PT 
                = (ls n).fst.fst 
        pps (n :: Nat) :: PProg (pts n) 
                = (ls n).fst.snd 
        drs (n :: Nat) 
               :: (X :: pred) -> 
                  Prog X -> 
                  el ( (pts n X) `subset` (X `sub` fs n))  
               = (ls n).snd 
        pt :: PT = PTlim pts  
        pp :: PProg pt = PProgLim pts pps  
        dr (X :: pred) (pX :: Prog X) 
               ::  el (pt X `subset` (X `sub` (OpLim fs)))
               = \(a :: Ot) -> 
                 \(xa :: el (pt X a)) -> 
                 pX (OpLim fs a) 
                    (\(n :: Nat) -> 
                          drs n X pX a (xa n)) 
      in struct 
           fst = struct 
                   fst = pt
                   snd = pp 
           snd = dr 

  {- If we have a closure lens for f, then 
     we can get a lens for Nabla f. 
     It is maybe unhygienic that there is a case 
     distinction here. 
  -}

  NablaLens (f :: op Ot) 
            (cl :: CLens f ) 
    :: Lens (Nabla f) 
    = let
        pt  :: PT            = cl.fst.fst        
        pp  :: PProg pt      = cl.fst.snd  
        pf  :: (X :: pred) -> Prog X -> 
                 el (pt X `subset` X) 
            = cl.snd.fst 
        cls :: (X :: pred) -> (p :: Prog X) -> 
                   el (pt X `clunder`f) 
            = cl.snd.snd               
        pt' :: PT 
            = \(X :: pred) -> pt X `sub` Nabla f 
        pp' :: PProg pt'
            = \(X :: pred) -> 
              \(pX :: Prog X) -> 
              \(a :: Ot) -> 
              \(h ::  el (B (pt' X) a)) -> 
              case a of 
                (O)    -> cls X pX a (pp X pX a star)
                (S a') -> cls X pX (succ (Nabla f a')) 
                             (pp X pX (succ (Nabla f a')) h) 
                (L ls) -> pp X pX (Nabla f a) h      
        dr' (X :: pred) (pX :: Prog X)
            :: el ((pt' X) `subset` (X `sub` (Nabla f)))
            = \(a :: Ot) -> pf X pX (Nabla f a)    
      in struct 
           fst = struct 
                  fst = pt'
                  snd = pp' 
           snd = dr'

  {- The following predicate is pivotal. -}
  LensPredicate (a :: Ord) :: SET
    = LENS (v a)

  SuccLens (f :: op Ot) (lf :: Lens f)
    :: Lens (deriv f)
    = NablaLens (OpItw f) 
                (ItClens f (MkClens f lf)) 

  LimLens (fs :: Seq (op Ot)) 
          (lfs :: (n :: Nat) -> Lens (fs n)) 
    :: Lens (derivl fs)
    = let  f :: op Ot = OpLim fs 
      in   NablaLens f (MkClens f (SupLens fs lfs))

  ZeroLens :: Lens (deriv wexp) 
    = SuccLens wexp GentzenLens

--------------------------------------------------------
{- We are now back outside the "small" package. The file
  concludes with a proof of the accessibility of
  Gamma_0 -}

{- Next universe operator. -}

NextU (FS :: Fam Set) :: Fam Set
   = (small FS).Next

{- Accessibility relative to a family of sets -}
acc (FS :: Fam Set) :: Ord -> Set
   = (small FS).Acc

ACC (FS :: Fam Set) :: Ord -> Set
   = acc (NextU FS) 

{- The set of lenses relative to a family of sets -}
Lens (FS :: Fam Set)(f :: Ord -> Ord) :: Set
   = (small FS).Lens f

PRED (FS :: Fam Set)
   :: Set
   = (small (NextU FS)).pred

{- The predicate wrt FS that Lens (v a) -}
lenspred (FS :: Fam Set) 
   :: PRED FS 
   = (small FS).LensPredicate 

PROG (FS :: Fam Set)
   :: Pow (PRED FS) 
   = (small (NextU FS)).Prog 

{- That the above predicate is progressive -}
lenspredprog (FS :: Fam Set) 
   :: PROG FS (lenspred FS) 
   = \(a::Ord) -> 
     case a of 
        (O) -> \(_::N1) -> 
                  (small FS).ZeroLens
        (S a') -> (small FS).SuccLens 
                       (v a')
        (L ls) -> (small FS).LimLens 
                       (\(n::Nat) -> v (ls n))

{- The key lemma which shows how for each 
   layer of the veblen hierarchy, you can 
   use another universe -}
 
LemmaV (FS :: Fam Set) 
      (a :: Ord)
      (acca :: ACC FS a)
   :: (b :: Ord) -> acc FS b -> acc FS (v a b) 
   = let vl :: Lens FS (v a) 
            = acca (lenspred FS) (lenspredprog FS) 
     in (small FS).LensLemmaV (v a) vl

{- Just for completeness, we pull out 
   of the package above the corresponding 
   lemma for the function w. -}

LemmaG (FS :: Fam Set) 
      (a :: Ord)
      (acca :: acc FS a)
   :: (b :: Ord) -> acc FS b -> acc FS (w a b) 
   = (small FS).LensLemmaG a acca

{- RECURSIVE
   The main theorem.  
   To express the recursion by use of NatRec, we 
   would need a superuniverse closed under NextU -}

Theorem (FS :: Fam Set) (n :: Nat) 
    :: acc FS (pd Gamma0 n) 
    =  case n of 
         (Z) ->  (small FS).Acc0 
         (S p) -> LemmaV FS 
                    (pd Gamma0 p) (Theorem (NextU FS) p) 
                     zero         (small FS).Acc0

Corollary (FS :: Fam Set) 
    :: acc FS Gamma0
    = (small FS).AccL (pd Gamma0) (Theorem FS)