typeoftm : tm -> tp -> type.
%name typeoftm _Typetm.


% Unit

typeoftm/unitintro : typeoftm unittm unittp.

% Arrow

typeoftm/arrintro :  ({x : tm} typeoftm x Tdom -> typeoftm (Mbody x) Tcod)
                  -> typeoftm (lamtm ([x] Mbody x)) (arrtp Tdom Tcod).

typeoftm/arrelim  :  typeoftm M1 (arrtp Tdom Tcod)
                  -> typeoftm M2 Tdom
                  -> typeoftm (apptm M1 M2) Tcod.

% Product

typeoftm/prodintro : typeoftm M1 T1
                  -> typeoftm M2 T2
                  -> typeoftm (pairtm M1 M2) (prod T1 T2).

typeoftm/prodelim1 : typeoftm M (prod T1 T2) -> typeoftm (fsttm M) T1.
typeoftm/prodelim2 : typeoftm M (prod T1 T2) -> typeoftm (sndtm M) T2.


% Fix

typeoftm/fix : ({u : tm} typeoftm u A -> typeoftm (Mbody u) A)
            -> typeoftm (fixtm ([u] Mbody u)) A.


% Sums

typeoftm/sumelim :
                   typeoftm M (sumty T1 T2)
                -> ({m1 : tm} typeoftm m1 T1 -> typeoftm (N1 m1) T)
                -> ({m2 : tm} typeoftm m2 T2 -> typeoftm (N2 m2) T)
                -> typeoftm (casetm M ([m1] N1 m1) ([m2] N2 m2)) T.

typeoftm/sumintro1 : typeoftm M T1 -> typeoftm (inltm M) (sumty T1 T2).
typeoftm/sumintro2 : typeoftm M T2 -> typeoftm (inrtm M) (sumty T1 T2).


%freeze typeoftm.