coq/bbencode.v

@@ -69,7 +69,7 @@ Compute (expr_subst "x"
 Example  example_let_reduction :
     e1 -->β  (expr_app (expr_app (expr_var "+") bb_zero) bb_zero).
 Proof.
-    apply E_Let.
+    apply E_AppLet.
 Qed.
 
 Compute     (expr_app bb_succ bb_zero) -->β bb_one.

coq/equiv.v

@@ -218,16 +218,6 @@ Inductive type_eq : type_term -> type_term -> Prop :=
     y === z ->
     x === z
 
-  | TEq_LadderAssocLR : forall x y z,
-    (type_ladder (type_ladder x y) z)
-    ===
-    (type_ladder x (type_ladder y z))
-
-  | TEq_LadderAssocRL : forall x y z,
-    (type_ladder x (type_ladder y z))
-    ===
-    (type_ladder (type_ladder x y) z)
-
   | TEq_Alpha : forall x y,
     x --->α y ->
     x === y
@@ -257,9 +247,6 @@ Proof.
   apply TEq_Trans with (y:=y).
   apply IHtype_eq2.
   apply IHtype_eq1.
-  
-  apply TEq_LadderAssocRL.
-  apply TEq_LadderAssocLR.
 
   apply type_alpha_symm in H.
   apply TEq_Alpha.

coq/morph.v

@@ -52,7 +52,7 @@ Inductive translate_morphism_path : context -> type_term -> type_term -> expr_te
     (translate_morphism_path Γ τ τ' m) ->
     (translate_morphism_path Γ (type_ladder σ τ) (type_ladder σ τ')
         (expr_morph "x" (type_ladder σ τ)
-          (expr_ascend σ (expr_app m (expr_descend τ (expr_var "x"))))))
+          (expr_ascend (type_ladder σ τ') (expr_app m (expr_descend τ (expr_var "x"))))))
 
   | Translate_Single : forall Γ h τ τ',
     (context_contains Γ h (type_morph τ τ')) ->

coq/smallstep.v

@@ -61,8 +61,8 @@ Inductive beta_step : expr_term -> expr_term -> Prop :=
     e -->β e' ->
     (expr_ty_app e τ) -->β (expr_ty_app e' τ)
 
-  | E_TypAppLam : forall α e τ,
-    (expr_ty_app (expr_ty_abs α e) τ) -->β (expr_specialize α τ e)
+  | E_TypAppLam : forall x e a,
+    (expr_ty_app (expr_ty_abs x e) a) -->β (expr_specialize x a e)
 
   | E_AppLam : forall x τ e a,
     (expr_app (expr_abs x τ e) a) -->β (expr_subst x a e)
@@ -70,25 +70,8 @@ Inductive beta_step : expr_term -> expr_term -> Prop :=
   | E_AppMorph : forall x τ e a,
     (expr_app (expr_morph x τ e) a) -->β (expr_subst x a e)
 
-  | E_Let : forall x e a,
-    (expr_let x a e) -->β (expr_subst x a e)
-
-  | E_StripAscend : forall τ e,
-    (expr_ascend τ e) -->β e
-
-  | E_StripDescend : forall τ e,
-    (expr_descend τ e) -->β e
-
-  | E_Ascend : forall τ e e',
-    (e -->β e') ->
-    (expr_ascend τ e) -->β (expr_ascend τ e')
-
-  | E_AscendCollapse : forall τ' τ e,
-    (expr_ascend τ' (expr_ascend τ e)) -->β (expr_ascend (type_ladder τ' τ) e)
-
-  | E_DescendCollapse : forall τ' τ e,
-    (τ':<=τ) ->
-    (expr_descend τ (expr_descend τ' e)) -->β (expr_descend τ e)
+  | E_AppLet : forall x t e a,
+    (expr_let x t a e) -->β (expr_subst x a e)
 
 where "s '-->β' t" := (beta_step s t).
 
@@ -102,43 +85,4 @@ Inductive multi {X : Type} (R : X -> X -> Prop) : X -> X -> Prop :=
 Notation " s -->α* t " := (multi expr_alpha s t) (at level 40).
 Notation " s -->β* t " := (multi beta_step s t) (at level 40).
 
-
-
-Example reduce1 :
-  [{
-    let "deg2turns" :=
-       (λ"x" $"Angle"$~$"Degrees"$~$"ℝ"$
-                ↦morph ((%"/"% (%"x"% des $"ℝ"$) %"360"%) as $"Angle"$~$"Turns"$))
-    in ( %"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$) )
-  }]
-  -->β*
-  [{
-     ((%"/"% %"60"%) %"360"%) as $"Angle"$~$"Turns"$
-  }].
-Proof.
-  apply Multi_Step with (y:=[{ (λ"x" $"Angle"$~$"Degrees"$~$"ℝ"$
-                ↦morph (((%"/"% (%"x"% des $"ℝ"$)) %"360"%) as $"Angle"$~$"Turns"$)) (%"60"% as $"Angle"$~$"Degrees"$) }]).
-  apply E_Let.
-
-  apply Multi_Step with (y:=(expr_subst "x" [{%"60"% as $"Angle"$~$"Degrees"$}]  [{ (((%"/"% (%"x"% des $"ℝ"$)) %"360"%) as $"Angle"$~$"Turns"$) }])).
-  apply E_AppMorph.
-  simpl.
-
-  apply Multi_Step with (y:=[{ ((%"/"% (%"60"% as $"Angle"$~$"Degrees"$)) %"360"%) as $"Angle"$~$"Turns"$ }]).
-  apply E_Ascend.
-  apply E_App1.
-  apply E_App2.
-  apply V_Abs, VAbs_Var.
-  apply E_StripDescend.
-
-  apply Multi_Step with (y:=[{ (%"/"% %"60"% %"360"%) as $"Angle"$~$"Turns"$ }]).
-  apply E_Ascend.
-  apply E_App1.
-  apply E_App2.
-  apply V_Abs, VAbs_Var.
-  apply E_StripAscend.
-
-  apply Multi_Refl.
-Qed.
-
 End Smallstep.

coq/soundness.v

@@ -16,402 +16,40 @@ Include Typing.
 
 Module Soundness.
 
-
-Lemma typing_weakening : forall Γ e τ x σ,
-  (Γ |- e \is τ) ->
-  ((ctx_assign x σ Γ) |- e \is τ)
-.
-Proof.
-  intros.
-  induction H.
-
-  apply T_Var.
-  apply C_shuffle.
-  apply H.
-  
-  apply T_Let with (σ:=σ0).
-  apply IHexpr_type1.
-  admit.
-
-Admitted.
-
-
-Lemma morphism_path_solves_type : forall Γ τ τ' m,
-  (translate_morphism_path Γ τ τ' m) ->
-  Γ |- m \is (type_morph τ τ')
-.
-Proof.
-  intros.
-  induction H.
-
-  (* Sub *)
-  apply T_MorphAbs.
-  apply T_DescendImplicit with (τ:=τ).
-  apply T_Var.
-  apply C_take.
-  apply H.
-
-  (* Lift *)
-  apply T_MorphAbs.
-  apply T_Ascend.
-  apply T_App with (σ':=τ) (σ:=τ).
-  apply T_MorphFun.
-  apply typing_weakening.
-  apply IHtranslate_morphism_path.
-  apply T_Descend with (τ:=(type_ladder σ τ)).
-  apply T_Var.
-  apply C_take.
-  apply TSubRepr_Ladder, TSubRepr_Refl, TEq_Refl.
-  apply M_Sub, TSubRepr_Refl, TEq_Refl.
-
-  (* Single *)
-  apply T_Var.
-  apply H.
-
-  (* Chain *)
-  apply T_MorphAbs.
-  apply T_App with (σ':=τ') (σ:=τ') (τ:=τ'').
-  apply T_MorphFun.
-  apply typing_weakening.
-  apply IHtranslate_morphism_path2.
-  
-  apply T_App with (σ':=τ) (σ:=τ) (τ:=τ').
-  apply T_MorphFun.
-  apply typing_weakening.
-  apply IHtranslate_morphism_path1.
-
-  apply T_Var.
-  apply C_take.
-  apply M_Sub, TSubRepr_Refl, TEq_Refl.
-  apply M_Sub, TSubRepr_Refl, TEq_Refl.
-
-  (* Map Sequence *)
-  apply T_MorphAbs.
-  apply T_App with (σ':=(type_spec (type_id "Seq") τ)) (σ:=(type_spec (type_id "Seq") τ)).
-  apply T_App with (σ':=(type_fun τ τ')) (σ:=(type_fun τ τ')).
-
-  admit.
-
-  apply T_MorphFun.
-  apply typing_weakening.
-  apply IHtranslate_morphism_path.
-  apply M_Sub, TSubRepr_Refl, TEq_Refl.
-
-  apply T_Var.
-  apply C_take.
-  apply M_Sub, TSubRepr_Refl, TEq_Refl.
-Admitted.
-
-(* reduction step preserves well-typedness *)
-Lemma preservation : forall Γ e e' τ,
-  ~(is_value e) ->
-  (Γ |- e \is τ) ->
-  (e -->β e') ->
-  (Γ |- e' \is τ)
-.
-Proof.
-  intros.
-  induction e.
-
-  (* `e` is Variable *)
-  contradict H.
-  apply V_Abs, VAbs_Var.
-
-  (* `e` is Type-Abstraction *)
-  contradict H.
-  apply V_Abs, VAbs_TypAbs.
-
-  (* `e` is Type-Application *)
-  admit.
-
-  (* `e` is Abstraction *)
-  contradict H.
-  apply V_Abs, VAbs_Abs.
-
-  (* `e` is morphism *)
-  contradict H.
-  apply V_Abs, VAbs_Morph.
-
-  (* `e` is Application *)
-  admit.
-
-  (* `e` is Let-Binding *)
-  admit.
-
-  (* `e` is Ascension *)
-  admit.
-
-  (* `e` is Descension *)
-  admit.
-Admitted.
-
-(* translation of expression preserves typing *)
-Lemma translation_preservation : forall Γ e e' τ,
-  (Γ |- e \is τ) ->
-  (translate_typing Γ e τ e') ->
-  (Γ |- e' \is τ)
-.
-Proof.
-  intros.  
-  induction H0.
-
-  (* e is Variable *)
-  apply H.
-
-  (* e is Let-Binding *)
-  apply T_Let with (τ:=τ) (σ:=σ).
-  apply IHtranslate_typing1.
-  apply H0.
-  apply IHtranslate_typing2.
-  apply H1.
-
-  (* e is Type-Abstraction *)
-  apply T_TypeAbs.
-  apply IHtranslate_typing.
-  apply H0.
-
-  (* e is Type-Application *)
-  admit.
-
-  (* e is Abstraction *)
-  apply T_Abs.
-  apply IHtranslate_typing.
-  apply H0.
-
-  (* e is Morphism-Abstraction *)
-  apply T_MorphAbs.
-  apply IHtranslate_typing.
-  apply H0.
-
-  (* e is Application *)
-  apply T_App with (σ':=σ) (σ:=σ) (τ:=τ).
-  apply IHtranslate_typing1.
-  apply H0.
-
-  induction H3.
-
-    (* Repr-Subtype *)
-    apply T_App with (σ':=τ0) (σ:=τ0) (τ:=τ').
-    apply T_MorphFun.
-    apply T_MorphAbs.
-    apply T_DescendImplicit with (τ:=τ0).
-    apply T_Var.
-    apply C_take.
-    apply H3.
-
-    apply T_DescendImplicit with (τ:=τ0).
-    apply IHtranslate_typing2.
-    apply H1.
-    apply TSubRepr_Refl, TEq_Refl.
-    apply M_Sub, TSubRepr_Refl, TEq_Refl.
-
-    (* Lifted Morphism *)
-    apply T_App with (σ':=(type_ladder σ τ0)) (σ:=(type_ladder σ τ0)) (τ:=(type_ladder σ τ')).
-    apply T_MorphFun.
-    apply T_MorphAbs.
-    apply T_Ascend with (τ:=τ').
-    apply T_App with (σ':=τ0) (σ:=τ0) (τ:=τ').
-    apply T_MorphFun.
-    apply typing_weakening.
-    apply morphism_path_solves_type.
-    apply H4.
-
-    apply T_Descend with (τ:=(type_ladder σ τ0)).
-    apply T_Var.
-    apply C_take.
-
-    apply TSubRepr_Ladder, TSubRepr_Refl, TEq_Refl.
-    apply M_Sub, TSubRepr_Refl, TEq_Refl.
-    apply IHtranslate_typing2.
-    apply H1.
-
-    apply M_Sub, TSubRepr_Refl, TEq_Refl.
-
-    (* argument coecrion is single function variable *)
-    apply T_App with (σ':= τ0) (σ:=τ0).
-    apply T_MorphFun.
-    apply T_Var.
-    apply H3.
-    apply IHtranslate_typing2.
-    apply H1.
-    (* lemma: every context implies identity morphism *)
-    apply M_Sub, TSubRepr_Refl, TEq_Refl.
-
-    (* argument coecrion is chain of coercions *)
-    apply T_App with (σ':=τ0) (σ:=τ0).
-    apply T_MorphFun.
-    apply T_MorphAbs.
-    apply T_App with (σ':=τ') (σ:=τ').
-    apply T_MorphFun.
-    apply typing_weakening.
-    apply morphism_path_solves_type.
-    apply H3_0.
-    apply T_App with (σ':=τ0) (σ:=τ0).
-    apply T_MorphFun.
-    apply typing_weakening.
-    apply morphism_path_solves_type.
-    apply H3_.
-    apply T_Var.
-    apply C_take.
-    (* lemma: every context implies identity morphism *)
-    apply M_Sub, TSubRepr_Refl, TEq_Refl.
-    (* lemma: every context implies identity morphism *)
-    apply M_Sub, TSubRepr_Refl, TEq_Refl.
-    apply IHtranslate_typing2.
-    apply H1.
-    (* lemma: every context implies identity morphism *)
-    apply M_Sub, TSubRepr_Refl, TEq_Refl.
-
-    (* argument coercion is is map *)
-(*
-    apply T_App with (σ':=(type_spec (type_id "Seq") τ0)) (σ:=(type_spec (type_id "Seq") τ0)).
-    apply T_MorphFun.
-    apply T_MorphAbs.
-    apply T_App with (σ':=(type_spec (type_id "Seq") τ0)) (σ:=(type_spec (type_id "Seq") τ0)).
-    apply T_App with (σ':=(type_fun τ0 τ')) (σ:=(type_fun τ0 τ')).
-    apply T_TypeApp with
-      (α:="T2"%string)
-      (e:=(expr_ty_app (expr_var "map") τ0))
-      (τ:=(type_fun
-            (type_fun τ0 τ')
-            (type_fun
-              (type_spec (type_id "Seq") τ0)
-              (type_spec (type_id "Seq") τ')))).
-
-    apply T_TypeApp with
-      (α:="T1"%string)
-      (e:=(expr_var "map"))
-      (τ:=(type_univ "T2"
-          (type_fun
-            (type_fun τ0 τ')
-            (type_fun
-              (type_spec (type_id "Seq") (type_var "T1"))
-              (type_spec (type_id "Seq") (type_var "T2")))))).
-
-    apply T_Var.
-    admit.
-
-    apply TSubst_VarReplace.
-    apply TSubst_UnivReplace.
-*)
-    admit.
-
-    (* argument coercion *)
-    apply M_Sub, TSubRepr_Refl, TEq_Refl.
-
-  (* end case `e application` *)
-
-  (* e is Morphism *)
-  apply T_MorphFun.
-  apply IHtranslate_typing.
-  apply H0.
-
-  (* e is Ascension *)
-  apply T_Ascend.
-  apply IHtranslate_typing.
-  apply H0.
-
-  (* e is Desecension *)
-  apply T_DescendImplicit with (τ:=τ).
-  apply IHtranslate_typing.
-  apply H0.
-  apply H1.
-Admitted.
-
 (* e is stuck when it is neither a value, nor can it be reduced *)
 Definition is_stuck (e:expr_term) : Prop :=
   ~(is_value e) ->
   ~(exists e', e -->β e')
 .
 
-(* the translation any well typed term is not stuck *)
+(* every well typed term is not stuck *)
 Lemma progress :
-  forall Γ e τ e',
+  forall (e:expr_term),
+  (is_well_typed e) -> ~(is_stuck e)
+.
+Proof.
+  
+Admitted.
+
+(* reduction step preserves well-typedness *)
+Lemma preservation :
+  forall Γ e e' τ,
   (Γ |- e \is τ) ->
-  (translate_typing Γ e τ e') ->
-  ~(is_stuck e')
+  (e -->β e') ->
+  (Γ |- e' \is τ)
 .
 Proof.
 Admitted.
 
-(* every well-typed expression is translated,
- * such that it be reduced to a value
- *)
+(* every well-typed expression can be reduced to a value *)
 Theorem soundness :
-  forall Γ e e' τ,
-  (Γ |- e \is τ) ->
-  (translate_typing Γ e τ e') ->
-  (exists v, (e' -->β* v) /\ (is_value v) /\ (Γ |- v \is τ))
+  forall (e:expr_term),
+  (is_well_typed e) ->
+  (exists e', e -->β* e' /\ (is_value e'))
 .
 Proof.
   intros.
-
-  (* `e` is Variable *)
-  induction H0.
-  exists (expr_var x).
-  split. apply Multi_Refl.
-  split. apply V_Abs,VAbs_Var.
-  apply H.
-
-  (* `e` is Let-Binding *)
-  exists (expr_subst x e' t').
-  split.
-  apply Multi_Step with (y:=(expr_subst x e' t')).
-  apply E_Let with (x:=x) (a:=e') (e:=t').
-  apply Multi_Refl.
-(*
-  split.
-  unfold expr_subst.
-  induction t'.
   
-  exists (expr_subst x e' (expr_var s)).
-  split.
-  unfold expr_subst.
-  apply E_Let.
-  *)
-  admit.
-
-  (* `e` is Type-Abstraction *)
-  exists (expr_ty_abs α e').
-  split.
-  apply Multi_Refl.
-  split.
-  apply V_Abs, VAbs_TypAbs.
-  apply T_TypeAbs.
-  apply translation_preservation with (e:=e).
-  apply H0.
-  apply H1.
-
-  (* `e` is Type-Application *)
-  admit.
-
-  (* `e`is Abstraction *)
-  exists (expr_abs x σ e').
-  split. apply Multi_Refl.
-  split. apply V_Abs, VAbs_Abs.
-  apply T_Abs.
-  apply translation_preservation with (e:=e).
-  apply H0.
-  apply H2.
-
-  (* `e` is Morphism Abstraction *)
-  exists (expr_morph x σ e').
-  split. apply Multi_Refl.
-  split. apply V_Abs, VAbs_Morph.
-  apply T_MorphAbs.
-  apply translation_preservation with (e:=e).
-  apply H0.
-  apply H2.
-
-  (* `e` is Application *)
-  admit.
-  admit.
-
-  (* `e` is Ascension *)
-  admit.
-
-  (* `e` is Descension *)
-  admit.
 Admitted.
 
 End Soundness.

coq/terms.v

@@ -30,35 +30,46 @@ Inductive expr_term : Type :=
   | expr_descend : type_term -> expr_term -> expr_term
 .
 
-(* values *)
-Inductive is_abs_value : expr_term -> Prop :=
-  | VAbs_Var : forall x,
-    (is_abs_value (expr_var x))
+(* TODO
 
-  | VAbs_Abs : forall x τ e,
-    (is_abs_value (expr_abs x τ e))
+Inductive type_DeBruijn : Type :=
+  | id : nat -> type_DeBruijn
+  | var : nat -> type_DeBruijn
+  | fun : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
+  | univ : type_DeBruijn -> type_DeBruijn
+  | spec : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
+  | morph : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
+  | ladder : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
 
-  | VAbs_Morph : forall x τ e,
-    (is_abs_value (expr_morph x τ e))
-
-  | VAbs_TypAbs : forall τ e,
-    (is_abs_value (expr_ty_abs τ e))
+Inductive expr_DeBruijn : Type :=
+  | var : nat -> expr_DeBruijn
+  | ty_abs : expr_DeBruijn -> expr_DeBruijn
+  | ty_app : expr_DeBruijn -> type_DeBruijn -> expr_Debruijn
+  | abs   : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
+  | morph : type_DeBruijn -> expr_DeBruijn -> expr_Debruijn
+  | app : expr_DeBruijn -> expr_DeBruijn -> expr_Debruijn
+  | let : type_DeBruijn -> expr_DeBruijn -> expr_Debruijn -> expr_Debruijn
+  | ascend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
+  | descend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
 .
+*)
 
+
+
+(* values *)
 Inductive is_value : expr_term -> Prop :=
-  | V_Abs : forall e,
-    (is_abs_value e) ->
-    (is_value e)
+  | V_Abs : forall x τ e,
+    (is_value (expr_abs x τ e))
+
+  | V_TypAbs : forall τ e,
+    (is_value (expr_ty_abs τ e))
 
   | V_Ascend : forall τ e,
-    (is_abs_value e) ->
+    (is_value e) ->
     (is_value (expr_ascend τ e))
-
-  | V_Descend : forall τ e,
-    (is_abs_value e) ->
-    (is_value (expr_descend τ e))
 .
 
+
 Declare Scope ladder_type_scope.
 Declare Scope ladder_expr_scope.
 Declare Custom Entry ladder_type.
@@ -97,8 +108,6 @@ Notation "'let' x ':=' e 'in' t" := (expr_let x e t)
   (in custom ladder_expr at level 20, x constr, e custom ladder_expr at level 99, t custom ladder_expr at level 99) : ladder_expr_scope.
 Notation "e 'as' τ" := (expr_ascend τ e)
   (in custom ladder_expr at level 30, e custom ladder_expr, τ custom ladder_type at level 99) : ladder_expr_scope.
-Notation "e 'des' τ" := (expr_descend τ e)
-  (in custom ladder_expr at level 30, e custom ladder_expr, τ custom ladder_type at level 99) : ladder_expr_scope.
 Notation "e1 e2" := (expr_app e1 e2)
   (in custom ladder_expr at level 50) : ladder_expr_scope.
 Notation "'(' e ')'" := e

coq/typing.v

@@ -61,7 +61,8 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
 
   | T_Ascend : forall Γ e τ τ',
     (Γ |- e \is τ) ->
-    (Γ |- (expr_ascend τ' e) \is (type_ladder τ' τ))
+    (τ' :<= τ) ->
+    (Γ |- (expr_ascend τ' e) \is τ')
 
   | T_DescendImplicit : forall Γ x τ τ',
     Γ |- x \is τ ->
@@ -76,8 +77,7 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
 where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).
 
 Definition is_well_typed (e:expr_term) : Prop :=
-  forall Γ,
-  exists τ,
+  exists Γ τ,
   Γ |- e \is τ
 .
 
@@ -135,9 +135,10 @@ Inductive translate_typing : context -> expr_term -> type_term -> expr_term -> P
 
   | Expand_Ascend : forall Γ e e' τ τ',
     (Γ |- e \is τ) ->
-    (Γ |- (expr_ascend τ' e) \is (type_ladder τ' τ)) ->
+    (τ' :<= τ) ->
+    (Γ |- (expr_ascend τ' e) \is τ') ->
     (translate_typing Γ e τ e') ->
-    (translate_typing Γ (expr_ascend τ' e) (type_ladder τ' τ) (expr_ascend τ' e'))
+    (translate_typing Γ (expr_ascend τ' e) τ' (expr_ascend τ' e'))
 
   | Expand_Descend : forall Γ e e' τ τ',
     (Γ |- e \is τ) ->
@@ -218,6 +219,7 @@ Example typing4 : (is_well_typed
 ).
 Proof.
   unfold is_well_typed.
+  exists ctx_empty.
   exists [< ∀"T",∀"U",%"T"%->%"U"%->%"T"% >].
   apply T_TypeAbs.
   apply T_TypeAbs.
@@ -229,29 +231,24 @@ Qed.
 
 Open Scope ladder_expr_scope.
 
-Example typing5 :
-  (ctx_assign "60" [< $"ℝ"$ >]
-  (ctx_assign "360" [< $"ℝ"$ >]
-  (ctx_assign "/" [< $"ℝ"$ -> $"ℝ"$ -> $"ℝ"$ >]
-    ctx_empty)))
-  |-
+Example typing5 : (is_well_typed
   [{
     let "deg2turns" :=
        (λ"x" $"Angle"$~$"Degrees"$~$"ℝ"$
-                ↦morph (((%"/"% %"x"%) %"360"%) as $"Angle"$~$"Turns"$))
-    in ( %"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$) )
+                ↦morph (((%"/"% %"x"%) %"360"%) as $"Angle"$~$"Turns"$~$"ℝ"$))
+    in ( %"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$~$"ℝ"$) )
   }]
-  \is
-  [<
-    $"Angle"$~$"Turns"$~$"ℝ"$
-  >]
-.
+).
 Proof.
+  unfold is_well_typed.
+  exists (ctx_assign "60" [< $"ℝ"$ >]
+          (ctx_assign "360" [< $"ℝ"$ >]
+          (ctx_assign "/" [< $"ℝ"$ -> $"ℝ"$ -> $"ℝ"$ >]
+              ctx_empty))).
+  exists [< $"Angle"$~$"Turns"$~$"ℝ"$ >].
   apply T_Let with (σ:=[< $"Angle"$~$"Degrees"$~$"ℝ"$ ->morph $"Angle"$~$"Turns"$~$"ℝ"$ >]).
   apply T_MorphAbs.
-  apply T_DescendImplicit with (τ:=(type_ladder [<$"Angle"$~$"Turns"$>] [<$"ℝ"$>])).
-  2: apply TSubRepr_Refl, TEq_LadderAssocLR.
-  apply T_Ascend with (τ:=[<$"ℝ"$>]) (τ':=[<$"Angle"$~$"Turns"$>]).
+  apply T_Ascend with (τ:=[< $"ℝ"$ >]).
   apply T_App with (σ := [< $"ℝ"$ >]) (σ' := [< $"ℝ"$ >]).
   apply T_App with (σ := [< $"ℝ"$ >]) (σ' := [< $"ℝ"$ >]).
   apply T_Var.
@@ -268,15 +265,18 @@ Proof.
   apply M_Sub.
   apply TSubRepr_Refl.
   apply TEq_Refl.
+  apply TSubRepr_Ladder, TSubRepr_Ladder, TSubRepr_Refl.
+  apply TEq_Refl.
   apply T_App with (σ:=[<$"Angle"$~$"Degrees"$~$"ℝ"$>]) (σ':=[<$"Angle"$~$"Degrees"$~$"ℝ"$>]).
   apply T_MorphFun.
   apply T_Var.
   apply C_take.
-  apply T_DescendImplicit with (τ:=(type_ladder [<$"Angle"$~$"Degrees"$>] [<$"ℝ"$>])).
-  2: apply TSubRepr_Refl, TEq_LadderAssocLR.
-  apply T_Ascend.
+  apply T_Ascend with (τ:=[<$"ℝ"$>]).
   apply T_Var.
   apply C_shuffle. apply C_take.
+  apply TSubRepr_Ladder.
+  apply TSubRepr_Ladder.
+  apply TSubRepr_Refl. apply TEq_Refl.
   apply M_Sub. apply TSubRepr_Refl. apply TEq_Refl.
 Qed.