From 638ddf4fd1a3655264ded3852bf0074702af9e1b Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Sun, 8 Sep 2024 15:34:15 +0200
Subject: [PATCH] coq: add translate_typing

---
 coq/typing.v | 67 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 67 insertions(+)

diff --git a/coq/typing.v b/coq/typing.v
index 7c22901..05e9b2e 100644
--- a/coq/typing.v
+++ b/coq/typing.v
@@ -81,6 +81,73 @@ Definition is_well_typed (e:expr_term) : Prop :=
   Γ |- e \is τ
 .
 
+Inductive translate_typing : context -> expr_term -> type_term -> expr_term -> Prop :=
+  | Expand_Var : forall Γ x τ,
+    (Γ |- (expr_var x) \is τ) ->
+    (translate_typing Γ (expr_var x) τ (expr_var x))
+
+  | Expand_Let : forall Γ x e e' t t' σ τ,
+    (Γ |- e \is σ) ->
+    ((ctx_assign x σ Γ) |- t \is τ) ->
+    (translate_typing Γ e σ e') ->
+    (translate_typing (ctx_assign x σ Γ) t τ t') ->
+    (translate_typing Γ (expr_let x e t) τ (expr_let x e' t'))
+
+  | Expand_TypeAbs : forall Γ α e e' τ,
+    (Γ |- e \is τ) ->
+    (translate_typing Γ e τ e') ->
+    (translate_typing Γ
+      (expr_ty_abs α e)
+      (type_univ α τ)
+      (expr_ty_abs α e'))
+
+  | Expand_TypeApp : forall Γ e e' σ α τ,
+    (Γ |- e \is (type_univ α τ)) ->
+    (translate_typing Γ e τ e') ->
+    (translate_typing Γ (expr_ty_app e τ) (type_subst α σ τ) (expr_ty_app e' τ))
+
+  | Expand_Abs : forall Γ x σ e e' τ,
+    ((ctx_assign x σ Γ) |- e \is τ) ->
+    (Γ |- (expr_abs x σ e) \is (type_fun σ τ)) ->
+    (translate_typing (ctx_assign x σ Γ) e τ e') ->
+    (translate_typing Γ (expr_abs x σ e) (type_fun σ τ) (expr_abs x σ e'))
+
+  | Expand_MorphAbs : forall Γ x σ e e' τ,
+    ((ctx_assign x σ Γ) |- e \is τ) ->
+    (Γ |- (expr_abs x σ e) \is (type_fun σ τ)) ->
+    (translate_typing (ctx_assign x σ Γ) e τ e') ->
+    (translate_typing Γ (expr_morph x σ e) (type_morph σ τ) (expr_morph x σ e'))
+
+  | Expand_App : forall Γ f f' a a' m σ τ σ',
+    (Γ |- f \is (type_fun σ τ)) ->
+    (Γ |- a \is σ') ->
+    (Γ |- σ' ~> σ) ->
+    (translate_typing Γ f (type_fun σ τ) f') ->
+    (translate_typing Γ a σ' a') ->
+    (translate_morphism_path Γ σ' σ m) ->
+    (translate_typing Γ (expr_app f a) τ (expr_app f' (expr_app m a')))
+
+  | Expand_MorphFun : forall Γ f f' σ τ,
+    (Γ |- f \is (type_morph σ τ)) ->
+    (Γ |- f \is (type_fun σ τ)) ->
+    (translate_typing Γ f (type_morph σ τ) f') ->
+    (translate_typing Γ f (type_fun σ τ) f')
+
+  | Expand_Ascend : forall Γ e e' τ τ',
+    (Γ |- e \is τ) ->
+    (τ' :<= τ) ->
+    (Γ |- (expr_ascend τ' e) \is τ') ->
+    (translate_typing Γ e τ e') ->
+    (translate_typing Γ (expr_ascend τ' e) τ' (expr_ascend τ' e'))
+
+  | Expand_Descend : forall Γ e e' τ τ',
+    (Γ |- e \is τ) ->
+    (τ :<= τ') ->
+    (Γ |- e \is τ') ->
+    (translate_typing Γ e τ e') ->
+    (translate_typing Γ e τ' e')
+.
+
 (* Examples *)
 
 Example typing1 :