translation.ott

grammar
tran :: translation_ ::=
  | tran1 , x : tran2	:: :: ctx_app
  | mudG ( G ok )		:: :: ctx
  | GC = mudG ( G ok )  :: :: gcDef
  | ec = muE ( G |- es : ts )
						:: :: ecTermDef
  | ec = muT ( G |- ts )
						:: :: ecTypeDef
  | gamma = muS ( G |- ts1 <: ts2 )
						:: :: cvtDef
  | muT ( G |- ts )		:: :: ty
  | muT ( G1 |- ts1 ) -> muT ( G2 |- ts2 )
						:: :: tyarr


defns Jctarget :: '' ::=

defn GC |- ec1 : ec2 :: :: twftarget :: TWFTarget_ by

omitted
------------------------------------- :: TrueRef
GC |- ( BC , unitc equal unitc of Unitc ) : sst

mudE ( G , v : { v1 : B | top } |- es1 : { v2 : B' | top } )
mudE ( G , v : { v1 : B | top } |- es2 : { v2 : B' | top } )
omitted
---------------------------------------------------- :: Base
GC |- Sigma BC (\ v : BC . ec1 equal ec2 of tc) : sst

mudT ( G |- { v : B | r1 } )
mudT ( G |- { v : B | r2 } )
-------------------------------------------------- :: Conj
GC |- Sigma BC (\ v : BC . (Pred1 v , Pred2 v)) : sst

mudT ( G |- ts1 )
mudT ( G , x : ts1 |- ts2 )
---------------------------- :: Arr
GC |- Pi x : tc1 . tc2 : sst

</ mudT ( G |- tsi ) // i />
------------------------------ :: ADT
GC |- < </ li : tci // i />  > : sst


defn GC |- ec1 : ec2 :: :: tytarget :: TTarget_ by

mudT ( G |- ts )
x : tc in GC
----------------- :: VarW
GC |- x : tc

mudT ( G |- (x : ts1) -> ts2 )
mudE ( G , x : ts1 |- es : ts2 )
--------------------------------------- :: Abs
GC |- \ x : tc1 . ec : Pi x : tc1 . tc2

mudE (G |- es1 : (x : ts1) -> ts2)
mudE (G |- es2 : ts1)
---------------------------------- :: App
GC |- ec1 ec2 : [ x |-> ec2 ] tc2

mudT (G |- ts')
mudE (G |- es : ts)
</ mudE (G , xi : tsi , x : { _ : Unit | es = (< li = xi > as ts) of ts } |- esi : ts') // i />
omitted
x fresh
----------------------------------------------------------------------------------------- :: Case
GC |- case ec of </ li = xi proof pi -> ( \x : tci' . eci ) ( Sigma Unitc pi ) // i /> : tc'

% TODO either add a lambda in the dpair or change the definition of dpair, replacing Px with *

mudE (G |- es : tsj)
lj in </ li // i />
mudT (G |- < </ li : tsi // i /> >)
--------------------------------------------------------------------- :: Con
GC |- < lj = ec> as < </ li : tci // i /> > : < </ li : tci // i /> >

mudE (G |- es : ts)
mudS (G |- ts <: ts') \\\\
omitted
---------------------------------- :: Sub
GC |- gamma ec : tc'


defn GC |- ec1 : ec2 :: :: sttarget :: STTarget_ by

GC |- sigma : Pi v : BC . tc1 -> tc2
omitted
------------------------------------------------------- :: Base
GC |- seconddp sigma : (Sigma BC tc1) -> (Sigma BC tc2)

mudS (G |- ts1' <: ts1)
mudS (G , x : ts1' |- ts2 <: ts2')
omitted
------------------------------------------------------- :: Arr
GC |- \f : (Pi x : tc1. tc2). \x : tc1'. gamma2 (f (gamma1 x)) : (Pi x : tc1. tc2) -> (Pi x : tc1'. tc2')