switch examples to PartialVecVec
[~helmut/bidiragda.git] / FreeTheorems.agda
index 2695491..d4eb174 100644 (file)
@@ -1,10 +1,15 @@
 module FreeTheorems where
 
+open import Level using () renaming (zero to ℓ₀)
 open import Data.Nat using (ℕ)
 open import Data.List using (List ; map)
 open import Data.Vec using (Vec) renaming (map to mapV)
 open import Function using (_∘_)
-open import Relation.Binary.PropositionalEquality using (_≗_)
+open import Function.Equality using (_⟶_ ; _⟨$⟩_)
+open import Function.Injection using (module Injection) renaming (Injection to _↪_)
+open import Relation.Binary.PropositionalEquality using (_≗_ ; cong) renaming (setoid to EqSetoid)
+open import Relation.Binary using (Setoid)
+open Injection using (to)
 
 import GetTypes
 
@@ -31,3 +36,15 @@ module VecVec where
 
   assume-get : {getlen : ℕ → ℕ} → (get : get-type getlen) → Get
   assume-get {getlen} get = record { getlen = getlen; get = get; free-theorem = free-theorem get }
+
+module PartialVecVec where
+  get-type : {I : Setoid ℓ₀ ℓ₀} → (I ↪ (EqSetoid ℕ)) → (I ⟶ (EqSetoid ℕ)) → Set₁
+  get-type {I} gl₁ gl₂ = {A : Set} {i : Setoid.Carrier I} → Vec A (to gl₁ ⟨$⟩ i) → Vec A (gl₂ ⟨$⟩ i)
+
+  open GetTypes.PartialVecVec public
+
+  postulate
+    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
+
+  assume-get : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ (EqSetoid ℕ)) → (gl₂ : I ⟶ (EqSetoid ℕ)) (get : get-type gl₁ gl₂) → Get
+  assume-get {I} gl₁ gl₂ get = record { I = I; gl₁ = gl₁; gl₂ = gl₂; get = get; free-theorem = free-theorem gl₁ gl₂ get }