[Made Any-resp and Any-cong more general.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20130727192306
 Ignore-this: a22306ba40191f95a2488893ac1913a1
] hunk ./src/Data/Colist.agda 25
-open import Function.Inverse using (_↔_; module Inverse)
+open import Function.Inverse as Inv using (_↔_; module Inverse)
hunk ./src/Data/Colist.agda 253
--- Any respects equality.
+-- Any respects pointwise implication (for the predicate) and equality
+-- (for the colist).
hunk ./src/Data/Colist.agda 256
-Any-resp : ∀ {a p} {A : Set a} {P : A → Set p} → Any P Respects _≈_
-Any-resp (x ∷ xs≈) (here px) = here px
-Any-resp (x ∷ xs≈) (there p) = there (Any-resp (♭ xs≈) p)
+Any-resp :
+  ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} {xs ys} →
+  (∀ {x} → P x → Q x) → xs ≈ ys → Any P xs → Any Q ys
+Any-resp f (x ∷ xs≈) (here px) = here (f px)
+Any-resp f (x ∷ xs≈) (there p) = there (Any-resp f (♭ xs≈) p)
hunk ./src/Data/Colist.agda 262
--- Any P maps equal colists to isomorphic types.
+-- Any maps pointwise isomorphic predicates and equal colists to
+-- isomorphic types.
hunk ./src/Data/Colist.agda 265
-Any-cong : ∀ {a p} {A : Set a} {P : A → Set p} →
-           _≈_ =[ Any P ]⇒ _↔_
-Any-cong {P = P} xs≈ys = record
-  { to         = P.→-to-⟶ (Any-resp xs≈ys)
-  ; from       = P.→-to-⟶ (Any-resp (sym xs≈ys))
+Any-cong :
+  ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} {xs ys} →
+  (∀ {x} → P x ↔ Q x) → xs ≈ ys → Any P xs ↔ Any Q ys
+Any-cong {A = A} P↔Q xs≈ys = record
+  { to         = P.→-to-⟶ (Any-resp (_⟨$⟩_ (Inverse.to   P↔Q)) xs≈ys)
+  ; from       = P.→-to-⟶ (Any-resp (_⟨$⟩_ (Inverse.from P↔Q)) (sym xs≈ys))
hunk ./src/Data/Colist.agda 272
-    { left-inverse-of  = resp∘resp xs≈ys (sym xs≈ys)
-    ; right-inverse-of = resp∘resp (sym xs≈ys) xs≈ys
+    { left-inverse-of  = resp∘resp          P↔Q       xs≈ys (sym xs≈ys)
+    ; right-inverse-of = resp∘resp (Inv.sym P↔Q) (sym xs≈ys)     xs≈ys
hunk ./src/Data/Colist.agda 279
-  resp∘resp : ∀ {xs ys}
+  resp∘resp : ∀ {p q} {P : A → Set p} {Q : A → Set q} {xs ys}
+              (P↔Q : ∀ {x} → P x ↔ Q x)
hunk ./src/Data/Colist.agda 282
-              Any-resp ys≈xs (Any-resp xs≈ys p) ≡ p
-  resp∘resp (x ∷ xs≈) (.x ∷ ys≈) (here px) = P.refl
-  resp∘resp (x ∷ xs≈) (.x ∷ ys≈) (there p) =
-    P.cong there (resp∘resp (♭ xs≈) (♭ ys≈) p)
+              Any-resp (_⟨$⟩_ (Inverse.from P↔Q)) ys≈xs
+                (Any-resp (_⟨$⟩_ (Inverse.to P↔Q)) xs≈ys p) ≡ p
+  resp∘resp P↔Q (x ∷ xs≈) (.x ∷ ys≈) (here px) =
+    P.cong here (Inverse.left-inverse-of P↔Q px)
+  resp∘resp P↔Q (x ∷ xs≈) (.x ∷ ys≈) (there p) =
+    P.cong there (resp∘resp P↔Q (♭ xs≈) (♭ ys≈) p)
hunk ./src/Data/Colist.agda 309
-  ∀ {a p} {A : Set a} {P : A → Set p} {xs ys}
+  ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q}
+    {f : ∀ {x} → P x → Q x} {xs ys}
hunk ./src/Data/Colist.agda 312
-  index (Any-resp xs≈ys p) ≡ index p
+  index (Any-resp f xs≈ys p) ≡ index p
hunk ./src/Data/Colist/Infinite-merge.agda 85
-    Any P ⟦ program xs ⋎ ys ⟧P                ↔⟨ Any-cong (⋎-homP (program xs)) ⟩
+    Any P ⟦ program xs ⋎ ys ⟧P                ↔⟨ Any-cong Inv.id (⋎-homP (program xs)) ⟩
hunk ./src/Data/Colist/Infinite-merge.agda 87
-    (Any P ⟦ program xs ⟧P ⊎ Any P ⟦ ys ⟧P)   ↔⟨ Any-cong (⟦program⟧P _) ⊎-cong (_ ∎) ⟩
+    (Any P ⟦ program xs ⟧P ⊎ Any P ⟦ ys ⟧P)   ↔⟨ Any-cong Inv.id (⟦program⟧P _) ⊎-cong (_ ∎) ⟩
hunk ./src/Data/Colist/Infinite-merge.agda 96
-    with       Any-resp (⋎-homW (whnf (program xs)) _) p
-       | index-Any-resp (⋎-homW (whnf (program xs)) _) p
+    with       Any-resp      id  (⋎-homW (whnf (program xs)) _) p
+       | index-Any-resp {f = id} (⋎-homW (whnf (program xs)) _) p
hunk ./src/Data/Colist/Infinite-merge.agda 103
-    with       Any-resp (⟦program⟧P xs) r
-       | index-Any-resp (⟦program⟧P xs) r
+    with       Any-resp      id  (⟦program⟧P xs) r
+       | index-Any-resp {f = id} (⟦program⟧P xs) r