From 67e4c13d57b47cf8d745d71f3ba6721a1efcab83 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Sat, 21 Sep 2024 06:47:55 +0200
Subject: [PATCH] translate morphism path: fix morph mapping
---
coq/morph_debruijn.v | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/coq/morph_debruijn.v b/coq/morph_debruijn.v
index f4b5872..3cf03a0 100644
--- a/coq/morph_debruijn.v
+++ b/coq/morph_debruijn.v
@@ -54,13 +54,13 @@ Parameter at_map : atom.
Inductive translate_morphism_path : context -> type_DeBruijn -> type_DeBruijn -> expr_DeBruijn -> Prop :=
| Translate_Descend : forall Γ τ τ',
(τ :<= τ') ->
- (Γ |- [[ τ ~~> τ' ]] = [{ λ τ ↦ (%0 des τ') }])
+ (Γ |- [[ τ ~~> τ' ]] = [{ λ τ ↦morph (%0 des τ') }])
| Translate_Lift : forall Γ σ τ τ' m,
(Γ |- τ ~~> τ') ->
(Γ |- [[ τ ~~> τ' ]] = m) ->
(Γ |- [[ [< σ~τ >] ~~> [< σ~τ' >] ]] =
- [{ λ (σ ~ τ) ↦ (m (%0 des τ)) as σ }])
+ [{ λ (σ ~ τ) ↦morph (m (%0 des τ)) as σ }])
| Translate_Single : forall Γ h τ τ',
In (h, [< τ ->morph τ' >]) Γ ->
@@ -69,7 +69,7 @@ Inductive translate_morphism_path : context -> type_DeBruijn -> type_DeBruijn ->
| Translate_Chain : forall Γ τ τ' τ'' m1 m2,
(Γ |- [[ τ ~~> τ' ]] = m1) ->
(Γ |- [[ τ' ~~> τ'' ]] = m2) ->
- (Γ |- [[ τ ~~> τ'' ]] = [{ λ τ ↦ m2 (m1 %0) }])
+ (Γ |- [[ τ ~~> τ'' ]] = [{ λ τ ↦morph m2 (m1 %0) }])
| Translate_MapSeq : forall Γ τ τ' m,
(Γ |- [[ τ ~~> τ' ]] = m) ->