Category : (Type -> Type -> Type) -> Type
Category (~>) = {
    id : forall a . a ~> a,
    compose : forall a b c . (b ~> c) -> (a ~> b) -> (a ~> c),
}

fnCategory : Category (->)
fnCategory = {
    id = \x -> x,
    compose = \f g x -> f (g x),
}

LamLang repr (~>) = Category (~>) -> {
    lam : forall a b . (repr a ~> repr b) -> repr (a ~> b),
    app : forall a b . repr (a ~> b) -> repr a -> repr b,
}

RecLang repr (~>) = Category (~>) -> {
    fix : forall a . (repr a ~> repr a) -> repr a,
}

ArithLang repr = {
    int : Int -> repr Int,
    add : repr Int -> repr Int -> repr Int,
    mul : repr Int -> repr Int -> repr Int,
}

test : forall repr . ArithLang repr -> LamLang repr (->) -> Category (->) -> repr
test a l c =
    let lc = l c
        add1 = lc.lam (\x -> a.add (a.int 1) x)
        square = lc.lam (\x -> a.mul x x)
    in
        lc.app square (lc.app add1 (a.int 1))