-- basic training

    level-ex.agda
    list-level.agda
    list.agda
    record-ex.agda
    negnat.agda

    system-f.agda
    system-t.agda

-- Category Utilities 

    HomReasoning.agda             -- extensions for reasoning
    cat-utility.agda              -- basic category constructs

-- Category Theorems

    idF.agda
    category-ex.agda
    list-monoid-cat.agda
    list-nat.agda
    list-nat0.agda
    maybe-monad.agda
    maybeCat.agda
    monoid-monad.agda

    yoneda.agda

-- Monad and adjunction

    kleisli.agda
    em-category.agda
    adj-monad.agda
    comparison-em.agda
    comparison-functor.agda

-- Limit 

    equalizer.agda
    universal-mapping.agda
    free-monoid.agda
    CatExponetial.agda
    pullback.agda
    discrete.agda
    limit-to.agda

-- no yet finished

    freyd.agda
    Comma.agda
    linton.agda

-- repositories

   https://bitbucket.org/shinji_kono/category-exercise-in-agda/src