-- 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
    maybeCat.agda
    monoid-monad.agda

    yoneda.agda

-- Monad and adjunction

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

-- Limit 

    equalizer.agda
    universal-mapping.agda
    free-monoid.agda
    CatExponetial.agda
    pullback.agda                -- including limit from product and equalizer
    discrete.agda
    limit-to.agda
    SetsCompleteness.agda

-- Freyd Adjoint Functor Theorem

    Comma.agda
    Comma1.agda
    freyd.agda
    freyd1.agda
    freyd2.agda

-- Monoidal functor and Applicative

    monoidal.agda                 -- Monoidal category and Functor
    applicative.agda              -- Applicative functor is a monoidal functor
    monad→monoidal.agda

-- Cartesian Closed Category

    deductive.agda                -- deduction theorem
    CCC.agda
    CCChom.agda
    CCCGraph.agda                 -- CCC generated from graph

-- no yet finished

-- repositories

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