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.

diff --git a/BFF.agda b/BFF.agda
index 12524ca..26d1d5e 100644 (file)
--- a/BFF.agda
+++ b/BFF.agda
@@ -18,7 +18,7 @@ open import Generic using (sequenceV ; ≡-to-Π)
 open import Structures using (Shaped ; module Shaped)
 open import Instances using (VecShaped)
 import CheckInsert
-open import GetTypes using (VecVec-to-PartialVecVec ; PartialVecVec-to-PartialShapeVec ; PartialShapeVec-to-PartialShapeShape)
+open import GetTypes using (VecVec-to-PartialVecVec ; PartialVecVec-to-PartialShapeShape)
 
 module PartialShapeBFF (A : DecSetoid ℓ₀ ℓ₀) where
   open GetTypes.PartialShapeShape public using (Get ; module Get)
@@ -67,10 +67,10 @@ module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where
   denumerate = PartialShapeBFF.denumerate A VecShaped
 
   bff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Vec (Maybe Carrier) (Get.|gl₁| G j))
-  bff G j s v = PartialShapeBFF.bff A (PartialShapeVec-to-PartialShapeShape (PartialVecVec-to-PartialShapeVec G)) j s v
+  bff G j s v = PartialShapeBFF.bff A (PartialVecVec-to-PartialShapeShape G) j s v
 
   sbff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Vec Carrier (Get.|gl₁| G j))
-  sbff  G j s v = PartialShapeBFF.sbff A (PartialShapeVec-to-PartialShapeShape (PartialVecVec-to-PartialShapeVec G)) j s v
+  sbff  G j s v = PartialShapeBFF.sbff A (PartialVecVec-to-PartialShapeShape G) j s v
 
 module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where
   open GetTypes.VecVec public using (Get)

diff --git a/GetTypes.agda b/GetTypes.agda
index 2812e2b..f23d154 100644 (file)
--- 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