Что такое комбинаторно-логический эквивалент интуиционистской теории типов?

Недавно я закончил университетский курс, посвященный Haskell и Agda (, функциональному языку программирования с зависимой типизацией ), и мне было интересно, можно ли заменить в них лямбда-исчисление комбинаторной логикой. В Haskell это кажется возможным с помощью комбинаторов S и K, что делает его свободным от точек -. Мне было интересно, какой эквивалент был для Агды. То есть, можно ли сделать функциональный язык программирования с зависимой типизацией эквивалентным Agda без использования каких-либо переменных?

Кроме того, можно ли как-то заменить квантификацию комбинаторами? Я не знаю, совпадение ли это, но универсальная количественная оценка, например, делает сигнатуру типа похожей на лямбда-выражение. Есть ли способ удалить универсальную количественную оценку из подписи типа, не меняя ее значения? Например. в:

forall a : Int -> a < 0 -> a + a < a

Можно ли то же самое выразить без использования forall?