zanzix

namespace OpKind
  data Kind : Type where 
    Set : Kind -- Set
    Op : Kind -> Kind -- Set^op
  
  data Ty : Kind -> Type where 
    NAT : Ty k 
    Zero : Ty k
    Add : Ty k -> Ty k -> Ty k 
    One : Ty k

zanzix

import Data.Relevant.Cover as Rel
import Data.Linear.Cover as Lin

import Data.Vect

Ctx : Type
Ctx = List String

export infixr 5 ~>
data Ty : (typeVars : Ctx) -> Type where

zanzix

module Ty

public export
data Kind : Type where
  Set : Kind
  Op : Kind

public export
data Dual : Kind -> Kind -> Type where
  L : Dual Set Op