module Palmse.Combinators.TyTm where open import Data.List infixr 10 _=>_ infixl 3 _´_ data Ty : Set where N : Ty _=>_ : Ty -> Ty -> Ty data Tm : Ty -> Set where ze : Tm N su : Tm (N => N) k : {a b : Ty} -> Tm (a => b => a) s : {a b c : Ty} -> Tm ((a => b => c) => (a => b) => a => c) _´_ : {a b : Ty} -> Tm (a => b) -> Tm a -> Tm b=