From 19670abeff9895de593ef26ad2da247ae590ce90 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 30 Jan 2014 09:13:11 +0100 Subject: allow importing of Bidir without any postulates --- GetTypes.agda | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 GetTypes.agda (limited to 'GetTypes.agda') diff --git a/GetTypes.agda b/GetTypes.agda new file mode 100644 index 0000000..99675f9 --- /dev/null +++ b/GetTypes.agda @@ -0,0 +1,20 @@ +module GetTypes 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 + record Get : Set₁ where + field + get : {A : Set} → List A → List A + free-theorem : {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get + +module VecVec where + record Get : Set₁ where + field + getlen : ℕ → ℕ + get : {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n) + free-theorem : {α β : Set} (f : α → β) {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get -- cgit v1.2.3