module Thm where

open import PrimTypes
open Sg'
open import Model
open import ObsEq

Guts : (S : Ty SET)
       (C : [ S ] -> Ty SET)
       (R : (s : [ S ])(c : [ C s ]) -> Ty SET)
       (n : (s : [ S ])(c : [ C s ])(r : [ R s c ]) -> [ S ]) ->
       (s : [ S ]) -> Ty SET
Guts S C R n s = `Sg' (C s) \ c -> `Pi' (R s c) \ r -> `INu' S C R n (n s c r)

conOutLaw : (uf : forall {S}{F : Cont S}(A : S -> Set) -> (A ->> Fun F A) -> A ->> INu F) ->
            (S : Ty SET)
            (C : [ S ] -> Ty SET)
            (R : (s : [ S ])(c : [ C s ]) -> Ty SET)
            (n : (s : [ S ])(c : [ C s ])(r : [ R s c ]) -> [ S ]) ->
            (s : [ S ])(x : [ `INu' S C R n s ]) ->
            [ `Prf'
             ! `INu' S C R n s > x == `INu' S C R n s > con (command x) (continue x) ! ]
conOutLaw uf S C R n s x = uf
    (\ sxsx ->
     let sx0 = fst sxsx
         s0 = fst sx0
         x0 = snd sx0
         sx1 = snd sxsx
         s1 = fst sx1
         x1 = snd sx1
     in  [ `Prf' (! S > s0 == S > s1 ! &
                  ! Guts S C R n s0 > out x0 == Guts S C R n s1 > out x1 !) ])
  {! (\ sxsx scfq ->
     let sx0 = fst sxsx
         s0 = fst sx0
         x0 = snd sx0
         sx1 = snd sxsx
         s1 = fst sx1
         x1 = snd sx1
         sq = fst scfq
         cfq = snd scfq
         c0 = command x0
         c1 = command x1
         cq = fst cfq
         f0 = continue x0
         f1 = continue x1
         fq = snd cfq
     in  cq , sp0 \ r0 -> sp0 \ r1 rq ->
         let n0 = n s0 c0 r0
             n1 = n s1 c1 r1
             nq = refl (`Pi' S \ s -> `Pi' (C s) \ c -> `Pi' (R s c) \ _ -> S) n
                  s0 s1 sq c0 c1 cq r0 r1 rq 
         in  nq , refl (`Pi' S \ s -> `Pi' (`INu' S C R n s) \ _ -> Guts S C R n s)
                       (\ s x -> out x)
                  n0 n1 nq (f0 r0) (f1 r1) (fq r0 r1 rq)) !}
    _ (refl S s , refl (Guts S C R n s) (out x))


 {-unfold
  (sp1 (sp1 (\ s0 x0 -> sp1 \ s1 x1 ->
    [ `Prf' (`Sg' ! S > s0 == S > s1 ! \ _ ->
            ! Guts S C R n s0  > out x0 == Guts S C R n s1 > out x1 !) ])))
  (sp0 (sp0 \ s0 x0 -> sp0 \ s1 x1 -> sp0 \ sq -> sp0 \ cq fq -> cq ,
   sp0 \ r0 -> sp0 \ r1 rq -> {!refl (`Pi' S \ s -> `Pi' (`INu' S C R n s) \ _ -> Guts S C R n s) (\ s x -> out x) !}))
  ((s , _) , (s , _)) (? , refl (Guts S C R n s) (out x)) -}