From 7ba21759412a8b356f7790ac5f5e413302331183 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Fri, 5 Oct 2012 12:47:09 +0200 Subject: move all postulates to one module This should make it easier to see what is assumed. --- FreeTheorems.agda | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 FreeTheorems.agda (limited to 'FreeTheorems.agda') diff --git a/FreeTheorems.agda b/FreeTheorems.agda new file mode 100644 index 0000000..f37cada --- /dev/null +++ b/FreeTheorems.agda @@ -0,0 +1,21 @@ +module FreeTheorems where + +open import Data.Nat using (ℕ) +open import Data.List using (List ; map) +open import Data.Vec using (Vec) renaming (map to mapV) +open import Function using (_∘_) +open import Relation.Binary.PropositionalEquality using (_≗_) + +module ListList where + get-type : Set₁ + get-type = {A : Set} → List A → List A + + postulate + free-theorem : (get : get-type) → {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get + +module VecVec where + get-type : (ℕ → ℕ) → Set₁ + get-type getlen = {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n) + + postulate + free-theorem : {getlen : ℕ → ℕ} → (get : get-type getlen) → {α β : Set} → (f : α → β) → {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get -- cgit v1.2.3