Mercurial > hg > Members > atton > delta_monad
log agda/delta/functor.agda @ 93:8d92ed54a94f
age | author | description |
---|---|---|
Mon, 19 Jan 2015 15:21:29 +0900 | Yasutaka Higa | Prove functor-laws for deltaM |
Mon, 19 Jan 2015 12:11:38 +0900 | Yasutaka Higa | Unify levels on data type. only use suc to proofs |
Mon, 19 Jan 2015 11:48:41 +0900 | Yasutaka Higa | Defining DeltaM in Agda... |
Mon, 19 Jan 2015 11:00:34 +0900 | Yasutaka Higa | Split functor-proofs into delta.functor |