Relating computational effects by ⊤⊤-lifting

We consider the problem of establishing a relationship between two interpretations of base type terms of a λcλc-calculus extended with algebraic operations. We show that the given relationship holds if it satisfies a set of natural conditions. We apply this result to 1) comparing two monadic semantics related by a strong monad morphism, and 2) comparing two monadic semantics of fresh name creation: Starkʼs new name creation monad and the global counter monad. We also consider the same problem, relating semantics of computational effects, in the presence of recursive functions. We apply this additional by extending the previous monad morphism comparison result to the recursive case.