[Included the map id ≡ id law as well.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080306134847] hunk ./MultiComposition.agda 8
-         -- Assume extensionality; it is used in a proof below.
+         -- Assume extensionality; it is used in proofs below.
hunk ./MultiComposition.agda 24
-    Fun   : Set -> Set
-    map   : forall {a b} -> (a -> b) -> Fun a -> Fun b
+    Fun : Set -> Set
+    map : forall {a b} -> (a -> b) -> Fun a -> Fun b
hunk ./MultiComposition.agda 30
-    map-∘ : forall {a b c} (f : b -> c) (g : a -> b) ->
-            map (f ∘ g) ≡ map f ∘ map g
+    map-id : forall a -> map (id {a = a}) ≡ id
+    map-∘  : forall {a b c} (f : b -> c) (g : a -> b) ->
+             map (f ∘ g) ≡ map f ∘ map g
hunk ./MultiComposition.agda 38
-  { Fun   = \c -> c
-  ; map   = \f as -> f as
-  ; map-∘ = \f g -> ≡-refl
+  { Fun    = \c -> c
+  ; map    = \f as -> f as
+  ; map-id = \a -> ≡-refl
+  ; map-∘  = \f g -> ≡-refl
hunk ./MultiComposition.agda 48
-  { Fun   = \c -> a -> Fun bs c
-  ; map   = \f k x -> map bs f (k x)
-  ; map-∘ = \f g -> ≡-ext \k -> ≡-ext \x ->
+  { Fun    = \c -> a -> Fun bs c
+  ; map    = \f k x -> map bs f (k x)
+  ; map-id = \a -> ≡-ext \k -> ≡-ext \x ->
+      ≡-cong (\h -> h (k x)) (map-id bs a)
+  ; map-∘  = \f g -> ≡-ext \k -> ≡-ext \x ->
hunk ./MultiComposition.agda 60
-  { Fun   = \c -> Fun as (Fun bs c)
-  ; map   = \f k -> map as (map bs f) k
-  ; map-∘ = \f g -> begin
+  { Fun    = \c -> Fun as (Fun bs c)
+  ; map    = \f k -> map as (map bs f) k
+  ; map-id = \a -> begin
+      map as (map bs id)
+        ≡⟨ ≡-cong (map as) (map-id bs a) ⟩
+      map as id
+        ≡⟨ map-id as (Fun bs a) ⟩
+      id
+        ∎
+  ; map-∘  = \f g -> begin