2024-09-04 12:41:00 +02:00
|
|
|
|
From Coq Require Import Strings.String.
|
|
|
|
|
Require Import terms.
|
|
|
|
|
Require Import subst.
|
|
|
|
|
Require Import equiv.
|
|
|
|
|
Require Import subtype.
|
2024-09-05 12:47:30 +02:00
|
|
|
|
Require Import context.
|
2024-09-04 12:41:00 +02:00
|
|
|
|
|
|
|
|
|
Include Terms.
|
|
|
|
|
Include Subst.
|
|
|
|
|
Include Equiv.
|
|
|
|
|
Include Subtype.
|
2024-09-05 12:47:30 +02:00
|
|
|
|
Include Context.
|
2024-09-04 12:41:00 +02:00
|
|
|
|
|
|
|
|
|
Module Morph.
|
|
|
|
|
|
2024-09-05 12:47:30 +02:00
|
|
|
|
(* Given a context, there is a morphism path from τ to τ' *)
|
|
|
|
|
Reserved Notation "Γ '|-' σ '~>' τ" (at level 101, σ at next level, τ at next level).
|
2024-09-04 12:41:00 +02:00
|
|
|
|
|
2024-09-05 12:47:30 +02:00
|
|
|
|
Inductive morphism_path : context -> type_term -> type_term -> Prop :=
|
|
|
|
|
| M_Sub : forall Γ τ τ',
|
|
|
|
|
(τ :<= τ') ->
|
|
|
|
|
(Γ |- τ ~> τ')
|
2024-09-04 12:41:00 +02:00
|
|
|
|
|
2024-09-05 12:47:30 +02:00
|
|
|
|
| M_Single : forall Γ h τ τ',
|
2024-09-04 12:41:00 +02:00
|
|
|
|
(context_contains Γ h (type_morph τ τ')) ->
|
2024-09-05 12:47:30 +02:00
|
|
|
|
(Γ |- τ ~> τ')
|
2024-09-04 12:41:00 +02:00
|
|
|
|
|
2024-09-05 12:47:30 +02:00
|
|
|
|
| M_Chain : forall Γ τ τ' τ'',
|
|
|
|
|
(Γ |- τ ~> τ') ->
|
|
|
|
|
(Γ |- τ' ~> τ'') ->
|
|
|
|
|
(Γ |- τ ~> τ'')
|
2024-09-04 12:41:00 +02:00
|
|
|
|
|
2024-09-05 12:47:30 +02:00
|
|
|
|
| M_MapSeq : forall Γ τ τ',
|
|
|
|
|
(Γ |- τ ~> τ') ->
|
|
|
|
|
(Γ |- (type_spec (type_id "Seq") τ) ~> (type_spec (type_id "Seq") τ'))
|
2024-09-04 12:41:00 +02:00
|
|
|
|
|
2024-09-05 12:47:30 +02:00
|
|
|
|
where "Γ '|-' s '~>' t" := (morphism_path Γ s t).
|
2024-09-04 12:41:00 +02:00
|
|
|
|
|
2024-09-05 12:47:30 +02:00
|
|
|
|
End Morph.
|