diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-10-14 09:52:00 +0200 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-10-14 09:52:00 +0200 |
| commit | b1b80567288030782231418407e7244b37227450 (patch) | |
| tree | 59f8235071780a89505166349b7bc2f7af03d9e5 /GetTypes.agda | |
| parent | f9fc1aba9386216a6a01ba17d85fcae71756d928 (diff) | |
| download | bidiragda-b1b80567288030782231418407e7244b37227450.tar.gz | |
drop the injection requirement for gl₁
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.
Diffstat (limited to 'GetTypes.agda')
| -rw-r--r-- | GetTypes.agda | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/GetTypes.agda b/GetTypes.agda index f23d154..033257a 100644 --- a/GetTypes.agda +++ b/GetTypes.agda @@ -4,12 +4,10 @@ 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 Function using (_∘_ ; id) open import Function.Equality using (_⟶_ ; _⟨$⟩_) -open import Function.Injection using (module Injection) renaming (Injection to _↪_ ; id to id↪) open import Relation.Binary.PropositionalEquality using (_≗_) renaming (setoid to EqSetoid) open import Relation.Binary using (Setoid) -open Injection using (to) open import Generic using (≡-to-Π) open import Structures using (Shaped ; module Shaped) @@ -32,11 +30,11 @@ module PartialVecVec where record Get : Set₁ where field I : Setoid ℓ₀ ℓ₀ - gl₁ : I ↪ EqSetoid ℕ + gl₁ : I ⟶ EqSetoid ℕ gl₂ : I ⟶ EqSetoid ℕ |I| = Setoid.Carrier I - |gl₁| = _⟨$⟩_ (to gl₁) + |gl₁| = _⟨$⟩_ gl₁ |gl₂| = _⟨$⟩_ gl₂ field @@ -46,7 +44,7 @@ module PartialVecVec where VecVec-to-PartialVecVec : VecVec.Get → PartialVecVec.Get VecVec-to-PartialVecVec G = record { I = EqSetoid ℕ - ; gl₁ = id↪ + ; gl₁ = ≡-to-Π id ; gl₂ = ≡-to-Π getlen ; get = get ; free-theorem = free-theorem @@ -64,11 +62,11 @@ module PartialShapeShape where ViewShapeT : Shaped ViewShape ViewContainer I : Setoid ℓ₀ ℓ₀ - gl₁ : I ↪ EqSetoid SourceShape + gl₁ : I ⟶ EqSetoid SourceShape gl₂ : I ⟶ EqSetoid ViewShape |I| = Setoid.Carrier I - |gl₁| = _⟨$⟩_ (to gl₁) + |gl₁| = _⟨$⟩_ gl₁ |gl₂| = _⟨$⟩_ gl₂ open Shaped SourceShapeT using () renaming (fmap to fmapS) |