Kind.agda

module Kind (Gnd : Set)(U : Set)(T : U -> Set) where

open import Basics
open import Pr
open import Nom

data Kind : Set where
  Ty    : Gnd -> Kind
  _|>_  : Kind -> Kind -> Kind
  Pi    : (u : U) -> (T u -> Kind) -> Kind

infixr 60 _|>_