From c62e107155b8fea28dbf1637f9187e4f24f75173 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Tue, 31 Jan 2012 18:26:32 +0100
Subject: postulate free theorem for List a -> List a

---
 Bidir.agda | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Bidir.agda b/Bidir.agda
index 6bb6608..81f00dd 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -103,5 +103,8 @@ bff get eq s v = let s′ = idrange (length s)
                      h′ = fmap (flip union g) h
                  in fmap (flip map s′ ∘ flip lookup) h′
 
+postulate
+  free-theorem-list-list : {β γ : Set} → (get : {α : Set} → List α → List α) → (f : β → γ) → (l : List β) → get (map f l) ≡ map f (get l)
+
 theorem-1 : (get : {α : Set} → List α → List α) → {τ : Set} → (eq : EqInst τ) → (s : List τ) → bff get eq s (get s) ≡ just s
 theorem-1 get eq s = {!!}
-- 
cgit v1.2.3