Type.Base

{-# OPTIONS --safe --without-K #-}
module Type.Base where

infixr 7 _⇒_

data Ty : Set where
  ι   : Ty
  _⇒_ : (a : Ty) → (b : Ty) → Ty
  □_  : (a : Ty) → Ty

variable
  a b c d : Ty

Generated from commit 2fd14c996b195ef101dff8919e837907ca0a08aa.