From 850285cff0a88f652d4ee4251fc0cfb700712d75 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Sun, 8 Sep 2024 15:29:47 +0200 Subject: [PATCH] morphism paths: add Lift path --- coq/morph.v | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/coq/morph.v b/coq/morph.v index 01ea18c..8b7855c 100644 --- a/coq/morph.v +++ b/coq/morph.v @@ -30,6 +30,10 @@ Inductive morphism_path : context -> type_term -> type_term -> Prop := (Γ |- τ' ~> τ'') -> (Γ |- τ ~> τ'') + | M_Lift : forall Γ σ τ τ', + (Γ |- τ ~> τ') -> + (Γ |- (type_ladder σ τ) ~> (type_ladder σ τ')) + | M_MapSeq : forall Γ τ τ', (Γ |- τ ~> τ') -> (Γ |- (type_spec (type_id "Seq") τ) ~> (type_spec (type_id "Seq") τ'))