% % Theorem (Coercion) % coerce : % If {E : exp} typeof+sub E A % then -> {E' : exp} typeof E' A -> type. %mode coerce +E +D -E' -D'. - : coerce _ (typeof+sub/topintro IsVal) _ (typeof/topintro IsVal). - : coerce E (typeof+sub/sectintro D1 D2) (merge E1' E2') (typeof/sectintro (typeof/merge1 D1') (typeof/merge2 D2')) <- coerce E D1 E1' D1' <- coerce E D2 E2' D2'. - : coerce E (typeof+sub/sectelim1 D1) E' (typeof/sectelim1 D1') <- coerce E D1 E' D1'. - : coerce E (typeof+sub/sectelim2 D2) E' (typeof/sectelim2 D2') <- coerce E D2 E' D2'. - : coerce E (typeof+sub/unintro1 D1) E' (typeof/unintro1 D1') <- coerce E D1 E' D1'. - : coerce E (typeof+sub/unintro2 D2) E' (typeof/unintro2 D2') <- coerce E D2 E' D2'. coerce/unelim : {A1 : ty} {A2 : ty} {C : ty} {E0:exp} {D0:typeof+sub E0 (unty A1 A2)} {E0':exp} {D0':typeof E0' (unty A1 A2)} {EC:eval-context} {EH:exp -> exp} {Fill : fill EC EH} {D1:{x:exp} typeof+sub x A1 -> typeof+sub (EH x) C} {D1':{x:exp} typeof x A1 -> typeof (E1 x) C} {D2:{x:exp} typeof+sub x A2 -> typeof+sub (EH x) C} {D2':{x:exp} typeof x A2 -> typeof (E2 x) C} coerce (EH E0) (typeof+sub/unelim Fill D0 D1 D2) (app (lam ([y] (merge (E1 y) (E2 y)))) E0') (typeof/unelim (ec/app2 (lam ([y] (merge (E1 y) (E2 y)))) (is-value/lam) (ec/hole)) (fill/app2 (fill/hole)) D0' ([x1] [Dx1] typeof/arrelim (typeof/arrintro ([y] [Dy] typeof/merge1 (D1' y Dy))) Dx1) ([x2] [Dx2] typeof/arrelim (typeof/arrintro ([y] [Dy] typeof/merge2 (D2' y Dy))) Dx2) ) <- coerce E0 D0 E0' D0' <- ( {e:exp} {D1arg : typeof+sub e A1} {D1arg' : typeof e A1} {_ : coerce e D1arg e D1arg'} coerce (EH e) (D1 e D1arg) (E1 e) (D1' e D1arg') ) <- ( {e:exp} {D2arg : typeof+sub e A2} {D2arg' : typeof e A2} {_ : coerce e D2arg e D2arg'} coerce (EH e) (D2 e D2arg) (E2 e) (D2' e D2arg') ) . coerce/direct : {A1 : ty} {C : ty} {E0:exp} {D0:typeof+sub E0 A1} {E0':exp} {D0':typeof E0' A1} {EC:eval-context} {EH:exp -> exp} {Fill : fill EC EH} {D1:{x:exp} typeof+sub x A1 -> typeof+sub (EH x) C} {D1':{x:exp} typeof x A1 -> typeof (E1 x) C} coerce (EH E0) (typeof+sub/direct Fill D0 D1) (app (lam [y] E1 y) E0') (typeof/direct (ec/app2 (lam ([y] E1 y)) (is-value/lam) (ec/hole)) (fill/app2 (fill/hole)) D0' ([x1] [Dx1] typeof/arrelim (typeof/arrintro ([y] [Dy] D1' y Dy)) Dx1) ) <- coerce E0 D0 E0' D0' <- ( {e:exp} {D1arg : typeof+sub e A1} {D1arg' : typeof e A1} {_ : coerce e D1arg e D1arg'} coerce (EH e) (D1 e D1arg) (E1 e) (D1' e D1arg') ) . - : coerce (merge E1 E2) (typeof+sub/merge1 D1) (merge E1' E2) (typeof/merge1 D1') <- coerce E1 D1 E1' D1'. - : coerce (merge E1 E2) (typeof+sub/merge2 D2) (merge E1 E2') (typeof/merge2 D2') <- coerce E2 D2 E2' D2'. - : coerce (app E1 E2) (typeof+sub/arrelim D1 D2) (app E1' E2') (typeof/arrelim D1' D2') <- coerce E1 D1 E1' D1' <- coerce E2 D2 E2' D2'. - : coerce (fix ([u] Ebody u)) (typeof+sub/fix D) (fix ([u'] Ebody' u')) (typeof/fix D') <- ( {e:exp} {DFix : typeof+sub e A} {DFix' : typeof e A} {_ : coerce e DFix e DFix'} coerce (Ebody e) (D e DFix) (Ebody' e) (D' e DFix') ). - : coerce _ (typeof+sub/arrintro D) _ (typeof/arrintro D') <- ( {e:exp} {DArg : typeof+sub e A} {DArg' : typeof e A} {_ : coerce e DArg e DArg'} coerce _ (D e DArg) _ (D' e DArg') ). - : coerce E (typeof+sub/sub Coe CoeTyping D Sub) (Coe E') (CoeTyping E' D') <- coerce E D E' D'. %block coerce\block : some {A : ty} block {e : exp} {D : typeof+sub e A} {D' : typeof e A} {_ : coerce e D e D'}. %worlds (coerce\block) (coerce _ _ _ _). %total {D} (coerce _ D _ _).