change meaning of expr_ascend to only explicitly state the top segment of the type ladder.

also add associativity of ladder types in type-equivalence

coq/equiv.v

@@ -218,6 +218,16 @@ 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
@@ -247,6 +257,9 @@ 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 (type_ladder σ τ') (expr_app m (expr_descend τ (expr_var "x"))))))
+          (expr_ascend σ (expr_app m (expr_descend τ (expr_var "x"))))))
 
   | Translate_Single : forall Γ h τ τ',
     (context_contains Γ h (type_morph τ τ')) ->

coq/soundness.v

@@ -53,7 +53,7 @@ Proof.
 
   (* Lift *)
   apply T_MorphAbs.
-  apply T_Ascend with (τ:=τ').
+  apply T_Ascend.
   apply T_App with (σ':=τ) (σ:=τ).
   apply T_MorphFun.
   apply typing_weakening.
@@ -63,7 +63,6 @@ Proof.
   apply C_take.
   apply TSubRepr_Ladder, TSubRepr_Refl, TEq_Refl.
   apply M_Sub, TSubRepr_Refl, TEq_Refl.
-  apply TSubRepr_Ladder, TSubRepr_Refl, TEq_Refl.
 
   (* Single *)
   apply T_Var.
@@ -216,14 +215,13 @@ Proof.
     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 TSubRepr_Ladder, TSubRepr_Refl, TEq_Refl.
     apply IHtranslate_typing2.
     apply H1.
 
@@ -309,10 +307,9 @@ Proof.
   apply H0.
 
   (* e is Ascension *)
-  apply T_Ascend with (τ:=τ).
+  apply T_Ascend.
   apply IHtranslate_typing.
   apply H0.
-  apply H1.
 
   (* e is Desecension *)
   apply T_DescendImplicit with (τ:=τ).

coq/typing.v

@@ -61,8 +61,7 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
 
   | T_Ascend : forall Γ e τ τ',
     (Γ |- e \is τ) ->
-    (τ' :<= τ) ->
-    (Γ |- (expr_ascend τ' e) \is τ')
+    (Γ |- (expr_ascend τ' e) \is (type_ladder τ' τ))
 
   | T_DescendImplicit : forall Γ x τ τ',
     Γ |- x \is τ ->
@@ -77,7 +76,8 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
 where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).
 
 Definition is_well_typed (e:expr_term) : Prop :=
-  exists Γ τ,
+  forall Γ,
+  exists τ,
   Γ |- e \is τ
 .
 
@@ -135,10 +135,9 @@ Inductive translate_typing : context -> expr_term -> type_term -> expr_term -> P
 
   | Expand_Ascend : forall Γ e e' τ τ',
     (Γ |- e \is τ) ->
-    (τ' :<= τ) ->
-    (Γ |- (expr_ascend τ' e) \is τ') ->
+    (Γ |- (expr_ascend τ' e) \is (type_ladder τ' τ)) ->
     (translate_typing Γ e τ e') ->
-    (translate_typing Γ (expr_ascend τ' e) τ' (expr_ascend τ' e'))
+    (translate_typing Γ (expr_ascend τ' e) (type_ladder τ' τ) (expr_ascend τ' e'))
 
   | Expand_Descend : forall Γ e e' τ τ',
     (Γ |- e \is τ) ->
@@ -219,7 +218,6 @@ 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.
@@ -231,24 +229,29 @@ Qed.
 
 Open Scope ladder_expr_scope.
 
-Example typing5 : (is_well_typed
+Example typing5 :
+  (ctx_assign "60" [< $"ℝ"$ >]
+  (ctx_assign "360" [< $"ℝ"$ >]
+  (ctx_assign "/" [< $"ℝ"$ -> $"ℝ"$ -> $"ℝ"$ >]
+    ctx_empty)))
+  |-
   [{
     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_Ascend with (τ:=[< $"ℝ"$ >]).
+  apply T_DescendImplicit with (τ:=(type_ladder [<$"Angle"$~$"Turns"$>] [<$"ℝ"$>])).
+  2: apply TSubRepr_Refl, TEq_LadderAssocLR.
+  apply T_Ascend with (τ:=[<$"ℝ"$>]) (τ':=[<$"Angle"$~$"Turns"$>]).
   apply T_App with (σ := [< $"ℝ"$ >]) (σ' := [< $"ℝ"$ >]).
   apply T_App with (σ := [< $"ℝ"$ >]) (σ' := [< $"ℝ"$ >]).
   apply T_Var.
@@ -265,18 +268,15 @@ 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_Ascend with (τ:=[<$"ℝ"$>]).
+  apply T_DescendImplicit with (τ:=(type_ladder [<$"Angle"$~$"Degrees"$>] [<$"ℝ"$>])).
+  2: apply TSubRepr_Refl, TEq_LadderAssocLR.
+  apply T_Ascend.
   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.