ladder-calculus/coq/morph.v

From Coq Require Import Strings.String.
Require Import terms.
Require Import subst.
Require Import equiv.
Require Import subtype.
Require Import context.

Include Terms.
Include Subst.
Include Equiv.
Include Subtype.
Include Context.

Module Morph.

(* Given a context, there is a morphism path from τ to τ' *)
Reserved Notation "Γ '|-' σ '~>' τ" (at level 101, σ at next level, τ at next level).

Inductive morphism_path : context -> type_term -> type_term -> Prop :=
  | M_Sub : forall Γ τ τ',
    (τ :<= τ') ->
    (Γ |- τ ~> τ')

  | M_Single : forall Γ h τ τ',
    (context_contains Γ h (type_morph τ τ')) ->
    (Γ |- τ ~> τ')

  | M_Chain : forall Γ τ τ' τ'',
    (Γ |- τ ~> τ') ->
    (Γ |- τ' ~> τ'') ->
    (Γ |- τ ~> τ'')

  | M_Lift : forall Γ σ τ τ',
    (Γ |- τ ~> τ') ->
    (Γ |- (type_ladder σ τ) ~> (type_ladder σ τ'))

  | M_MapSeq : forall Γ τ τ',
    (Γ |- τ ~> τ') ->
    (Γ |- (type_spec (type_id "Seq") τ) ~> (type_spec (type_id "Seq") τ'))

where "Γ '|-' s '~>' t" := (morphism_path Γ s t).

End Morph.