This repository contains the agda mechanization of the proofs in the paper titled Exponential Elimination for Bicartesian Closed Categorical Combinators
We show that every term between first-order types in a combinator language with products, sums and exponentials (higher-order functions) can be transformed to first-order terms (which don't use exponentials) in the language when equipped with a distributivity combinator.
Jump to main theorem here: Main.agda
Paper here: http://nachivpn.me/expelim.pdf