fix compilation against agda stdlib 0.9
[~helmut/bidiragda.git] / FreeTheorems.agda
1 module FreeTheorems where
2
3 open import Level using () renaming (zero to ℓ₀)
4 open import Data.Nat using (ℕ)
5 open import Data.List using (List ; map)
6 open import Data.Vec using (Vec) renaming (map to mapV)
7 open import Function using (_∘_)
8 open import Function.Equality using (_⟶_ ; _⟨$⟩_)
9 open import Relation.Binary.PropositionalEquality using (_≗_ ; cong) renaming (setoid to EqSetoid)
10 open import Relation.Binary using (Setoid)
11
12 import GetTypes
13
14 module ListList where
15   get-type : Set₁
16   get-type = {A : Set} → List A → List A
17
18   open GetTypes.ListList public
19
20   postulate
21     free-theorem : (get : get-type) → {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
22
23   assume-get : get-type → Get
24   assume-get get = record { get = get; free-theorem = free-theorem get }
25
26 module VecVec where
27   get-type : (ℕ → ℕ) → Set₁
28   get-type getlen = {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
29
30   open GetTypes.VecVec public
31
32   postulate
33     free-theorem : {getlen : ℕ → ℕ} → (get : get-type getlen) → {α β : Set} → (f : α → β) → {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
34
35   assume-get : {getlen : ℕ → ℕ} → (get : get-type getlen) → Get
36   assume-get {getlen} get = record { getlen = getlen; get = get; free-theorem = free-theorem get }
37
38 module PartialVecVec where
39   get-type : {I : Setoid ℓ₀ ℓ₀} → (I ⟶ EqSetoid ℕ) → (I ⟶ EqSetoid ℕ) → Set₁
40   get-type {I} gl₁ gl₂ = {A : Set} {i : Setoid.Carrier I} → Vec A (gl₁ ⟨$⟩ i) → Vec A (gl₂ ⟨$⟩ i)
41
42   open GetTypes.PartialVecVec public
43
44   postulate
45     free-theorem : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ⟶ EqSetoid ℕ) → (gl₂ : I ⟶ EqSetoid ℕ) (get : get-type gl₁ gl₂)  → {α β : Set} → (f : α → β) → {i : Setoid.Carrier I} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get
46
47   assume-get : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ⟶ EqSetoid ℕ) → (gl₂ : I ⟶ EqSetoid ℕ) (get : get-type gl₁ gl₂) → Get
48   assume-get {I} gl₁ gl₂ get = record { I = I; gl₁ = gl₁; gl₂ = gl₂; get = get; free-theorem = free-theorem gl₁ gl₂ get }