diff options
Diffstat (limited to 'FreeTheorems.agda')
| -rw-r--r-- | FreeTheorems.agda | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/FreeTheorems.agda b/FreeTheorems.agda index 08bbe88..25759e0 100644 --- a/FreeTheorems.agda +++ b/FreeTheorems.agda @@ -5,9 +5,7 @@ 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 Function.Equality using (_⟶_ ; _⟨$⟩_) -open import Relation.Binary.PropositionalEquality using (_≗_ ; cong) renaming (setoid to EqSetoid) -open import Relation.Binary using (Setoid) +open import Relation.Binary.PropositionalEquality using (_≗_) import GetTypes @@ -36,13 +34,13 @@ module VecVec where 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 (gl₁ ⟨$⟩ i) → Vec A (gl₂ ⟨$⟩ i) + get-type : {I : Set} → (I → ℕ) → (I → ℕ) → Set₁ + get-type {I} gl₁ gl₂ = {A : Set} {i : I} → Vec A (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 + free-theorem : {I : Set} → (gl₁ : I → ℕ) → (gl₂ : I → ℕ) (get : get-type gl₁ gl₂) → {α β : Set} → (f : α → β) → {i : 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 : Set} → (gl₁ : I → ℕ) → (gl₂ : I → ℕ) (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 } |