From b1b80567288030782231418407e7244b37227450 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Tue, 14 Oct 2014 09:52:00 +0200 Subject: drop the injection requirement for gl₁ MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Turns out, we never use this requirement. The only place where it may come in relevant is the free theorems. But here non-injectivity turns out to be reasoning about multiple get functions that are selected by the additional index each individually satisfying the free theorem and thus commonly satisfying it as well. --- FreeTheorems.agda | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) (limited to 'FreeTheorems.agda') diff --git a/FreeTheorems.agda b/FreeTheorems.agda index d4eb174..08bbe88 100644 --- a/FreeTheorems.agda +++ b/FreeTheorems.agda @@ -6,10 +6,8 @@ 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 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 @@ -38,13 +36,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 (to gl₁ ⟨$⟩ i) → Vec A (gl₂ ⟨$⟩ i) + 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) 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 : 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 : 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 } -- cgit v1.2.3