pass get functions as records
[~helmut/bidiragda.git] / FreeTheorems.agda
1 module FreeTheorems where
2
3 open import Data.Nat using (ℕ)
4 open import Data.List using (List ; map)
5 open import Data.Vec using (Vec) renaming (map to mapV)
6 open import Function using (_∘_)
7 open import Relation.Binary.PropositionalEquality using (_≗_)
8
9 module ListList where
10   get-type : Set₁
11   get-type = {A : Set} → List A → List A
12
13   record Get : Set₁ where
14     field
15       get : {A : Set} → List A → List A
16       free-theorem : {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
17
18   postulate
19     free-theorem : (get : get-type) → {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
20
21   assume-get : get-type → Get
22   assume-get get = record { get = get; free-theorem = free-theorem get }
23
24 module VecVec where
25   get-type : (ℕ → ℕ) → Set₁
26   get-type getlen = {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
27
28   record Get : Set₁ where
29     field
30       getlen : ℕ → ℕ
31       get : {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
32       free-theorem : {α β : Set} (f : α → β) {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
33
34   postulate
35     free-theorem : {getlen : ℕ → ℕ} → (get : get-type getlen) → {α β : Set} → (f : α → β) → {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
36
37   assume-get : {getlen : ℕ → ℕ} → (get : get-type getlen) → Get
38   assume-get {getlen} get = record { getlen = getlen; get = get; free-theorem = free-theorem get }