From 19670abeff9895de593ef26ad2da247ae590ce90 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Thu, 30 Jan 2014 09:13:11 +0100
Subject: allow importing of Bidir without any postulates

---
 FreeTheorems.agda | 13 ++++---------
 1 file changed, 4 insertions(+), 9 deletions(-)

(limited to 'FreeTheorems.agda')

diff --git a/FreeTheorems.agda b/FreeTheorems.agda
index d2ba3ef..2695491 100644
--- a/FreeTheorems.agda
+++ b/FreeTheorems.agda
@@ -6,14 +6,13 @@ open import Data.Vec using (Vec) renaming (map to mapV)
 open import Function using (_∘_)
 open import Relation.Binary.PropositionalEquality using (_≗_)
 
+import GetTypes
+
 module ListList where
   get-type : Set₁
   get-type = {A : Set} → List A → List A
 
-  record Get : Set₁ where
-    field
-      get : {A : Set} → List A → List A
-      free-theorem : {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
+  open GetTypes.ListList public
 
   postulate
     free-theorem : (get : get-type) → {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
@@ -25,11 +24,7 @@ module VecVec where
   get-type : (ℕ → ℕ) → Set₁
   get-type getlen = {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
 
-  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
+  open GetTypes.VecVec public
 
   postulate
     free-theorem : {getlen : ℕ → ℕ} → (get : get-type getlen) → {α β : Set} → (f : α → β) → {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
-- 
cgit v1.2.3