2 Sep 14:41 2015

### Lambda terms as a natural transformation.

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