Require Import debruijn.
Require Import equiv.
Require Import subtype.
Require Import env.
Require Import Atom.
Import AtomImpl.
From Coq Require Import Lists.List.
Import ListNotations.
Require Import Environment.

Open Scope ladder_type_scope.
Open Scope ladder_expr_scope.

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

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

  | M_Single : forall Γ h τ τ',
    (binds h [< τ ->morph τ' >] Γ) ->
    (Γ |- τ ~~> τ')

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

  | M_Lift : forall Γ σ τ τ',
    (Γ |- τ ~~> τ') ->
    (Γ |- [< σ ~ τ >] ~~> [< σ ~ τ' >])

  | M_MapSeq : forall Γ τ τ',
    (Γ |- τ ~~> τ') ->
    (Γ |- [< [τ] >] ~~> [< [τ'] >])

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

Lemma id_morphism_path : forall Γ τ, Γ |- τ ~~> τ.
Proof.
  intros.
  apply M_Sub, TSubRepr_Refl, TEq_Refl.
Qed.




Reserved Notation "Γ '|-' '[[' σ '~~>' τ ']]' '=' m" (at level 101).

(* some atom for the 'map' function on lists *)
Parameter at_map : atom.

Inductive translate_morphism_path : env -> type_DeBruijn -> type_DeBruijn -> expr_DeBruijn -> Prop :=
  | Translate_Descend : forall Γ τ τ',
    (τ :<= τ') ->
    (Γ |- [[ τ ~~> τ' ]] = [{ λ τ ↦morph (%0 des τ') }])

  | Translate_Lift : forall Γ σ τ τ' m,
    (Γ |- τ ~~> τ') ->
    (Γ |- [[ τ ~~> τ' ]] = m) ->
    (Γ |- [[ [< σ~τ >] ~~> [< σ~τ' >] ]] =
      [{ λ (σ ~ τ) ↦morph (m (%0 des τ)) as σ }])

  | Translate_Single : forall Γ h τ τ',
    binds h [< τ ->morph τ' >] Γ ->
    (Γ |- [[ τ ~~> τ' ]] = [{ $h }])

  | Translate_Chain : forall Γ τ τ' τ'' m1 m2,
    (Γ |- [[ τ ~~> τ' ]] = m1) ->
    (Γ |- [[ τ' ~~> τ'' ]] = m2) ->
    (Γ |- [[ τ ~~> τ'' ]] = [{ λ τ ↦morph m2 (m1 %0) }])

  | Translate_MapSeq : forall Γ τ τ' m,
    (Γ |- [[ τ ~~> τ' ]] = m) ->
    (Γ |- [[ [< [τ] >] ~~> [< [τ'] >] ]] =
      [{
        λ [τ] ↦morph ($at_map # τ # τ' m %0)
      }])

where "Γ '|-' '[[' σ '~~>' τ ']]' = m" := (translate_morphism_path Γ σ τ m).