From 20ff2bd915d116223e1ea9eda60647c60de98725 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Thu, 3 Apr 2014 08:45:19 +0200
Subject: drop PartialShapeVec

One can use PartialShapeShape instead, so there is limited utility for
this type. It is not used directly and there also is no PartialVecShape.
---
 GetTypes.agda | 41 ++++-------------------------------------
 1 file changed, 4 insertions(+), 37 deletions(-)

(limited to 'GetTypes.agda')

diff --git a/GetTypes.agda b/GetTypes.agda
index 2812e2b..f23d154 100644
--- a/GetTypes.agda
+++ b/GetTypes.agda
@@ -52,39 +52,6 @@ VecVec-to-PartialVecVec G = record
   ; free-theorem = free-theorem
   } where open VecVec.Get G
 
-module PartialShapeVec where
-  record Get : Set₁ where
-    field
-      Shape : Set
-      Container : Set → Shape → Set
-      ShapeT : Shaped Shape Container
-
-      I : Setoid ℓ₀ ℓ₀
-      gl₁ : I ↪ EqSetoid Shape
-      gl₂ : I ⟶ EqSetoid ℕ
-
-    |I|   = Setoid.Carrier I
-    |gl₁| = _⟨$⟩_ (to gl₁)
-    |gl₂| = _⟨$⟩_ gl₂
-
-    open Shaped ShapeT using (fmap)
-
-    field
-      get : {A : Set} {i : |I|} → Container A (|gl₁| i) → Vec A (|gl₂| i)
-      free-theorem : {α β : Set} → (f : α → β) → {i : |I|} → get {_} {i} ∘ fmap f ≗ mapV f ∘ get
-
-    open Shaped ShapeT public
-
-PartialVecVec-to-PartialShapeVec : PartialVecVec.Get → PartialShapeVec.Get
-PartialVecVec-to-PartialShapeVec G = record
-  { ShapeT       = VecShaped
-  ; I            = I
-  ; gl₁          = gl₁
-  ; gl₂          = gl₂
-  ; get          = get
-  ; free-theorem = free-theorem
-  } where open PartialVecVec.Get G
-
 module PartialShapeShape where
   record Get : Set₁ where
     field
@@ -114,13 +81,13 @@ module PartialShapeShape where
     open Shaped SourceShapeT public using () renaming (fmap to fmapS)
     open Shaped ViewShapeT public using () renaming (fmap to fmapV)
 
-PartialShapeVec-to-PartialShapeShape : PartialShapeVec.Get → PartialShapeShape.Get
-PartialShapeVec-to-PartialShapeShape G = record
-  { SourceShapeT = ShapeT
+PartialVecVec-to-PartialShapeShape : PartialVecVec.Get → PartialShapeShape.Get
+PartialVecVec-to-PartialShapeShape G = record
+  { SourceShapeT = VecShaped
   ; ViewShapeT   = VecShaped
   ; I            = I
   ; gl₁          = gl₁
   ; gl₂          = gl₂
   ; get          = get
   ; free-theorem = free-theorem
-  } where open PartialShapeVec.Get G
+  } where open PartialVecVec.Get G
-- 
cgit v1.2.3