Merge branch feature-get-record into feature-partial-getlen
[~helmut/bidiragda.git] / GetTypes.agda
1 module GetTypes 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 Function.Injection using (module Injection) renaming (Injection to _↪_ ; id to id↪)
10 open import Relation.Binary.PropositionalEquality using (_≗_) renaming (setoid to EqSetoid)
11 open import Relation.Binary using (Setoid)
12 open Injection using (to)
13
14 open import Generic using (≡-to-Π)
15
16 module ListList where
17   record Get : Set₁ where
18     field
19       get : {A : Set} → List A → List A
20       free-theorem : {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
21
22 module VecVec where
23   record Get : Set₁ where
24     field
25       getlen : ℕ → ℕ
26       get : {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
27       free-theorem : {α β : Set} (f : α → β) {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
28
29 module PartialVecVec where
30   record Get : Set₁ where
31     field
32       I : Setoid ℓ₀ ℓ₀
33       gl₁ : I ↪ EqSetoid ℕ
34       gl₂ : I ⟶ EqSetoid ℕ
35       get : {A : Set} {i : Setoid.Carrier I} → Vec A (to gl₁ ⟨$⟩ i) → Vec A (gl₂ ⟨$⟩ i)
36       free-theorem : {α β : Set} → (f : α → β) → {i : Setoid.Carrier I} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get
37
38 VecVec-to-PartialVecVec : VecVec.Get → PartialVecVec.Get
39 VecVec-to-PartialVecVec G = record
40   { I = EqSetoid ℕ
41   ; gl₁ = id↪
42   ; gl₂ = ≡-to-Π getlen
43   ; get = get
44   ; free-theorem = free-theorem
45   } where open VecVec.Get G