add translate_morphism_path \& morphism path examples

coq/morph.v

@@ -40,4 +40,63 @@ Inductive morphism_path : context -> type_term -> type_term -> Prop :=
 
 where "Γ '|-' s '~>' t" := (morphism_path Γ s t).
 
+
+Inductive translate_morphism_path : context -> type_term -> type_term -> expr_term -> Prop :=
+  | Translate_Subtype : forall Γ τ τ',
+    (τ :<= τ') ->
+    (translate_morphism_path Γ τ τ'
+        (expr_morph "x" τ (expr_var "x")))
+
+  | Translate_Lift : forall Γ σ τ τ' m,
+    (Γ |- τ ~> τ') ->
+    (translate_morphism_path Γ τ τ' m) ->
+    (translate_morphism_path Γ (type_ladder σ τ) (type_ladder σ τ')
+        (expr_morph "x" (type_ladder σ τ)
+          (expr_ascend (type_ladder σ τ') (expr_app m (expr_descend τ (expr_var "x"))))))
+
+  | Translate_Single : forall Γ h τ τ',
+    (context_contains Γ h (type_morph τ τ')) ->
+    (translate_morphism_path Γ τ τ' (expr_var h))
+
+  | Translate_Chain : forall Γ τ τ' τ'' m1 m2,
+    (translate_morphism_path Γ τ τ' m1) -> 
+    (translate_morphism_path Γ τ' τ'' m2) ->
+    (translate_morphism_path Γ τ τ''
+      (expr_morph "x" τ (expr_app m2 (expr_app m1 (expr_var "x")))))
+
+  | Translate_MapSeq : forall Γ τ τ' m,
+    (translate_morphism_path Γ τ τ' m) ->
+    (translate_morphism_path Γ
+      (type_spec (type_id "Seq") τ)
+      (type_spec (type_id "Seq") τ')
+      (expr_morph "xs"
+        (type_spec (type_id "Seq") τ)
+        (expr_app (expr_app (expr_ty_app (expr_ty_app
+          (expr_var "map") τ) τ') m)
+          (expr_var "xs"))))
+.
+
+
+Example morphism_paths :
+  (ctx_assign "degrees-to-turns" [< $"Angle"$~$"Degrees"$~$"ℝ"$ ->morph $"Angle"$~$"Turns"$~$"ℝ"$ >]
+    (ctx_assign "turns-to-radians" [< $"Angle"$~$"Turns"$~$"ℝ"$ ->morph $"Angle"$~$"Radians"$~$"ℝ"$ >]
+      ctx_empty))
+
+  |- [< <$"Seq"$ $"Hue"$~$"Angle"$~$"Degrees"$~$"ℝ"$> >]
+  ~> [< <$"Seq"$ $"Hue"$~$"Angle"$~$"Radians"$~$"ℝ"$> >]
+.
+Proof.
+  intros.
+  apply M_MapSeq.
+  apply M_Lift.
+  apply M_Chain with (τ':=[<$"Angle"$~$"Turns"$~$"ℝ"$>]).
+  apply M_Single with (h:="degrees-to-turns"%string).
+  apply C_take.
+  
+  apply M_Single with (h:="turns-to-radians"%string).
+  apply C_shuffle.
+  apply C_take.
+Qed.
+
+
 End Morph.