agda workbook for TypeTheory course (Maietti, Sambin) module TypeTheory where -- import natural to have a better rappresentation inside the script open import Data.Nat using (ℕ; zero; suc)