module ObsEq where

open import PrimTypes
open Sg'
open import Model


mutual
  funQ : (S T : Ty SET) -> ([ S ] -> [ T ] -> Ty PROP) -> Ty PROP
  funQ S T R = `Pi' S \ s -> `Pi' T \ t -> ! S > s == T > t ! => R s t
  DFunQ : (S T : Ty SET) -> ([ S ] -> [ T ] -> Ty PROP) -> Ty PROP
  DFunQ S T R =  (S <-> T) & funQ S T R

  _<->_ : Ty SET -> Ty SET -> Ty PROP
  `2'                   <-> `2'         = `1'
  `Pi' Sl Tl            <-> `Pi' Sr Tr  = DFunQ Sr Sl \ sr sl -> Tl sl <-> Tr sr
  `Sg' Sl Tl            <-> `Sg' Sr Tr  = DFunQ Sl Sr \ sl sr -> Tl sl <-> Tr sr
  `IMu' Sl Cl Rl nl sl  <-> `IMu' Sr Cr Rr nr sr =
    ! Sl > sl == Sr > sr ! &
    DFunQ Sl Sr \ sl sr ->
    DFunQ (Cl sl) (Cr sr) \ cl cr ->
    DFunQ (Rr sr cr) (Rl sl cl) \ rr rl ->
    ! Sl > nl sl cl rl == Sr > nr sr cr rr !
  `INu' Sl Cl Rl nl sl  <-> `INu' Sr Cr Rr nr sr =
    ! Sl > sl == Sr > sr ! &
    DFunQ Sl Sr \ sl sr ->
    DFunQ (Cl sl) (Cr sr) \ cl cr ->
    DFunQ (Rr sr cr) (Rl sl cl) \ rr rl ->
    ! Sl > nl sl cl rl == Sr > nr sr cr rr !
  `Prf' Pl              <-> `Prf' Pr    = (Pl => Pr) & (Pr => Pl)
  _                     <-> _           = `0'

  !_>_==_>_! : (S : Ty SET) -> [ S ] -> (T : Ty SET) -> [ T ] -> Ty PROP
  ! `2' > tt == `2' > tt ! = `1'
  ! `2' > tt == `2' > ff ! = `0'
  ! `2' > ff == `2' > tt ! = `0'
  ! `2' > ff == `2' > ff ! = `1'
  ! `Pi' Sl Tl > fl == `Pi' Sr Tr > fr ! =
    funQ Sl Sr \ sl sr -> ! Tl sl > fl sl == Tr sr > fr sr !
  ! `Sg' Sl Tl > pl == `Sg' Sr Tr > pr ! =
    ! Sl > fst pl == Sr > fst pr ! &
    ! Tl (fst pl) > snd pl == Tr (fst pr) > snd pr !
  ! `IMu' Sl Cl Rl nl sl > dl == `IMu' Sr Cr Rr nr sr > dr ! = muQ sl dl sr dr where
    muQ : (sl : [ Sl ]) -> [ `IMu' Sl Cl Rl nl sl ] ->
          (sr : [ Sr ]) -> [ `IMu' Sr Cr Rr nr sr ] -> Ty PROP
    muQ sl (con cl fl) sr (con cr fr) =
      ! Cl sl > cl == Cr sr > cr ! &
      `Pi' (Rl sl cl) \ rl -> `Pi' (Rr sr cr) \ rr ->
      ! Rl sl cl > rl == Rr sr cr > rr ! =>
      muQ (nl sl cl rl) (fl rl) (nr sr cr rr) (fr rr)
  ! `INu' Sl Cl Rl nl sl > dl == `INu' Sr Cr Rr nr sr > dr ! =
    `INu' (`Sg' Sl (`INu' Sl Cl Rl nl) & `Sg' Sr (`INu' Sr Cr Rr nr))
    (sp0 (sp0 \ sl dl -> sp0 \ sr dr -> ! Cl sl > command dl == Cr sr > command dr !))
    (sp0 (sp0 \ sl dl -> sp0 \ sr dr q ->
     `Sg' (Rl sl (command dl)) \ rl -> `Sg' (Rr sr (command dr)) \ rr ->
     `Prf' ! Rl sl (command dl) > rl == Rr sr (command dr) > rr !))
    (sp0 (sp0 \ sl dl -> sp0 \ sr dr cq -> sp0 \ rl -> sp0 \ rr rq ->
      (nl sl (command dl) rl , continue dl rl) , (nr sr (command dr) rr , continue dr rr) ))
    ((sl , dl) , (sr , dr))
  ! `Prf' y > s == `Prf' y' > t ! = `1'
  ! _ > _ == _ > _ ! = `1'

postulate refl : (S : Ty SET)(s : [ S ]) -> [ `Prf' ! S > s == S > s ! ]