@@ -6,13 +6,26 @@ public export record Identity (a : Type) where
66 constructor Id
77 runIdentity : a
88
9−implementation Functor Identity where
9+Functor Identity where
1010 map fn (Id a) = Id (fn a)
1111
12−implementation Applicative Identity where
12+Applicative Identity where
1313 pure x = Id x
14−
1514 (Id f) <*> (Id g) = Id (f g)
1615
17−implementation Monad Identity where
16+Monad Identity where
1817 (Id x) >>= k = k x
18+
19+Show a => Show (Identity a) where
20+ showPrec d (Id x) = showCon d "Id" $ showArg x
21+
22+Eq a => Eq (Identity a) where
23+ (Id x) == (Id y) = x == y
24+
25+Ord a => Ord (Identity a) where
26+ compare (Id x) (Id y) = compare x y
27+
28+Enum a => Enum (Identity a) where
29+ toNat (Id x) = toNat x
30+ fromNat n = Id $ fromNat n
31+ pred (Id n) = Id $ pred n