From dbad09a8a5843e91f862657c3011ec7f63ea819b Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Tue, 9 Jun 2015 16:09:37 +0200
Subject: drop the Function.Equality requirement from GetTypes
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

We never used the equality property. Thus a simple function is
sufficient here. We always fulfilled the property using ≡-to-Π anyway.
---
 GetTypes.agda | 35 ++++++++++++++++-------------------
 1 file changed, 16 insertions(+), 19 deletions(-)

(limited to 'GetTypes.agda')

diff --git a/GetTypes.agda b/GetTypes.agda
index 033257a..286b9aa 100644
--- a/GetTypes.agda
+++ b/GetTypes.agda
@@ -5,11 +5,8 @@ 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 (_∘_ ; id)
-open import Function.Equality using (_⟶_ ; _⟨$⟩_)
-open import Relation.Binary.PropositionalEquality using (_≗_) renaming (setoid to EqSetoid)
-open import Relation.Binary using (Setoid)
+open import Relation.Binary.PropositionalEquality using (_≗_)
 
-open import Generic using (≡-to-Π)
 open import Structures using (Shaped ; module Shaped)
 open import Instances using (VecShaped)
 
@@ -29,13 +26,13 @@ module VecVec where
 module PartialVecVec where
   record Get : Set₁ where
     field
-      I : Setoid ℓ₀ ℓ₀
-      gl₁ : I ⟶ EqSetoid ℕ
-      gl₂ : I ⟶ EqSetoid ℕ
+      I : Set
+      gl₁ : I → ℕ
+      gl₂ : I → ℕ
 
-    |I|   = Setoid.Carrier I
-    |gl₁| = _⟨$⟩_ gl₁
-    |gl₂| = _⟨$⟩_ gl₂
+    |I|   = I
+    |gl₁| = gl₁
+    |gl₂| = gl₂
 
     field
       get : {A : Set} {i : |I|} → Vec A (|gl₁| i) → Vec A (|gl₂| i)
@@ -43,9 +40,9 @@ module PartialVecVec where
 
 VecVec-to-PartialVecVec : VecVec.Get → PartialVecVec.Get
 VecVec-to-PartialVecVec G = record
-  { I = EqSetoid ℕ
-  ; gl₁ = ≡-to-Π id
-  ; gl₂ = ≡-to-Π getlen
+  { I = ℕ
+  ; gl₁ = id
+  ; gl₂ = getlen
   ; get = get
   ; free-theorem = free-theorem
   } where open VecVec.Get G
@@ -61,13 +58,13 @@ module PartialShapeShape where
       ViewContainer : Set → ViewShape → Set
       ViewShapeT : Shaped ViewShape ViewContainer
 
-      I : Setoid ℓ₀ ℓ₀
-      gl₁ : I ⟶ EqSetoid SourceShape
-      gl₂ : I ⟶ EqSetoid ViewShape
+      I : Set
+      gl₁ : I → SourceShape
+      gl₂ : I → ViewShape
 
-    |I|   = Setoid.Carrier I
-    |gl₁| = _⟨$⟩_ gl₁
-    |gl₂| = _⟨$⟩_ gl₂
+    |I|   = I
+    |gl₁| = gl₁
+    |gl₂| = gl₂
 
     open Shaped SourceShapeT using () renaming (fmap to fmapS)
     open Shaped ViewShapeT using () renaming (fmap to fmapV)
-- 
cgit v1.2.3