comparison agda/laws.agda @ 131:d205ff1e406f InfiniteDeltaWithMonad

Cleanup proofs
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 03 Feb 2015 12:57:13 +0900
parents 5902b2a24abf
children 575de2e38385
comparison
equal deleted inserted replaced
130:ac45d065cbf2 131:d205ff1e406f
1 open import Relation.Binary.PropositionalEquality 1 open import Relation.Binary.PropositionalEquality
2 open import Level 2 open import Level
3
3 open import basic 4 open import basic
4 5
5 module laws where 6 module laws where
6 7
7 record Functor {l : Level} (F : Set l -> Set l) : Set (suc l) where 8 record Functor {l : Level} (F : Set l -> Set l) : Set (suc l) where