From b1b80567288030782231418407e7244b37227450 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
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.
---
 GetTypes.agda | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

(limited to 'GetTypes.agda')

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)
-- 
cgit v1.2.3