[Agda] Lambda terms as a natural transformation.

[effectfully]

Hi. I tried to rewrite the code from the "Relative monads formalized"
paper ([1]) using in the category of contexts order preserving
embeddings ([2]) as morphisms instead of functions, but then I
realized that substitution is a functor from ConCat to Fam Ty as well
as renaming:

    ren : ∀ {Γ Δ σ} -> Γ ⊆ Δ -> σ ∈ Γ -> σ ∈ Δ
    sub : ∀ {Γ Δ σ} -> Γ ⊆ Δ -> Γ ⊢ σ -> Δ ⊢ σ

    Ren : Functor ConCat (Fam Ty)
    Sub : Functor ConCat (Fam Ty)

Terms then form a natural transformation between these functors:

    Term : NaturalTransformation Ren Sub
    Term = record
      { η          = var
      ; naturality = λ v -> refl
      }

This is completely trivial. Is this well-known?

The code (with a bit different names) can be found at [3].

[1] http://cs.ioc.ee/~james/papers/AssistedMonads2.pdf
[2] http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=91
[3] https://github.com/effectfully/Categories/blob/master/NaturalTransformation/Lambda.agda