From c63ff4179147ab237afe7d21d9e3740737c9b942 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Thu, 30 Jan 2014 09:02:06 +0100
Subject: pass get functions as records

This allows passing both getlen and get as a single parameter. It also
allows to make the free theorem a prerequisite instead of a postulate.
---
 FreeTheorems.agda | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'FreeTheorems.agda')

diff --git a/FreeTheorems.agda b/FreeTheorems.agda
index f37cada..d2ba3ef 100644
--- a/FreeTheorems.agda
+++ b/FreeTheorems.agda
@@ -10,12 +10,29 @@ 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
+
   postulate
     free-theorem : (get : get-type) → {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
 
+  assume-get : get-type → Get
+  assume-get get = record { get = get; free-theorem = free-theorem get }
+
 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
+
   postulate
     free-theorem : {getlen : ℕ → ℕ} → (get : get-type getlen) → {α β : Set} → (f : α → β) → {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
+
+  assume-get : {getlen : ℕ → ℕ} → (get : get-type getlen) → Get
+  assume-get {getlen} get = record { getlen = getlen; get = get; free-theorem = free-theorem get }
-- 
cgit v1.2.3