From ec955c3c19bd6f89e1e2c6afa37f538ac5044a97 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Thu, 25 Jul 2024 12:41:44 +0200
Subject: [PATCH] coq: add morphism type

---
 coq/subst.v | 1 +
 coq/terms.v | 2 ++
 2 files changed, 3 insertions(+)

diff --git a/coq/subst.v b/coq/subst.v
index 74e586c..1f2b0c8 100644
--- a/coq/subst.v
+++ b/coq/subst.v
@@ -23,6 +23,7 @@ Fixpoint expr_subst (v:string) (n:expr_term) (e0:expr_term) :=
   | expr_ty_abs x e => if (eqb v x) then e0 else expr_ty_abs x (expr_subst v n e)
   | expr_ty_app e t => expr_ty_app (expr_subst v n e) t
   | expr_tm_abs x t e => if (eqb v x) then e0 else expr_tm_abs x t (expr_subst v n e)
+  | expr_tm_abs_morph x t e => if (eqb v x) then e0 else expr_tm_abs_morph x t (expr_subst v n e)
   | expr_tm_app e a => expr_tm_app (expr_subst v n e) (expr_subst v n a)
   | expr_let x t a e => expr_let x t (expr_subst v n a) (expr_subst v n e)
   | expr_ascend t e => expr_ascend t (expr_subst v n e)
diff --git a/coq/terms.v b/coq/terms.v
index de2217d..1930840 100644
--- a/coq/terms.v
+++ b/coq/terms.v
@@ -15,6 +15,7 @@ Inductive type_term : Type :=
   | type_fun : type_term -> type_term -> type_term
   | type_univ : string -> type_term -> type_term
   | type_spec : type_term -> type_term -> type_term
+  | type_morph : type_term -> type_term -> type_term
   | type_ladder : type_term -> type_term -> type_term
 .
 
@@ -24,6 +25,7 @@ Inductive expr_term : Type :=
   | expr_ty_abs : string -> expr_term -> expr_term
   | expr_ty_app : expr_term -> type_term -> expr_term
   | expr_tm_abs : string -> type_term -> expr_term -> expr_term
+  | expr_tm_abs_morph : string -> type_term -> expr_term -> expr_term
   | expr_tm_app : expr_term -> expr_term -> expr_term
   | expr_let : string -> type_term -> expr_term -> expr_term -> expr_term
   | expr_ascend : type_term -> expr_term -> expr_term