diff options
Diffstat (limited to 'FreeTheorems.agda')
| -rw-r--r-- | FreeTheorems.agda | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/FreeTheorems.agda b/FreeTheorems.agda index 2695491..d4eb174 100644 --- a/FreeTheorems.agda +++ b/FreeTheorems.agda @@ -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 } |