Я обнаружил, что между логикой и программированием существует изоморфизм, называемыйПереписка Карри-ГовардаТак есть ли такая эквивалентность для теории категорий, которая помогает понимать такие вещи, как функторы или монады?