From 3616445f9a60402701ca00a22e9e6e2fbe95c741 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Fri, 7 Mar 2014 15:18:24 +0100
Subject: add a Functor structure

The intent is to replace some uses of Vec with a structure that also
happens to be a functor. RawFunctors from the standard library provide
no laws though, so we define a Functor structure that adds the laws. As
an additional law congruence is added, because

 * Other standard library structures in Algebra.Structures also require
   congruence.
 * Otherwise the identity law would have to reason about different
   identities.
---
 Everything.agda |  1 +
 Structures.agda | 31 +++++++++++++++++++++++++++++++
 2 files changed, 32 insertions(+)
 create mode 100644 Structures.agda

diff --git a/Everything.agda b/Everything.agda
index e37c76e..7383dd5 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -2,6 +2,7 @@
 module Everything where
 
 import Generic
+import Structures
 import FinMap
 import CheckInsert
 import GetTypes
diff --git a/Structures.agda b/Structures.agda
new file mode 100644
index 0000000..f1fd85b
--- /dev/null
+++ b/Structures.agda
@@ -0,0 +1,31 @@
+module Structures where
+
+open import Category.Functor using (RawFunctor ; module RawFunctor)
+open import Function using (_∘_ ; id)
+open import Function.Equality using (_⟶_ ; _⇨_ ; _⟨$⟩_)
+open import Relation.Binary using (_Preserves_⟶_)
+open import Relation.Binary.PropositionalEquality as P using (_≗_ ; _≡_ ; refl)
+
+record IsFunctor (F : Set → Set) (f : {α β : Set} → (α →  β) → F α → F β) : Set₁ where
+  field
+    cong : {α β : Set} → f {α} {β} Preserves _≗_ ⟶ _≗_
+    identity : {α : Set} → f {α} id ≗ id
+    composition : {α β γ : Set} → (g : β → γ) → (h : α → β) →
+                  f (g ∘ h) ≗ f g ∘ f h
+
+  isCongruence : {α β : Set} → (P.setoid α ⇨ P.setoid β) ⟶ P.setoid (F α) ⇨ P.setoid (F β)
+  isCongruence {α} {β} = record
+    { _⟨$⟩_ = λ g → record
+      { _⟨$⟩_ = f (_⟨$⟩_ g)
+      ; cong = P.cong (f (_⟨$⟩_ g))
+      }
+    ; cong = λ {g} {h} g≗h {x} x≡y → P.subst (λ z → f (_⟨$⟩_ g) x ≡ f (_⟨$⟩_ h) z) x≡y (cong (λ _ → g≗h refl) x)
+    }
+
+record Functor (f : Set → Set) : Set₁ where
+  field
+    rawfunctor : RawFunctor f
+    isFunctor : IsFunctor f (RawFunctor._<$>_ rawfunctor)
+
+  open RawFunctor rawfunctor public
+  open IsFunctor isFunctor public
-- 
cgit v1.2.3


From dab051e89bbe904587a047d239e79610554d5c91 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Mon, 10 Mar 2014 08:17:41 +0100
Subject: implement a bff on a shaped source type

Add IsShaped and Shaped records describing shapely types as in Jay95.
Implement bff on Shaped and rewrite PartialVecVec to use the vector
shape retaining all proofs on the vector implementation.
---
 BFF.agda        | 53 +++++++++++++++++++++++++++++++++++---------------
 Everything.agda |  1 +
 GetTypes.agda   | 35 +++++++++++++++++++++++++++++++++
 Instances.agda  | 18 +++++++++++++++++
 Structures.agda | 60 +++++++++++++++++++++++++++++++++++++++++++++++++++++++--
 5 files changed, 150 insertions(+), 17 deletions(-)
 create mode 100644 Instances.agda

diff --git a/BFF.agda b/BFF.agda
index 2ce24db..b78e2af 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -15,11 +15,13 @@ open import Relation.Binary using (Setoid ; DecSetoid ; module DecSetoid)
 
 open import FinMap
 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)
+open import GetTypes using (VecVec-to-PartialVecVec ; PartialVecVec-to-PartialShapeVec)
 
-module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where
-  open GetTypes.PartialVecVec public using (Get)
+module PartialShapeBFF (A : DecSetoid ℓ₀ ℓ₀) where
+  open GetTypes.PartialShapeVec public using (Get ; module Get)
   open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq)
   open CheckInsert A
 
@@ -27,27 +29,48 @@ module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where
   assoc []V       []V       = just empty
   assoc (i ∷V is) (b ∷V bs) = (assoc is bs) >>= (checkInsert i b)
 
+  enumerate : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → (s : S) → C (Fin (Shaped.arity ShapeT s)) s
+  enumerate ShapeT s = fill s (allFin (arity s))
+    where open Shaped ShapeT
+
+  denumerate : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → {α : Set} {s : S} → (c : C α s) → Fin (Shaped.arity ShapeT s) → α
+  denumerate ShapeT c = flip lookupV (Shaped.content ShapeT c)
+
+  bff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Get.Container G Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Get.Container G (Maybe Carrier) (Get.|gl₁| G j))
+  bff G {i} j s v = let s′ = enumerate ShapeT (|gl₁| i)
+                        t′ = get s′
+                        g  = fromFunc (denumerate ShapeT s)
+                        g′ = delete-many t′ g
+                        t  = enumerate ShapeT (|gl₁| j)
+                        h  = assoc (get t) v
+                        h′ = (flip union (reshape g′ (arity (|gl₁| j)))) <$> h
+                    in ((λ f → fmap f t) ∘ flip lookupM) <$> h′
+    where open Get G
+
+  sbff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Get.Container G Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Get.Container G Carrier (Get.|gl₁| G j))
+  sbff G j s v = bff G j s v >>= Get.sequence G
+
+module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where
+  open GetTypes.PartialVecVec public using (Get)
+  open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq)
+  open CheckInsert A
+
+  open PartialShapeBFF A public using (assoc)
+
   enumerate : {n : ℕ} → Vec Carrier n → Vec (Fin n) n
-  enumerate {n} _ = allFin n
+  enumerate {n} _ = PartialShapeBFF.enumerate A VecShaped n
 
   enumeratel : (n : ℕ) → Vec (Fin n) n
-  enumeratel = allFin
+  enumeratel = PartialShapeBFF.enumerate A VecShaped
 
   denumerate : {n : ℕ} → Vec Carrier n → Fin n → Carrier
-  denumerate = flip lookupV
+  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 i s v = let s′ = enumerate s
-                    t′ = Get.get G s′
-                    g  = fromFunc (denumerate s)
-                    g′ = delete-many t′ g
-                    t  = enumeratel (Get.|gl₁| G i)
-                    h  = assoc (Get.get G t) v
-                    h′ = (flip union (reshape g′ (Get.|gl₁| G i))) <$> h
-                in (flip mapV t ∘ flip lookupM) <$> h′
+  bff G j s v = PartialShapeBFF.bff A (PartialVecVec-to-PartialShapeVec 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 = bff G j s v >>= sequenceV
+  sbff  G j s v = PartialShapeBFF.sbff A (PartialVecVec-to-PartialShapeVec G) j s v
 
 module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where
   open GetTypes.VecVec public using (Get)
diff --git a/Everything.agda b/Everything.agda
index 7383dd5..5ca5550 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -3,6 +3,7 @@ module Everything where
 
 import Generic
 import Structures
+import Instances
 import FinMap
 import CheckInsert
 import GetTypes
diff --git a/GetTypes.agda b/GetTypes.agda
index eb72cea..0db3f31 100644
--- a/GetTypes.agda
+++ b/GetTypes.agda
@@ -12,6 +12,8 @@ open import Relation.Binary using (Setoid)
 open Injection using (to)
 
 open import Generic using (≡-to-Π)
+open import Structures using (Shaped ; module Shaped)
+open import Instances using (VecShaped)
 
 module ListList where
   record Get : Set₁ where
@@ -49,3 +51,36 @@ VecVec-to-PartialVecVec G = record
   ; get = get
   ; 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
diff --git a/Instances.agda b/Instances.agda
new file mode 100644
index 0000000..faff6f8
--- /dev/null
+++ b/Instances.agda
@@ -0,0 +1,18 @@
+module Instances where
+
+open import Data.Nat using (ℕ)
+open import Data.Vec using (Vec)
+open import Function using (id)
+open import Relation.Binary.PropositionalEquality using (refl)
+
+open import Structures using (Shaped)
+
+VecShaped : Shaped ℕ Vec
+VecShaped = record
+  { arity = id
+  ; content = id
+  ; fill = λ _ → id
+  ; isShaped = record
+    { content-fill = λ _ → refl
+    ; fill-content = λ _ _ → refl
+    } }
diff --git a/Structures.agda b/Structures.agda
index f1fd85b..10abd42 100644
--- a/Structures.agda
+++ b/Structures.agda
@@ -1,10 +1,17 @@
 module Structures where
 
 open import Category.Functor using (RawFunctor ; module RawFunctor)
-open import Function using (_∘_ ; id)
+open import Category.Monad using (module RawMonad)
+open import Data.Maybe using (Maybe) renaming (monad to MaybeMonad)
+open import Data.Nat using (ℕ)
+open import Data.Vec as V using (Vec)
+import Data.Vec.Properties as VP
+open import Function using (_∘_ ; flip ; id)
 open import Function.Equality using (_⟶_ ; _⇨_ ; _⟨$⟩_)
 open import Relation.Binary using (_Preserves_⟶_)
-open import Relation.Binary.PropositionalEquality as P using (_≗_ ; _≡_ ; refl)
+open import Relation.Binary.PropositionalEquality as P using (_≗_ ; _≡_ ; refl ; module ≡-Reasoning)
+
+open import Generic using (sequenceV)
 
 record IsFunctor (F : Set → Set) (f : {α β : Set} → (α →  β) → F α → F β) : Set₁ where
   field
@@ -29,3 +36,52 @@ record Functor (f : Set → Set) : Set₁ where
 
   open RawFunctor rawfunctor public
   open IsFunctor isFunctor public
+
+record IsShaped (S : Set)
+                (C : Set → S → Set)
+                (arity : S → ℕ)
+                (content : {α : Set} {s : S} → C α s → Vec α (arity s))
+                (fill : {α : Set} → (s : S) → Vec α (arity s) → C α s)
+                : Set₁ where
+  field
+    content-fill : {α : Set} {s : S} → (c : C α s) → fill s (content c) ≡ c
+    fill-content : {α : Set} → (s : S) → (v : Vec α (arity s)) → content (fill s v) ≡ v
+
+  fmap : {α β : Set} → (f : α → β) → {s : S} → C α s → C β s
+  fmap f {s} c = fill s (V.map f (content c))
+
+  isFunctor : (s : S) → IsFunctor (flip C s) (λ f → fmap f)
+  isFunctor s = record
+    { cong = λ g≗h c → P.cong (fill s) (VP.map-cong g≗h (content c))
+    ; identity = λ c → begin
+        fill s (V.map id (content c))
+          ≡⟨ P.cong (fill s) (VP.map-id (content c)) ⟩
+        fill s (content c)
+          ≡⟨ content-fill c ⟩
+        c ∎
+    ; composition = λ g h c → P.cong (fill s) (begin
+        V.map (g ∘ h) (content c)
+          ≡⟨ VP.map-∘ g h (content c) ⟩
+        V.map g (V.map h (content c))
+          ≡⟨ P.cong (V.map g) (P.sym (fill-content s (V.map h (content c)))) ⟩
+        V.map g (content (fill s (V.map h (content c)))) ∎)
+    } where open ≡-Reasoning
+
+  fmap-content : {α β : Set} → (f : α → β) → {s : S} → content {β} {s} ∘ fmap f ≗ V.map f ∘ content
+  fmap-content f c = fill-content _ (V.map f (content c))
+  fill-fmap : {α β : Set} → (f : α → β) → (s : S) → fmap f ∘ fill s ≗ fill s ∘ V.map f
+  fill-fmap f s v = P.cong (fill s ∘ V.map f) (fill-content s v)
+
+  sequence : {α : Set} {s : S} → C (Maybe α) s → Maybe (C α s)
+  sequence {s = s} c = fill s <$> sequenceV (content c)
+    where open RawMonad MaybeMonad
+
+record Shaped (S : Set) (C : Set → S → Set) : Set₁ where
+  field
+    arity : S → ℕ
+    content : {α : Set} {s : S} → C α s → Vec α (arity s)
+    fill : {α : Set} → (s : S) → Vec α (arity s) → C α s
+
+    isShaped : IsShaped S C arity content fill
+
+  open IsShaped isShaped public
-- 
cgit v1.2.3


From 3532b34beabbaa6967fe660385c4b4036493a8f1 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Mon, 10 Mar 2014 09:31:57 +0100
Subject: port theorem-{1,2} to PartialShapeVec

---
 Bidir.agda     | 147 +++++++++++++++++++++++++++++++++++++++------------------
 Instances.agda |  30 ++++++++++--
 2 files changed, 127 insertions(+), 50 deletions(-)

diff --git a/Bidir.agda b/Bidir.agda
index ae99c5a..1a661de 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -13,7 +13,7 @@ open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_)
 open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_)
 open import Data.List using (List)
 open import Data.List.All using (All)
-open import Data.Vec using (Vec ; [] ; _∷_ ; toList ; map) renaming (lookup to lookupVec)
+open import Data.Vec using (Vec ; [] ; _∷_ ; toList ; map ; allFin) renaming (lookup to lookupVec)
 open import Data.Vec.Equality using () renaming (module Equality to VecEq)
 open import Data.Vec.Properties using (lookup∘tabulate ; map-cong ; map-∘ ; map-lookup-allFin)
 open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂)
@@ -24,14 +24,16 @@ open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ;
 open import Relation.Binary using (Setoid ; module Setoid ; module DecSetoid)
 import Relation.Binary.EqReasoning as EqR
 
+open import Structures using (Functor ; IsFunctor ; Shaped ; module Shaped)
+open import Instances using (MaybeFunctor)
 import GetTypes
-open GetTypes.PartialVecVec using (Get ; module Get)
+open GetTypes.PartialShapeVec using (Get ; module Get)
 open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; VecISetoid ; just-injective)
 open import FinMap
 import CheckInsert
 open CheckInsert A
 import BFF
-open BFF.PartialVecBFF A using (assoc ; enumerate ; enumeratel ; denumerate ; bff)
+open BFF.PartialShapeBFF A using (assoc ; enumerate ; denumerate ; bff)
 open Setoid using () renaming (_≈_ to _∋_≈_)
 open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq)
 
@@ -107,11 +109,24 @@ lemma-2 (i ∷ is) (x ∷ xs) h p | just h' | [ ir ] = begin
   just x ∷ map just xs ∎
   where open EqR (VecISetoid (MaybeSetoid A.setoid) at _)
 
-theorem-1 : (G : Get) → {i : Get.|I| G} → (s : Vec Carrier (Get.|gl₁| G i)) → bff G i s (Get.get G s) ≡ just (map just s)
+lemma-fmap-denumerate-enumerate : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → {α : Set} {s : S} → (c : C α s) → Shaped.fmap ShapeT (denumerate ShapeT c) (enumerate ShapeT s) ≡ c
+lemma-fmap-denumerate-enumerate {S} {C} ShapeT {s = s} c = begin
+  fmap (denumerate ShapeT c) (fill s (allFin (arity s)))
+    ≡⟨ fill-fmap (denumerate ShapeT c) s (allFin (arity s)) ⟩
+  fill s (map (flip lookupVec (content c)) (allFin (arity s)))
+    ≡⟨ cong (fill s) (map-lookup-allFin (content c)) ⟩
+  fill s (content c)
+    ≡⟨ content-fill c ⟩
+  c ∎
+  where open ≡-Reasoning
+        open Shaped ShapeT
+
+
+theorem-1 : (G : Get) → {i : Get.|I| G} → (s : Get.Container G Carrier (Get.|gl₁| G i)) → bff G i s (Get.get G s) ≡ just (Get.fmap G just s)
 theorem-1 G {i} s = begin
   bff G i s (get s)
-    ≡⟨ cong (bff G i s ∘ get) (sym (map-lookup-allFin s)) ⟩
-  bff G i s (get (map f t))
+    ≡⟨ cong (bff G i s ∘ get) (sym (lemma-fmap-denumerate-enumerate ShapeT s)) ⟩
+  bff G i s (get (fmap f t))
     ≡⟨ cong (bff G i s) (free-theorem f t) ⟩
   bff G i s (map f (get t))
     ≡⟨ refl ⟩
@@ -119,26 +134,26 @@ theorem-1 G {i} s = begin
     ≡⟨ cong (_<$>_ h′↦r ∘ _<$>_ h↦h′) (lemma-1 f (get t)) ⟩
   (Maybe.just ∘ h′↦r ∘ h↦h′) (restrict f (toList (get t)))
     ≡⟨ cong just (begin
-      h′↦r (union (restrict f (toList (get t))) (reshape g′ (|gl₁| i)))
+      h′↦r (union (restrict f (toList (get t))) (reshape g′ (arity (|gl₁| i))))
         ≡⟨ cong (h′↦r ∘ union (restrict f (toList (get t)))) (lemma-reshape-id g′) ⟩
       h′↦r (union (restrict f (toList (get t))) g′)
         ≡⟨ cong h′↦r (lemma-disjoint-union f (get t)) ⟩
       h′↦r (fromFunc f)
         ≡⟨ refl ⟩
-      map (flip lookupM (fromFunc f)) t
-        ≡⟨ map-cong (lemma-lookupM-fromFunc f) t ⟩
-      map (Maybe.just ∘ f) t
-        ≡⟨ map-∘ just f t ⟩
-      map just (map f t)
-        ≡⟨ cong (map just) (map-lookup-allFin s) ⟩
-      map just s ∎) ⟩ _ ∎
+      fmap (flip lookupM (fromFunc f)) t
+        ≡⟨ IsFunctor.cong (isFunctor (|gl₁| i)) (lemma-lookupM-fromFunc f) t ⟩
+      fmap (Maybe.just ∘ f) t
+        ≡⟨ IsFunctor.composition (isFunctor (|gl₁| i)) just f t ⟩
+      fmap just (fmap f t)
+        ≡⟨ cong (fmap just) (lemma-fmap-denumerate-enumerate ShapeT s) ⟩
+      fmap just s ∎) ⟩ _ ∎
     where open ≡-Reasoning
           open Get G
-          t    = enumeratel (|gl₁| i)
-          f    = denumerate s
+          t    = enumerate ShapeT (|gl₁| i)
+          f    = denumerate ShapeT s
           g′   = delete-many (get t) (fromFunc f)
-          h↦h′ = flip union (reshape g′ (|gl₁| i))
-          h′↦r = flip map t ∘ flip lookupM
+          h↦h′ = flip union (reshape g′ (arity (|gl₁| i)))
+          h′↦r = (λ f′ → fmap f′ t) ∘ flip lookupM
 
 
 lemma-<$>-just : {A B : Set} {f : A → B} {b : B} (ma : Maybe A) → f <$> ma ≡ just b → ∃ λ a → ma ≡ just a
@@ -162,9 +177,21 @@ lemma->>=-just : {A B : Set} (ma : Maybe A) {f : A → Maybe B} {b : B} → (ma
 lemma->>=-just (just a) p = a , refl
 lemma->>=-just nothing  ()
 
-lemma-just-sequence : {A : Set} {n : ℕ} → (v : Vec A n) → sequenceV (map just v) ≡ just v
-lemma-just-sequence []       = refl
-lemma-just-sequence (x ∷ xs) = cong (_<$>_ (_∷_ x)) (lemma-just-sequence xs)
+lemma-just-sequenceV : {A : Set} {n : ℕ} → (v : Vec A n) → sequenceV (map just v) ≡ just v
+lemma-just-sequenceV []       = refl
+lemma-just-sequenceV (x ∷ xs) = cong (_<$>_ (_∷_ x)) (lemma-just-sequenceV xs)
+
+lemma-just-sequence : (G : Get) → {A : Set} {i : Get.|I| G} → (c : Get.Container G A (Get.|gl₁| G i)) → Get.sequence G (Get.fmap G just c) ≡ just c
+lemma-just-sequence G {i = i} c = begin
+  fill (|gl₁| i) <$> sequenceV (content (fmap just c))
+    ≡⟨ cong (_<$>_ (fill (|gl₁| i)) ∘ sequenceV) (fmap-content just c) ⟩
+  fill (|gl₁| i) <$> sequenceV (map just (content c))
+    ≡⟨ cong (_<$>_ (fill (|gl₁| i))) (lemma-just-sequenceV (content c)) ⟩
+  fill (|gl₁| i) <$> just (content c)
+    ≡⟨ cong just (content-fill c) ⟩
+  just c ∎
+  where open ≡-Reasoning
+        open Get G
 
 lemma-sequenceV-successful : {A : Set} {n : ℕ} → (v : Vec (Maybe A) n) → {r : Vec A n} → sequenceV v ≡ just r → v ≡ map just r
 lemma-sequenceV-successful []             {r = []}       p = refl
@@ -173,18 +200,44 @@ lemma-sequenceV-successful (just x ∷ xs)                 () | nothing | _
 lemma-sequenceV-successful (just x ∷ xs)  {r = .x ∷ .ys} refl  | just ys | [ p′ ] = cong (_∷_ (just x)) (lemma-sequenceV-successful xs p′)
 lemma-sequenceV-successful (nothing ∷ xs)                ()
 
-lemma-get-sequenceV : {A : Set} → (G : Get) → {i : Get.|I| G} {v : Vec (Maybe A) (Get.|gl₁| G i)} {r : Vec A (Get.|gl₁| G i)} → sequenceV v ≡ just r → Get.get G <$> sequenceV v ≡ sequenceV (Get.get G v)
-lemma-get-sequenceV G {v = v} {r = r} p = begin
-  get <$> sequenceV v
-    ≡⟨ cong (_<$>_ get ∘ sequenceV) (lemma-sequenceV-successful v p) ⟩
-  get <$> sequenceV (map just r)
-    ≡⟨ cong (_<$>_ get) (lemma-just-sequence r) ⟩
+lemma-sequence-successful : (G : Get) → {A : Set} {i : Get.|I| G} → (c : Get.Container G (Maybe A) (Get.|gl₁| G i)) → {r : Get.Container G A (Get.|gl₁| G i)} → Get.sequence G c ≡ just r → c ≡ Get.fmap G just r
+lemma-sequence-successful G {i = i} c {r} p = just-injective (sym (begin
+  fill (|gl₁| i) <$> (map just <$> (content <$> just r))
+    ≡⟨ cong (_<$>_ (fill (|gl₁| i)) ∘ _<$>_ (map just)) (begin
+      content <$> just r
+        ≡⟨ cong (_<$>_ content) (sym p) ⟩
+      content <$> (fill (|gl₁| i) <$> sequenceV (content c))
+        ≡⟨ sym (Functor.composition MaybeFunctor content (fill (|gl₁| i)) (sequenceV (content c))) ⟩
+      content ∘ fill (|gl₁| i) <$> sequenceV (content c)
+        ≡⟨ Functor.cong MaybeFunctor (fill-content (|gl₁| i)) (sequenceV (content c)) ⟩
+      id <$> sequenceV (content c)
+        ≡⟨ Functor.identity MaybeFunctor (sequenceV (content c)) ⟩
+      sequenceV (content c)
+        ≡⟨ cong sequenceV (lemma-sequenceV-successful (content c) (proj₂ wp)) ⟩
+      sequenceV (map just (proj₁ wp))
+        ≡⟨ lemma-just-sequenceV (proj₁ wp) ⟩
+      just (proj₁ (lemma-<$>-just (sequenceV (content c)) p)) ∎) ⟩
+  fill (|gl₁| i) <$> (map just <$> just (proj₁ (lemma-<$>-just (sequenceV (content c)) p)))
+    ≡⟨ cong (_<$>_ (fill (|gl₁| i)) ∘ just) (sym (lemma-sequenceV-successful (content c) (proj₂ wp))) ⟩
+  fill (|gl₁| i) <$> just (content c)
+    ≡⟨ cong just (content-fill c) ⟩
+  just c ∎))
+  where open ≡-Reasoning
+        open Get G
+        wp = lemma-<$>-just (sequenceV (content c)) p
+
+lemma-get-sequence : {A : Set} → (G : Get) → {i : Get.|I| G} {v : Get.Container G (Maybe A) (Get.|gl₁| G i)} {r : Get.Container G A (Get.|gl₁| G i)} → Get.sequence G v ≡ just r → Get.get G <$> Get.sequence G v ≡ sequenceV (Get.get G v)
+lemma-get-sequence G {v = v} {r = r} p = begin
+  get <$> sequence v
+    ≡⟨ cong (_<$>_ get ∘ sequence) (lemma-sequence-successful G v p) ⟩
+  get <$> sequence (fmap just r)
+    ≡⟨ cong (_<$>_ get) (lemma-just-sequence G r) ⟩
   get <$> just r
-    ≡⟨ sym (lemma-just-sequence (get r)) ⟩
+    ≡⟨ sym (lemma-just-sequenceV (get r)) ⟩
   sequenceV (map just (get r))
     ≡⟨ cong sequenceV (sym (free-theorem just r)) ⟩
-  sequenceV (get (map just r))
-    ≡⟨ cong (sequenceV ∘ get) (sym (lemma-sequenceV-successful v p)) ⟩
+  sequenceV (get (fmap just r))
+    ≡⟨ cong (sequenceV ∘ get) (sym (lemma-sequence-successful G v p)) ⟩
   sequenceV (get v) ∎
   where open ≡-Reasoning
         open Get G
@@ -198,16 +251,16 @@ sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong
 sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (VecISetoid S at _))
 sequence-cong {S}                                       (VecEq._∷-cong_ nothing xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S at _))
 
-theorem-2 : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Vec (Maybe Carrier) (Get.|gl₁| G j)) → bff G j s v ≡ just u → VecISetoid (MaybeSetoid A.setoid) at _ ∋ Get.get G u ≈ map just v
-theorem-2 G j s v u p with (lemma-<$>-just ((flip union (reshape (delete-many (Get.get G (enumerate s)) (fromFunc (denumerate s))) (Get.|gl₁| G j))) <$> (assoc (Get.get G (enumeratel (Get.|gl₁| G j))) v)) p)
-theorem-2 G j s v u p | h′ , ph′ with (lemma-<$>-just (assoc (Get.get G (enumeratel (Get.|gl₁| G j))) v) ph′)
-theorem-2 G j s v u p | h′ , ph′ | h , ph = begin⟨ VecISetoid (MaybeSetoid A.setoid) at _ ⟩
+theorem-2 : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Get.Container G Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Get.Container G (Maybe Carrier) (Get.|gl₁| G j)) → bff G j s v ≡ just u → VecISetoid (MaybeSetoid A.setoid) at _ ∋ Get.get G u ≈ map just v
+theorem-2 G {i} j s v u p with (lemma-<$>-just ((flip union (reshape (delete-many (Get.get G (enumerate (Get.ShapeT G) (Get.|gl₁| G i))) (fromFunc (denumerate (Get.ShapeT G) s))) (Get.arity G (Get.|gl₁| G j)))) <$> (assoc (Get.get G (enumerate (Get.ShapeT G) (Get.|gl₁| G j))) v)) p)
+theorem-2 G {i} j s v u p | h′ , ph′ with (lemma-<$>-just (assoc (Get.get G (enumerate (Get.ShapeT G) (Get.|gl₁| G j))) v) ph′)
+theorem-2 G {i} j s v u p | h′ , ph′ | h , ph = begin⟨ VecISetoid (MaybeSetoid A.setoid) at _ ⟩
   get u
     ≡⟨ just-injective (trans (cong (_<$>_ get) (sym p))
                              (cong (_<$>_ get ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph)) ⟩
   get (h′↦r (h↦h′ h))
     ≡⟨ refl ⟩
-  get (map (flip lookupM (h↦h′ h)) t)
+  get (fmap (flip lookupM (h↦h′ h)) t)
     ≡⟨ free-theorem (flip lookupM (h↦h′ h)) t ⟩
   map (flip lookupM (h↦h′ h)) (get t)
     ≡⟨ lemma-union-not-used h g′ (get t) (lemma-assoc-domain (get t) v h ph) ⟩
@@ -216,23 +269,23 @@ theorem-2 G j s v u p | h′ , ph′ | h , ph = begin⟨ VecISetoid (MaybeSetoid
   map just v ∎
     where open SetoidReasoning
           open Get G
-          s′   = enumerate s
-          g    = fromFunc (denumerate s)
+          s′   = enumerate ShapeT (|gl₁| i)
+          g    = fromFunc (denumerate ShapeT s)
           g′   = delete-many (get s′) g
-          t    = enumeratel (Get.|gl₁| G j)
-          h↦h′ = flip union (reshape g′ (Get.|gl₁| G j))
-          h′↦r = flip map t ∘ flip lookupM
+          t    = enumerate ShapeT (|gl₁| j)
+          h↦h′ = flip union (reshape g′ (arity (|gl₁| j)))
+          h′↦r = (λ f → fmap f t) ∘ flip lookupM
 
-theorem-2′ : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Vec Carrier (Get.|gl₁| G j)) → bff G j s v ≡ just (map just u) → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v
+theorem-2′ : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Get.Container G Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Get.Container G Carrier (Get.|gl₁| G j)) → bff G j s v ≡ just (Get.fmap G just u) → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v
 theorem-2′ G j s v u p = drop-just (begin
   get <$> just u
-    ≡⟨ cong (_<$>_ get) (sym (lemma-just-sequence u)) ⟩
-  get <$> sequenceV (map just u)
-    ≡⟨ lemma-get-sequenceV G (lemma-just-sequence u) ⟩
-  sequenceV (get (map just u))
-    ≈⟨ sequence-cong (theorem-2 G j s v (map just u) p) ⟩
+    ≡⟨ cong (_<$>_ get) (sym (lemma-just-sequence G u)) ⟩
+  get <$> sequence (fmap just u)
+    ≡⟨ lemma-get-sequence G (lemma-just-sequence G u) ⟩
+  sequenceV (get (fmap just u))
+    ≈⟨ sequence-cong (theorem-2 G j s v (fmap just u) p) ⟩
   sequenceV (map just v)
-    ≡⟨ lemma-just-sequence v ⟩
+    ≡⟨ lemma-just-sequenceV v ⟩
   just v ∎)
   where open EqR (MaybeSetoid (VecISetoid A.setoid at _))
         open Get G
diff --git a/Instances.agda b/Instances.agda
index faff6f8..b41b0a2 100644
--- a/Instances.agda
+++ b/Instances.agda
@@ -1,11 +1,35 @@
 module Instances where
 
+open import Category.Functor using (RawFunctor)
+open import Data.Maybe as M using (Maybe)
 open import Data.Nat using (ℕ)
 open import Data.Vec using (Vec)
-open import Function using (id)
-open import Relation.Binary.PropositionalEquality using (refl)
+open import Function using (_∘_ ; id)
+open import Relation.Binary.PropositionalEquality as P using (_≗_ ; refl)
 
-open import Structures using (Shaped)
+open import Structures using (Functor ; Shaped)
+
+MaybeFunctor : Functor Maybe
+MaybeFunctor = record
+  { rawfunctor = M.functor
+  ; isFunctor = record
+    { cong = cong
+    ; identity = identity
+    ; composition = composition
+    } }
+  where _<$>_ = RawFunctor._<$>_ M.functor
+
+        cong : {α β : Set} {g h : α → β} → g ≗ h → _<$>_ g ≗ _<$>_ h
+        cong g≗h (M.just x) = P.cong M.just (g≗h x)
+        cong g≗h M.nothing  = refl
+
+        identity : {α : Set} → _<$>_ {α} id ≗ id
+        identity (M.just x) = refl
+        identity M.nothing  = refl
+
+        composition : {α β γ : Set} → (g : β → γ) → (h : α → β) → _<$>_ (g ∘ h) ≗ _<$>_ g ∘ _<$>_ h
+        composition g h (M.just x) = refl
+        composition g h M.nothing = refl
 
 VecShaped : Shaped ℕ Vec
 VecShaped = record
-- 
cgit v1.2.3


From 2472958f099a2535cf4fba93e68b91ea164a0295 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Mon, 10 Mar 2014 09:39:16 +0100
Subject: port precondition to PartialShapeVec

---
 Precond.agda | 39 ++++++++++++++++++++-------------------
 1 file changed, 20 insertions(+), 19 deletions(-)

diff --git a/Precond.agda b/Precond.agda
index a76fddc..bc54cd5 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -25,6 +25,7 @@ open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ;
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 open import Relation.Nullary using (yes ; no)
 
+open import Structures using (IsFunctor)
 open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty ; delete-many ; lemma-tabulate-∘ ; delete ; lemma-lookupM-delete ; lemma-lookupM-fromFunc ; reshape ; lemma-reshape-id)
 import CheckInsert
 open CheckInsert (decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other)
@@ -32,8 +33,8 @@ import BFF
 import Bidir
 open Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain)
 import GetTypes
-open GetTypes.PartialVecVec using (Get ; module Get)
-open BFF.PartialVecBFF (decSetoid deq) using (assoc ; enumerate ; denumerate ; bff ; enumeratel)
+open GetTypes.PartialShapeVec using (Get ; module Get)
+open BFF.PartialShapeBFF (decSetoid deq) using (assoc ; enumerate ; denumerate ; bff)
 
 lemma-maybe-just : {A : Set} → (a : A) → (ma : Maybe A) → maybe′ Maybe.just (just a) ma ≡ Maybe.just (maybe′ id a ma)
 lemma-maybe-just a (just x) = refl
@@ -62,31 +63,31 @@ lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (Data.List.A
           maybe′ just (lookupM i (delete-many is (fromFunc g))) (lookup i h) ∎
         inner f | no f≢i = cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (fromFunc g)) f≢i)
 
-assoc-enough : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → ∃ (λ h → assoc (Get.get G (enumeratel (Get.|gl₁| G j))) v ≡ just h) → ∃ λ u → bff G j s v ≡ just u
-assoc-enough G {i} j s v (h , p) = _ , cong (_<$>_ (flip map t ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (|gl₁| j)))) p
+assoc-enough : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Get.Container G Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → ∃ (λ h → assoc (Get.get G (enumerate (Get.ShapeT G) (Get.|gl₁| G j))) v ≡ just h) → ∃ λ u → bff G j s v ≡ just u
+assoc-enough G {i} j s v (h , p) = _ , cong (_<$>_ ((λ f → fmap f t) ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (arity (|gl₁| j))))) p
   where open Get G
-        g′ = delete-many (get (enumerate s)) (fromFunc (denumerate s))
-        t  = enumeratel (|gl₁| j)
+        g′ = delete-many (get (enumerate ShapeT (|gl₁| i))) (fromFunc (denumerate ShapeT s))
+        t  = enumerate ShapeT (|gl₁| j)
 
-assoc-enough′ : (G : Get) → {i : Get.|I| G} → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G i)) → ∃ (λ h → assoc (Get.get G (enumeratel (Get.|gl₁| G i))) v ≡ just h) → ∃ λ u → bff G i s v ≡ just (map just u)
+assoc-enough′ : (G : Get) → {i : Get.|I| G} → (s : Get.Container G Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G i)) → ∃ (λ h → assoc (Get.get G (enumerate (Get.ShapeT G) (Get.|gl₁| G i))) v ≡ just h) → ∃ λ u → bff G i s v ≡ just (Get.fmap G just u)
 assoc-enough′ G {i} s v (h , p) = _ , (begin
   bff G i s v
     ≡⟨ proj₂ (assoc-enough G i s v (h , p)) ⟩
-  just (map (flip lookupM (union h (reshape g′ (|gl₁| i)))) t)
+  just (fmap (flip lookupM (union h (reshape g′ (arity (|gl₁| i))))) t)
     ≡⟨ cong just (begin _
-        ≡⟨ cong (flip map t ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩
-      map (flip lookupM (union h g′)) t
-        ≡⟨ cong (flip map t ∘ flip lookupM) (proj₂ wp) ⟩
-      map (flip lookupM (fromFunc (proj₁ wp))) t
-        ≡⟨ map-cong (lemma-lookupM-fromFunc (proj₁ wp)) t ⟩
-      map (Maybe.just ∘ proj₁ wp) t
-        ≡⟨ map-∘ just (proj₁ wp) t ⟩
-      map Maybe.just (map (proj₁ wp) t) ∎) ⟩ _ ∎)
+        ≡⟨ cong ((λ f → fmap f t) ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩
+      fmap (flip lookupM (union h g′)) t
+        ≡⟨ cong ((λ f → fmap f t) ∘ flip lookupM) (proj₂ wp) ⟩
+      fmap (flip lookupM (fromFunc (proj₁ wp))) t
+        ≡⟨ IsFunctor.cong (isFunctor (|gl₁| i)) (lemma-lookupM-fromFunc (proj₁ wp)) t ⟩
+      fmap (Maybe.just ∘ proj₁ wp) t
+        ≡⟨ IsFunctor.composition (isFunctor (|gl₁| i)) just (proj₁ wp) t ⟩
+      fmap Maybe.just (fmap (proj₁ wp) t) ∎) ⟩ _ ∎)
   where open Get G
-        s′ = enumerate s
-        g  = fromFunc (denumerate s)
+        s′ = enumerate ShapeT (|gl₁| i)
+        g  = fromFunc (denumerate ShapeT s)
         g′ = delete-many (get s′) g
-        t  = enumeratel (Get.|gl₁| G i)
+        t  = enumerate ShapeT (|gl₁| i)
         wp = lemma-union-delete-fromFunc (lemma-assoc-domain (get t) v h p)
 
 data All-different {A : Set} : List A → Set where
-- 
cgit v1.2.3


From c3467438fa8b9ca068fd08b599861cb6be8aa931 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Mon, 10 Mar 2014 13:32:11 +0100
Subject: Example: show that PairVec is Shaped
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Example inspired in VoigtlaenderHMW13. Note that Vec (α × β) (length s)
is not Shaped in this way since its real index is only a number.
---
 Examples.agda | 33 ++++++++++++++++++++++++++++++++-
 1 file changed, 32 insertions(+), 1 deletion(-)

diff --git a/Examples.agda b/Examples.agda
index c82bcf4..eca3c90 100644
--- a/Examples.agda
+++ b/Examples.agda
@@ -5,12 +5,14 @@ open import Data.Nat.Properties using (cancel-+-left)
 import Algebra.Structures
 open Algebra.Structures.IsCommutativeSemiring Data.Nat.Properties.isCommutativeSemiring using (+-isCommutativeMonoid)
 open Algebra.Structures.IsCommutativeMonoid +-isCommutativeMonoid using () renaming (comm to +-comm)
+open import Data.List using (List ; length) renaming ([] to []L ; _∷_ to _∷L_)
 open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_ ; tail ; take ; drop)
 open import Function using (id)
 open import Function.Injection using () renaming (Injection to _↪_ ; id to id↪)
-open import Relation.Binary.PropositionalEquality using (_≡_ ; refl) renaming (setoid to EqSetoid)
+open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong) renaming (setoid to EqSetoid)
 
 open import Generic using (≡-to-Π)
+open import Structures using (Shaped)
 import GetTypes
 import FreeTheorems
 
@@ -71,3 +73,32 @@ intersperse' : Get
 intersperse' = assume-get suc-injection (≡-to-Π intersperse-len) f
   where f : {A : Set} {n : ℕ} → Vec A (suc n) → Vec A (intersperse-len n)
         f (s ∷ v)        = intersperse s v
+
+data PairVec (α : Set) (β : Set) : List α → Set where
+  []P : PairVec α β []L
+  _,_∷P_ : (x : α) → β → {l : List α} → PairVec α β l → PairVec α β (x ∷L l)
+
+PairVecFirstShaped : (α : Set) → Shaped (List α) (PairVec α)
+PairVecFirstShaped α = record
+  { arity = length
+  ; content = content
+  ; fill = fill
+  ; isShaped = record
+    { content-fill = content-fill
+    ; fill-content = fill-content
+    } }
+  where content : {β : Set} {s : List α} → PairVec α β s → Vec β (length s)
+        content []P          = []
+        content (a , b ∷P p) = b ∷ content p
+
+        fill : {β : Set} → (s : List α) → Vec β (length s) → PairVec α β s
+        fill []L      v       = []P
+        fill (a ∷L s) (b ∷ v) = a , b ∷P fill s v
+
+        content-fill : {β : Set} {s : List α} → (p : PairVec α β s) → fill s (content p) ≡ p
+        content-fill []P          = refl
+        content-fill (a , b ∷P p) = cong (_,_∷P_ a b) (content-fill p)
+
+        fill-content : {β : Set} → (s : List α) → (v : Vec β (length s)) → content (fill s v) ≡ v
+        fill-content []L      []      = refl
+        fill-content (a ∷L s) (b ∷ v) = cong (_∷_ b) (fill-content s v)
-- 
cgit v1.2.3


From b0b22d17dd4a6037defd57aa20223e1c5781eb66 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Mon, 10 Mar 2014 16:00:57 +0100
Subject: generalize lemma-{just-sequence,sequence-successful}

---
 Bidir.agda | 50 +++++++++++++++++++++++++-------------------------
 1 file changed, 25 insertions(+), 25 deletions(-)

diff --git a/Bidir.agda b/Bidir.agda
index 1a661de..9637f17 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -181,17 +181,17 @@ lemma-just-sequenceV : {A : Set} {n : ℕ} → (v : Vec A n) → sequenceV (map
 lemma-just-sequenceV []       = refl
 lemma-just-sequenceV (x ∷ xs) = cong (_<$>_ (_∷_ x)) (lemma-just-sequenceV xs)
 
-lemma-just-sequence : (G : Get) → {A : Set} {i : Get.|I| G} → (c : Get.Container G A (Get.|gl₁| G i)) → Get.sequence G (Get.fmap G just c) ≡ just c
-lemma-just-sequence G {i = i} c = begin
-  fill (|gl₁| i) <$> sequenceV (content (fmap just c))
-    ≡⟨ cong (_<$>_ (fill (|gl₁| i)) ∘ sequenceV) (fmap-content just c) ⟩
-  fill (|gl₁| i) <$> sequenceV (map just (content c))
-    ≡⟨ cong (_<$>_ (fill (|gl₁| i))) (lemma-just-sequenceV (content c)) ⟩
-  fill (|gl₁| i) <$> just (content c)
+lemma-just-sequence : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → {A : Set} {s : S} → (c : C A s) → Shaped.sequence ShapeT (Shaped.fmap ShapeT just c) ≡ just c
+lemma-just-sequence ShapeT {s = s} c = begin
+  fill s <$> sequenceV (content (fmap just c))
+    ≡⟨ cong (_<$>_ (fill s) ∘ sequenceV) (fmap-content just c) ⟩
+  fill s <$> sequenceV (map just (content c))
+    ≡⟨ cong (_<$>_ (fill s)) (lemma-just-sequenceV (content c)) ⟩
+  fill s <$> just (content c)
     ≡⟨ cong just (content-fill c) ⟩
   just c ∎
   where open ≡-Reasoning
-        open Get G
+        open Shaped ShapeT
 
 lemma-sequenceV-successful : {A : Set} {n : ℕ} → (v : Vec (Maybe A) n) → {r : Vec A n} → sequenceV v ≡ just r → v ≡ map just r
 lemma-sequenceV-successful []             {r = []}       p = refl
@@ -200,16 +200,16 @@ lemma-sequenceV-successful (just x ∷ xs)                 () | nothing | _
 lemma-sequenceV-successful (just x ∷ xs)  {r = .x ∷ .ys} refl  | just ys | [ p′ ] = cong (_∷_ (just x)) (lemma-sequenceV-successful xs p′)
 lemma-sequenceV-successful (nothing ∷ xs)                ()
 
-lemma-sequence-successful : (G : Get) → {A : Set} {i : Get.|I| G} → (c : Get.Container G (Maybe A) (Get.|gl₁| G i)) → {r : Get.Container G A (Get.|gl₁| G i)} → Get.sequence G c ≡ just r → c ≡ Get.fmap G just r
-lemma-sequence-successful G {i = i} c {r} p = just-injective (sym (begin
-  fill (|gl₁| i) <$> (map just <$> (content <$> just r))
-    ≡⟨ cong (_<$>_ (fill (|gl₁| i)) ∘ _<$>_ (map just)) (begin
+lemma-sequence-successful : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → {A : Set} {s : S} → (c : C (Maybe A) s) → {r : C A s} → Shaped.sequence ShapeT c ≡ just r → c ≡ Shaped.fmap ShapeT just r
+lemma-sequence-successful ShapeT {s = s} c {r} p = just-injective (sym (begin
+  fill s <$> (map just <$> (content <$> just r))
+    ≡⟨ cong (_<$>_ (fill s) ∘ _<$>_ (map just)) (begin
       content <$> just r
         ≡⟨ cong (_<$>_ content) (sym p) ⟩
-      content <$> (fill (|gl₁| i) <$> sequenceV (content c))
-        ≡⟨ sym (Functor.composition MaybeFunctor content (fill (|gl₁| i)) (sequenceV (content c))) ⟩
-      content ∘ fill (|gl₁| i) <$> sequenceV (content c)
-        ≡⟨ Functor.cong MaybeFunctor (fill-content (|gl₁| i)) (sequenceV (content c)) ⟩
+      content <$> (fill s <$> sequenceV (content c))
+        ≡⟨ sym (Functor.composition MaybeFunctor content (fill s) (sequenceV (content c))) ⟩
+      content ∘ fill s <$> sequenceV (content c)
+        ≡⟨ Functor.cong MaybeFunctor (fill-content s) (sequenceV (content c)) ⟩
       id <$> sequenceV (content c)
         ≡⟨ Functor.identity MaybeFunctor (sequenceV (content c)) ⟩
       sequenceV (content c)
@@ -217,27 +217,27 @@ lemma-sequence-successful G {i = i} c {r} p = just-injective (sym (begin
       sequenceV (map just (proj₁ wp))
         ≡⟨ lemma-just-sequenceV (proj₁ wp) ⟩
       just (proj₁ (lemma-<$>-just (sequenceV (content c)) p)) ∎) ⟩
-  fill (|gl₁| i) <$> (map just <$> just (proj₁ (lemma-<$>-just (sequenceV (content c)) p)))
-    ≡⟨ cong (_<$>_ (fill (|gl₁| i)) ∘ just) (sym (lemma-sequenceV-successful (content c) (proj₂ wp))) ⟩
-  fill (|gl₁| i) <$> just (content c)
+  fill s <$> (map just <$> just (proj₁ (lemma-<$>-just (sequenceV (content c)) p)))
+    ≡⟨ cong (_<$>_ (fill s) ∘ just) (sym (lemma-sequenceV-successful (content c) (proj₂ wp))) ⟩
+  fill s <$> just (content c)
     ≡⟨ cong just (content-fill c) ⟩
   just c ∎))
   where open ≡-Reasoning
-        open Get G
+        open Shaped ShapeT
         wp = lemma-<$>-just (sequenceV (content c)) p
 
 lemma-get-sequence : {A : Set} → (G : Get) → {i : Get.|I| G} {v : Get.Container G (Maybe A) (Get.|gl₁| G i)} {r : Get.Container G A (Get.|gl₁| G i)} → Get.sequence G v ≡ just r → Get.get G <$> Get.sequence G v ≡ sequenceV (Get.get G v)
 lemma-get-sequence G {v = v} {r = r} p = begin
   get <$> sequence v
-    ≡⟨ cong (_<$>_ get ∘ sequence) (lemma-sequence-successful G v p) ⟩
+    ≡⟨ cong (_<$>_ get ∘ sequence) (lemma-sequence-successful ShapeT v p) ⟩
   get <$> sequence (fmap just r)
-    ≡⟨ cong (_<$>_ get) (lemma-just-sequence G r) ⟩
+    ≡⟨ cong (_<$>_ get) (lemma-just-sequence ShapeT r) ⟩
   get <$> just r
     ≡⟨ sym (lemma-just-sequenceV (get r)) ⟩
   sequenceV (map just (get r))
     ≡⟨ cong sequenceV (sym (free-theorem just r)) ⟩
   sequenceV (get (fmap just r))
-    ≡⟨ cong (sequenceV ∘ get) (sym (lemma-sequence-successful G v p)) ⟩
+    ≡⟨ cong (sequenceV ∘ get) (sym (lemma-sequence-successful ShapeT v p)) ⟩
   sequenceV (get v) ∎
   where open ≡-Reasoning
         open Get G
@@ -279,9 +279,9 @@ theorem-2 G {i} j s v u p | h′ , ph′ | h , ph = begin⟨ VecISetoid (MaybeSe
 theorem-2′ : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Get.Container G Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Get.Container G Carrier (Get.|gl₁| G j)) → bff G j s v ≡ just (Get.fmap G just u) → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v
 theorem-2′ G j s v u p = drop-just (begin
   get <$> just u
-    ≡⟨ cong (_<$>_ get) (sym (lemma-just-sequence G u)) ⟩
+    ≡⟨ cong (_<$>_ get) (sym (lemma-just-sequence ShapeT u)) ⟩
   get <$> sequence (fmap just u)
-    ≡⟨ lemma-get-sequence G (lemma-just-sequence G u) ⟩
+    ≡⟨ lemma-get-sequence G (lemma-just-sequence ShapeT u) ⟩
   sequenceV (get (fmap just u))
     ≈⟨ sequence-cong (theorem-2 G j s v (fmap just u) p) ⟩
   sequenceV (map just v)
-- 
cgit v1.2.3


From cb7f533f4119f044201df2f28838c96ee367b771 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Mon, 10 Mar 2014 16:11:15 +0100
Subject: also allow Shaped types for the view

Albeit long, this commit is relatively boring.
---
 BFF.agda       |  28 +++++-----
 Bidir.agda     | 171 ++++++++++++++++++++++++++++++++-------------------------
 GetTypes.agda  |  40 ++++++++++++++
 Instances.agda |  49 ++++++++++++++---
 Precond.agda   |  42 +++++++-------
 5 files changed, 211 insertions(+), 119 deletions(-)

diff --git a/BFF.agda b/BFF.agda
index b78e2af..12524ca 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -18,10 +18,10 @@ 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)
+open import GetTypes using (VecVec-to-PartialVecVec ; PartialVecVec-to-PartialShapeVec ; PartialShapeVec-to-PartialShapeShape)
 
 module PartialShapeBFF (A : DecSetoid ℓ₀ ℓ₀) where
-  open GetTypes.PartialShapeVec public using (Get ; module Get)
+  open GetTypes.PartialShapeShape public using (Get ; module Get)
   open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq)
   open CheckInsert A
 
@@ -36,19 +36,19 @@ module PartialShapeBFF (A : DecSetoid ℓ₀ ℓ₀) where
   denumerate : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → {α : Set} {s : S} → (c : C α s) → Fin (Shaped.arity ShapeT s) → α
   denumerate ShapeT c = flip lookupV (Shaped.content ShapeT c)
 
-  bff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Get.Container G Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Get.Container G (Maybe Carrier) (Get.|gl₁| G j))
-  bff G {i} j s v = let s′ = enumerate ShapeT (|gl₁| i)
+  bff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Get.SourceContainer G Carrier (Get.|gl₁| G i) → Get.ViewContainer G Carrier (Get.|gl₂| G j) → Maybe (Get.SourceContainer G (Maybe Carrier) (Get.|gl₁| G j))
+  bff G {i} j s v = let s′ = enumerate SourceShapeT (|gl₁| i)
                         t′ = get s′
-                        g  = fromFunc (denumerate ShapeT s)
-                        g′ = delete-many t′ g
-                        t  = enumerate ShapeT (|gl₁| j)
-                        h  = assoc (get t) v
-                        h′ = (flip union (reshape g′ (arity (|gl₁| j)))) <$> h
-                    in ((λ f → fmap f t) ∘ flip lookupM) <$> h′
+                        g  = fromFunc (denumerate SourceShapeT s)
+                        g′ = delete-many (Shaped.content ViewShapeT t′) g
+                        t  = enumerate SourceShapeT (|gl₁| j)
+                        h  = assoc (Shaped.content ViewShapeT (get t)) (Shaped.content ViewShapeT v)
+                        h′ = (flip union (reshape g′ (Shaped.arity SourceShapeT (|gl₁| j)))) <$> h
+                    in ((λ f → fmapS f t) ∘ flip lookupM) <$> h′
     where open Get G
 
-  sbff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Get.Container G Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Get.Container G Carrier (Get.|gl₁| G j))
-  sbff G j s v = bff G j s v >>= Get.sequence G
+  sbff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Get.SourceContainer G Carrier (Get.|gl₁| G i) → Get.ViewContainer G Carrier (Get.|gl₂| G j) → Maybe (Get.SourceContainer G Carrier (Get.|gl₁| G j))
+  sbff G j s v = bff G j s v >>= Shaped.sequence (Get.SourceShapeT G)
 
 module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where
   open GetTypes.PartialVecVec public using (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 (PartialVecVec-to-PartialShapeVec G) j s v
+  bff G j s v = PartialShapeBFF.bff A (PartialShapeVec-to-PartialShapeShape (PartialVecVec-to-PartialShapeVec 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 (PartialVecVec-to-PartialShapeVec G) j s v
+  sbff  G j s v = PartialShapeBFF.sbff A (PartialShapeVec-to-PartialShapeShape (PartialVecVec-to-PartialShapeVec G)) j s v
 
 module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where
   open GetTypes.VecVec public using (Get)
diff --git a/Bidir.agda b/Bidir.agda
index 9637f17..1513a17 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -25,9 +25,9 @@ open import Relation.Binary using (Setoid ; module Setoid ; module DecSetoid)
 import Relation.Binary.EqReasoning as EqR
 
 open import Structures using (Functor ; IsFunctor ; Shaped ; module Shaped)
-open import Instances using (MaybeFunctor)
+open import Instances using (MaybeFunctor ; ShapedISetoid)
 import GetTypes
-open GetTypes.PartialShapeVec using (Get ; module Get)
+open GetTypes.PartialShapeShape using (Get ; module Get)
 open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; VecISetoid ; just-injective)
 open import FinMap
 import CheckInsert
@@ -122,38 +122,40 @@ lemma-fmap-denumerate-enumerate {S} {C} ShapeT {s = s} c = begin
         open Shaped ShapeT
 
 
-theorem-1 : (G : Get) → {i : Get.|I| G} → (s : Get.Container G Carrier (Get.|gl₁| G i)) → bff G i s (Get.get G s) ≡ just (Get.fmap G just s)
+theorem-1 : (G : Get) → {i : Get.|I| G} → (s : Get.SourceContainer G Carrier (Get.|gl₁| G i)) → bff G i s (Get.get G s) ≡ just (Get.fmapS G just s)
 theorem-1 G {i} s = begin
   bff G i s (get s)
-    ≡⟨ cong (bff G i s ∘ get) (sym (lemma-fmap-denumerate-enumerate ShapeT s)) ⟩
-  bff G i s (get (fmap f t))
+    ≡⟨ cong (bff G i s ∘ get) (sym (lemma-fmap-denumerate-enumerate SourceShapeT s)) ⟩
+  bff G i s (get (fmapS f t))
     ≡⟨ cong (bff G i s) (free-theorem f t) ⟩
-  bff G i s (map f (get t))
+  bff G i s (fmapV f (get t))
     ≡⟨ refl ⟩
-  h′↦r <$> (h↦h′ <$> (assoc (get t) (map f (get t))))
-    ≡⟨ cong (_<$>_ h′↦r ∘ _<$>_ h↦h′) (lemma-1 f (get t)) ⟩
-  (Maybe.just ∘ h′↦r ∘ h↦h′) (restrict f (toList (get t)))
+  h′↦r <$> (h↦h′ <$> (assoc (Shaped.content ViewShapeT (get t)) (Shaped.content ViewShapeT (fmapV f (get t)))))
+    ≡⟨ cong (_<$>_ h′↦r ∘ _<$>_ h↦h′ ∘ assoc (Shaped.content ViewShapeT (get t))) (Shaped.fmap-content ViewShapeT f (get t)) ⟩
+  h′↦r <$> (h↦h′ <$> (assoc (Shaped.content ViewShapeT (get t)) (map f (Shaped.content ViewShapeT (get t)))))
+    ≡⟨ cong (_<$>_ h′↦r ∘ _<$>_ h↦h′) (lemma-1 f (Shaped.content ViewShapeT (get t))) ⟩
+  (Maybe.just ∘ h′↦r ∘ h↦h′) (restrict f (toList (Shaped.content ViewShapeT (get t))))
     ≡⟨ cong just (begin
-      h′↦r (union (restrict f (toList (get t))) (reshape g′ (arity (|gl₁| i))))
-        ≡⟨ cong (h′↦r ∘ union (restrict f (toList (get t)))) (lemma-reshape-id g′) ⟩
-      h′↦r (union (restrict f (toList (get t))) g′)
-        ≡⟨ cong h′↦r (lemma-disjoint-union f (get t)) ⟩
+      h′↦r (union (restrict f (toList (Shaped.content ViewShapeT (get t)))) (reshape g′ (Shaped.arity SourceShapeT (|gl₁| i))))
+        ≡⟨ cong (h′↦r ∘ union (restrict f (toList (Shaped.content ViewShapeT (get t))))) (lemma-reshape-id g′) ⟩
+      h′↦r (union (restrict f (toList (Shaped.content ViewShapeT (get t)))) g′)
+        ≡⟨ cong h′↦r (lemma-disjoint-union f (Shaped.content ViewShapeT (get t))) ⟩
       h′↦r (fromFunc f)
         ≡⟨ refl ⟩
-      fmap (flip lookupM (fromFunc f)) t
-        ≡⟨ IsFunctor.cong (isFunctor (|gl₁| i)) (lemma-lookupM-fromFunc f) t ⟩
-      fmap (Maybe.just ∘ f) t
-        ≡⟨ IsFunctor.composition (isFunctor (|gl₁| i)) just f t ⟩
-      fmap just (fmap f t)
-        ≡⟨ cong (fmap just) (lemma-fmap-denumerate-enumerate ShapeT s) ⟩
-      fmap just s ∎) ⟩ _ ∎
+      fmapS (flip lookupM (fromFunc f)) t
+        ≡⟨ IsFunctor.cong (Shaped.isFunctor SourceShapeT (|gl₁| i)) (lemma-lookupM-fromFunc f) t ⟩
+      fmapS (Maybe.just ∘ f) t
+        ≡⟨ IsFunctor.composition (Shaped.isFunctor SourceShapeT (|gl₁| i)) just f t ⟩
+      fmapS just (fmapS f t)
+        ≡⟨ cong (fmapS just) (lemma-fmap-denumerate-enumerate SourceShapeT s) ⟩
+      fmapS just s ∎) ⟩ _ ∎
     where open ≡-Reasoning
           open Get G
-          t    = enumerate ShapeT (|gl₁| i)
-          f    = denumerate ShapeT s
-          g′   = delete-many (get t) (fromFunc f)
-          h↦h′ = flip union (reshape g′ (arity (|gl₁| i)))
-          h′↦r = (λ f′ → fmap f′ t) ∘ flip lookupM
+          t    = enumerate SourceShapeT (|gl₁| i)
+          f    = denumerate SourceShapeT s
+          g′   = delete-many (Shaped.content ViewShapeT (get t)) (fromFunc f)
+          h↦h′ = flip union (reshape g′ (Shaped.arity SourceShapeT (|gl₁| i)))
+          h′↦r = (λ f′ → fmapS f′ t) ∘ flip lookupM
 
 
 lemma-<$>-just : {A B : Set} {f : A → B} {b : B} (ma : Maybe A) → f <$> ma ≡ just b → ∃ λ a → ma ≡ just a
@@ -226,66 +228,85 @@ lemma-sequence-successful ShapeT {s = s} c {r} p = just-injective (sym (begin
         open Shaped ShapeT
         wp = lemma-<$>-just (sequenceV (content c)) p
 
-lemma-get-sequence : {A : Set} → (G : Get) → {i : Get.|I| G} {v : Get.Container G (Maybe A) (Get.|gl₁| G i)} {r : Get.Container G A (Get.|gl₁| G i)} → Get.sequence G v ≡ just r → Get.get G <$> Get.sequence G v ≡ sequenceV (Get.get G v)
+lemma-get-sequence : {A : Set} → (G : Get) → {i : Get.|I| G} {v : Get.SourceContainer G (Maybe A) (Get.|gl₁| G i)} {r : Get.SourceContainer G A (Get.|gl₁| G i)} → Shaped.sequence (Get.SourceShapeT G) v ≡ just r → Get.get G <$> Shaped.sequence (Get.SourceShapeT G) v ≡ Shaped.sequence (Get.ViewShapeT G) (Get.get G v)
 lemma-get-sequence G {v = v} {r = r} p = begin
-  get <$> sequence v
-    ≡⟨ cong (_<$>_ get ∘ sequence) (lemma-sequence-successful ShapeT v p) ⟩
-  get <$> sequence (fmap just r)
-    ≡⟨ cong (_<$>_ get) (lemma-just-sequence ShapeT r) ⟩
+  get <$> Shaped.sequence SourceShapeT v
+    ≡⟨ cong (_<$>_ get ∘ Shaped.sequence SourceShapeT) (lemma-sequence-successful SourceShapeT v p) ⟩
+  get <$> Shaped.sequence SourceShapeT (fmapS just r)
+    ≡⟨ cong (_<$>_ get) (lemma-just-sequence SourceShapeT r) ⟩
   get <$> just r
-    ≡⟨ sym (lemma-just-sequenceV (get r)) ⟩
-  sequenceV (map just (get r))
-    ≡⟨ cong sequenceV (sym (free-theorem just r)) ⟩
-  sequenceV (get (fmap just r))
-    ≡⟨ cong (sequenceV ∘ get) (sym (lemma-sequence-successful ShapeT v p)) ⟩
-  sequenceV (get v) ∎
+    ≡⟨ sym (lemma-just-sequence ViewShapeT (get r)) ⟩
+  Shaped.sequence ViewShapeT (fmapV just (get r))
+    ≡⟨ cong (Shaped.sequence ViewShapeT) (sym (free-theorem just r)) ⟩
+  Shaped.sequence ViewShapeT (get (fmapS just r))
+    ≡⟨ cong (Shaped.sequence ViewShapeT ∘ get) (sym (lemma-sequence-successful SourceShapeT v p)) ⟩
+  Shaped.sequence ViewShapeT (get v) ∎
   where open ≡-Reasoning
         open Get G
 
-sequence-cong : {S : Setoid ℓ₀ ℓ₀} {n : ℕ} {m₁ m₂ : Setoid.Carrier (VecISetoid (MaybeSetoid S) at n)} → VecISetoid (MaybeSetoid S) at _ ∋ m₁ ≈ m₂ → MaybeSetoid (VecISetoid S at n) ∋ sequenceV m₁ ≈ sequenceV m₂
-sequence-cong {S}                                       VecEq.[]-cong = Setoid.refl (MaybeSetoid (VecISetoid S at _))
-sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) with sequenceV xs | sequenceV ys | sequence-cong xs≈ys
-sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | just sxs | just sys | just p = MaybeEq.just (VecEq._∷-cong_ x≈y p)
-sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | just sys | ()
-sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | just sxs | nothing | ()
-sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (VecISetoid S at _))
-sequence-cong {S}                                       (VecEq._∷-cong_ nothing xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S at _))
+sequenceV-cong : {S : Setoid ℓ₀ ℓ₀} {n : ℕ} {m₁ m₂ : Setoid.Carrier (VecISetoid (MaybeSetoid S) at n)} → VecISetoid (MaybeSetoid S) at _ ∋ m₁ ≈ m₂ → MaybeSetoid (VecISetoid S at n) ∋ sequenceV m₁ ≈ sequenceV m₂
+sequenceV-cong {S}                                       VecEq.[]-cong = Setoid.refl (MaybeSetoid (VecISetoid S at _))
+sequenceV-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) with sequenceV xs | sequenceV ys | sequenceV-cong xs≈ys
+sequenceV-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | just sxs | just sys | just p = MaybeEq.just (VecEq._∷-cong_ x≈y p)
+sequenceV-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | just sys | ()
+sequenceV-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | just sxs | nothing | ()
+sequenceV-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (VecISetoid S at _))
+sequenceV-cong {S}                                       (VecEq._∷-cong_ nothing xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S at _))
 
-theorem-2 : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Get.Container G Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Get.Container G (Maybe Carrier) (Get.|gl₁| G j)) → bff G j s v ≡ just u → VecISetoid (MaybeSetoid A.setoid) at _ ∋ Get.get G u ≈ map just v
-theorem-2 G {i} j s v u p with (lemma-<$>-just ((flip union (reshape (delete-many (Get.get G (enumerate (Get.ShapeT G) (Get.|gl₁| G i))) (fromFunc (denumerate (Get.ShapeT G) s))) (Get.arity G (Get.|gl₁| G j)))) <$> (assoc (Get.get G (enumerate (Get.ShapeT G) (Get.|gl₁| G j))) v)) p)
-theorem-2 G {i} j s v u p | h′ , ph′ with (lemma-<$>-just (assoc (Get.get G (enumerate (Get.ShapeT G) (Get.|gl₁| G j))) v) ph′)
-theorem-2 G {i} j s v u p | h′ , ph′ | h , ph = begin⟨ VecISetoid (MaybeSetoid A.setoid) at _ ⟩
-  get u
-    ≡⟨ just-injective (trans (cong (_<$>_ get) (sym p))
-                             (cong (_<$>_ get ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph)) ⟩
-  get (h′↦r (h↦h′ h))
+sequence-cong : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → (α : Setoid ℓ₀ ℓ₀) → {s : S} {x y : C (Maybe (Setoid.Carrier α)) s} → ShapedISetoid (EqSetoid S) ShapeT (MaybeSetoid α) at _ ∋ x ≈ y → MaybeSetoid (ShapedISetoid (EqSetoid S) ShapeT α at _) ∋ Shaped.sequence ShapeT x ≈ Shaped.sequence ShapeT y
+sequence-cong ShapeT α {x = x} {y = y} (shape≈ , content≈) with sequenceV (Shaped.content ShapeT x) | sequenceV (Shaped.content ShapeT y) | sequenceV-cong content≈
+sequence-cong ShapeT α {s} (shape≈ , content≈) | .(just x) | .(just y) | just {x} {y} x≈y = just (refl , (begin
+  content (fill s x)
+    ≡⟨ fill-content s x ⟩
+  x
+    ≈⟨ x≈y ⟩
+  y
+    ≡⟨ sym (fill-content s y) ⟩
+  content (fill s y) ∎))
+  where open EqR (VecISetoid α at _)
+        open Shaped ShapeT
+sequence-cong ShapeT α (shape≈ , content≈) | .nothing  | .nothing  | nothing = nothing
+
+theorem-2 : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Get.SourceContainer G Carrier (Get.|gl₁| G i)) → (v : Get.ViewContainer G Carrier (Get.|gl₂| G j)) → (u : Get.SourceContainer G (Maybe Carrier) (Get.|gl₁| G j)) → bff G j s v ≡ just u → ShapedISetoid (EqSetoid _) (Get.ViewShapeT G) (MaybeSetoid A.setoid) at _ ∋ Get.get G u ≈ Get.fmapV G just v
+theorem-2 G {i} j s v u p with (lemma-<$>-just ((flip union (reshape (delete-many (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.|gl₁| G i)))) (fromFunc (denumerate (Get.SourceShapeT G) s))) (Shaped.arity (Get.SourceShapeT G) (Get.|gl₁| G j)))) <$> (assoc (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.|gl₁| G j)))) (Shaped.content (Get.ViewShapeT G) v))) p)
+theorem-2 G {i} j s v u p | h′ , ph′ with (lemma-<$>-just (assoc (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.|gl₁| G j)))) (Shaped.content (Get.ViewShapeT G) v)) ph′)
+theorem-2 G {i} j s v u p | h′ , ph′ | h , ph = refl , (begin⟨ VecISetoid (MaybeSetoid A.setoid) at _ ⟩
+  content (get u)
+    ≡⟨ cong content (just-injective (trans (cong (_<$>_ get) (sym p))
+                                           (cong (_<$>_ get ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph))) ⟩
+  content (get (h′↦r (h↦h′ h)))
     ≡⟨ refl ⟩
-  get (fmap (flip lookupM (h↦h′ h)) t)
-    ≡⟨ free-theorem (flip lookupM (h↦h′ h)) t ⟩
-  map (flip lookupM (h↦h′ h)) (get t)
-    ≡⟨ lemma-union-not-used h g′ (get t) (lemma-assoc-domain (get t) v h ph) ⟩
-  map (flip lookupM h) (get t)
-    ≈⟨ lemma-2 (get t) v h ph ⟩
-  map just v ∎
+  content (get (fmapS (flip lookupM (h↦h′ h)) t))
+    ≡⟨ cong content (free-theorem (flip lookupM (h↦h′ h)) t) ⟩
+  content (fmapV (flip lookupM (h↦h′ h)) (get t))
+    ≡⟨ Shaped.fmap-content ViewShapeT (flip lookupM (h↦h′ h)) (get t) ⟩
+  map (flip lookupM (h↦h′ h)) (content (get t))
+    ≡⟨ lemma-union-not-used h g′ (content (get t)) (lemma-assoc-domain (content (get t)) (content v) h ph) ⟩
+  map (flip lookupM h) (content (get t))
+    ≈⟨ lemma-2 (content (get t)) (content v) h ph ⟩
+  map just (content v)
+    ≡⟨ sym (Shaped.fmap-content ViewShapeT just v) ⟩
+  content (fmapV just v) ∎)
     where open SetoidReasoning
           open Get G
-          s′   = enumerate ShapeT (|gl₁| i)
-          g    = fromFunc (denumerate ShapeT s)
-          g′   = delete-many (get s′) g
-          t    = enumerate ShapeT (|gl₁| j)
-          h↦h′ = flip union (reshape g′ (arity (|gl₁| j)))
-          h′↦r = (λ f → fmap f t) ∘ flip lookupM
+          open Shaped ViewShapeT using (content)
+          s′   = enumerate SourceShapeT (|gl₁| i)
+          g    = fromFunc (denumerate SourceShapeT s)
+          g′   = delete-many (Shaped.content ViewShapeT (get s′)) g
+          t    = enumerate SourceShapeT (|gl₁| j)
+          h↦h′ = flip union (reshape g′ (Shaped.arity SourceShapeT (|gl₁| j)))
+          h′↦r = (λ f → fmapS f t) ∘ flip lookupM
 
-theorem-2′ : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Get.Container G Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Get.Container G Carrier (Get.|gl₁| G j)) → bff G j s v ≡ just (Get.fmap G just u) → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v
+theorem-2′ : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Get.SourceContainer G Carrier (Get.|gl₁| G i)) → (v : Get.ViewContainer G Carrier (Get.|gl₂| G j)) → (u : Get.SourceContainer G Carrier (Get.|gl₁| G j)) → bff G j s v ≡ just (Get.fmapS G just u) → ShapedISetoid (EqSetoid _) (Get.ViewShapeT G) A.setoid at _ ∋ Get.get G u ≈ v
 theorem-2′ G j s v u p = drop-just (begin
   get <$> just u
-    ≡⟨ cong (_<$>_ get) (sym (lemma-just-sequence ShapeT u)) ⟩
-  get <$> sequence (fmap just u)
-    ≡⟨ lemma-get-sequence G (lemma-just-sequence ShapeT u) ⟩
-  sequenceV (get (fmap just u))
-    ≈⟨ sequence-cong (theorem-2 G j s v (fmap just u) p) ⟩
-  sequenceV (map just v)
-    ≡⟨ lemma-just-sequenceV v ⟩
+    ≡⟨ cong (_<$>_ get) (sym (lemma-just-sequence SourceShapeT u)) ⟩
+  get <$> Shaped.sequence SourceShapeT (fmapS just u)
+    ≡⟨ lemma-get-sequence G (lemma-just-sequence SourceShapeT u) ⟩
+  Shaped.sequence ViewShapeT (get (fmapS just u))
+    ≈⟨ sequence-cong ViewShapeT A.setoid (theorem-2 G j s v (fmapS just u) p) ⟩
+  Shaped.sequence ViewShapeT (fmapV just v)
+    ≡⟨ lemma-just-sequence ViewShapeT v ⟩
   just v ∎)
-  where open EqR (MaybeSetoid (VecISetoid A.setoid at _))
-        open Get G
+  where open Get G
+        open EqR (MaybeSetoid (ShapedISetoid (EqSetoid _) ViewShapeT A.setoid at _))
diff --git a/GetTypes.agda b/GetTypes.agda
index 0db3f31..2812e2b 100644
--- a/GetTypes.agda
+++ b/GetTypes.agda
@@ -84,3 +84,43 @@ PartialVecVec-to-PartialShapeVec G = record
   ; get          = get
   ; free-theorem = free-theorem
   } where open PartialVecVec.Get G
+
+module PartialShapeShape where
+  record Get : Set₁ where
+    field
+      SourceShape : Set
+      SourceContainer : Set → SourceShape → Set
+      SourceShapeT : Shaped SourceShape SourceContainer
+
+      ViewShape : Set
+      ViewContainer : Set → ViewShape → Set
+      ViewShapeT : Shaped ViewShape ViewContainer
+
+      I : Setoid ℓ₀ ℓ₀
+      gl₁ : I ↪ EqSetoid SourceShape
+      gl₂ : I ⟶ EqSetoid ViewShape
+
+    |I|   = Setoid.Carrier I
+    |gl₁| = _⟨$⟩_ (to gl₁)
+    |gl₂| = _⟨$⟩_ gl₂
+
+    open Shaped SourceShapeT using () renaming (fmap to fmapS)
+    open Shaped ViewShapeT using () renaming (fmap to fmapV)
+
+    field
+      get : {A : Set} {i : |I|} → SourceContainer A (|gl₁| i) → ViewContainer A (|gl₂| i)
+      free-theorem : {α β : Set} → (f : α → β) → {i : |I|} → get {_} {i} ∘ fmapS f ≗ fmapV f ∘ get
+
+    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
+  ; ViewShapeT   = VecShaped
+  ; I            = I
+  ; gl₁          = gl₁
+  ; gl₂          = gl₂
+  ; get          = get
+  ; free-theorem = free-theorem
+  } where open PartialShapeVec.Get G
diff --git a/Instances.agda b/Instances.agda
index b41b0a2..2e4ed3e 100644
--- a/Instances.agda
+++ b/Instances.agda
@@ -1,13 +1,22 @@
 module Instances where
 
+open import Level using () renaming (zero to ℓ₀)
 open import Category.Functor using (RawFunctor)
 open import Data.Maybe as M using (Maybe)
 open import Data.Nat using (ℕ)
+open import Data.Product using (_×_ ; _,_ ; proj₁ ; proj₂)
 open import Data.Vec using (Vec)
+import Data.Vec.Equality
+open Data.Vec.Equality.PropositionalEquality using () renaming (to-≡ to VecEq-to-≡)
 open import Function using (_∘_ ; id)
-open import Relation.Binary.PropositionalEquality as P using (_≗_ ; refl)
+open import Relation.Binary using (Setoid ; module Setoid)
+open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid)
+open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≗_ ; module ≡-Reasoning)
 
-open import Structures using (Functor ; Shaped)
+open Setoid using () renaming (_≈_ to _∋_≈_)
+
+open import Generic using (VecISetoid)
+open import Structures using (Functor ; Shaped ; module Shaped)
 
 MaybeFunctor : Functor Maybe
 MaybeFunctor = record
@@ -21,15 +30,15 @@ MaybeFunctor = record
 
         cong : {α β : Set} {g h : α → β} → g ≗ h → _<$>_ g ≗ _<$>_ h
         cong g≗h (M.just x) = P.cong M.just (g≗h x)
-        cong g≗h M.nothing  = refl
+        cong g≗h M.nothing  = P.refl
 
         identity : {α : Set} → _<$>_ {α} id ≗ id
-        identity (M.just x) = refl
-        identity M.nothing  = refl
+        identity (M.just x) = P.refl
+        identity M.nothing  = P.refl
 
         composition : {α β γ : Set} → (g : β → γ) → (h : α → β) → _<$>_ (g ∘ h) ≗ _<$>_ g ∘ _<$>_ h
-        composition g h (M.just x) = refl
-        composition g h M.nothing = refl
+        composition g h (M.just x) = P.refl
+        composition g h M.nothing  = P.refl
 
 VecShaped : Shaped ℕ Vec
 VecShaped = record
@@ -37,6 +46,28 @@ VecShaped = record
   ; content = id
   ; fill = λ _ → id
   ; isShaped = record
-    { content-fill = λ _ → refl
-    ; fill-content = λ _ _ → refl
+    { content-fill = λ _ → P.refl
+    ; fill-content = λ _ _ → P.refl
     } }
+
+ShapedISetoid : (S : Setoid ℓ₀ ℓ₀) {C : Set → (Setoid.Carrier S) → Set} → Shaped (Setoid.Carrier S) C → Setoid ℓ₀ ℓ₀ → ISetoid (Setoid.Carrier S) ℓ₀ ℓ₀
+ShapedISetoid S {C} ShapeT α = record
+  { Carrier = C (Setoid.Carrier α)
+  ; _≈_ = λ {s₁} {s₂} c₁ c₂ → S ∋ s₁ ≈ s₂ × ISetoid._≈_ (VecISetoid α) (content c₁) (content c₂)
+  ; isEquivalence = record
+    { refl = Setoid.refl S , ISetoid.refl (VecISetoid α)
+    ; sym = λ p → Setoid.sym S (proj₁ p) , ISetoid.sym (VecISetoid α) (proj₂ p)
+    ; trans = λ p q → Setoid.trans S (proj₁ p) (proj₁ q) , ISetoid.trans (VecISetoid α) (proj₂ p) (proj₂ q)
+    } } where open Shaped ShapeT
+
+Shaped≈-to-≡ : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → (α : Set) → {s : S} {x y : C α s} → ShapedISetoid (P.setoid S) ShapeT (P.setoid α) at s ∋ x ≈ y → x ≡ y
+Shaped≈-to-≡ ShapeT α {s} {x} {y} (shape≈ , content≈) = begin
+  x
+    ≡⟨ P.sym (content-fill x) ⟩
+  fill s (content x)
+    ≡⟨ P.cong (fill s) (VecEq-to-≡ content≈) ⟩
+  fill s (content y)
+    ≡⟨ content-fill y ⟩
+  y ∎
+  where open ≡-Reasoning
+        open Shaped ShapeT
diff --git a/Precond.agda b/Precond.agda
index bc54cd5..85c955c 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -25,7 +25,7 @@ open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ;
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 open import Relation.Nullary using (yes ; no)
 
-open import Structures using (IsFunctor)
+open import Structures using (IsFunctor ; Shaped)
 open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty ; delete-many ; lemma-tabulate-∘ ; delete ; lemma-lookupM-delete ; lemma-lookupM-fromFunc ; reshape ; lemma-reshape-id)
 import CheckInsert
 open CheckInsert (decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other)
@@ -33,7 +33,7 @@ import BFF
 import Bidir
 open Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain)
 import GetTypes
-open GetTypes.PartialShapeVec using (Get ; module Get)
+open GetTypes.PartialShapeShape using (Get ; module Get)
 open BFF.PartialShapeBFF (decSetoid deq) using (assoc ; enumerate ; denumerate ; bff)
 
 lemma-maybe-just : {A : Set} → (a : A) → (ma : Maybe A) → maybe′ Maybe.just (just a) ma ≡ Maybe.just (maybe′ id a ma)
@@ -63,32 +63,32 @@ lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (Data.List.A
           maybe′ just (lookupM i (delete-many is (fromFunc g))) (lookup i h) ∎
         inner f | no f≢i = cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (fromFunc g)) f≢i)
 
-assoc-enough : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Get.Container G Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → ∃ (λ h → assoc (Get.get G (enumerate (Get.ShapeT G) (Get.|gl₁| G j))) v ≡ just h) → ∃ λ u → bff G j s v ≡ just u
-assoc-enough G {i} j s v (h , p) = _ , cong (_<$>_ ((λ f → fmap f t) ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (arity (|gl₁| j))))) p
+assoc-enough : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Get.SourceContainer G Carrier (Get.|gl₁| G i)) → (v : Get.ViewContainer G Carrier (Get.|gl₂| G j)) → ∃ (λ h → assoc (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.|gl₁| G j)))) (Shaped.content (Get.ViewShapeT G) v) ≡ just h) → ∃ λ u → bff G j s v ≡ just u
+assoc-enough G {i} j s v (h , p) = _ , cong (_<$>_ ((λ f → fmapS f t) ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (Shaped.arity SourceShapeT (|gl₁| j))))) p
   where open Get G
-        g′ = delete-many (get (enumerate ShapeT (|gl₁| i))) (fromFunc (denumerate ShapeT s))
-        t  = enumerate ShapeT (|gl₁| j)
+        g′ = delete-many (Shaped.content ViewShapeT (get (enumerate SourceShapeT (|gl₁| i)))) (fromFunc (denumerate SourceShapeT s))
+        t  = enumerate SourceShapeT (|gl₁| j)
 
-assoc-enough′ : (G : Get) → {i : Get.|I| G} → (s : Get.Container G Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G i)) → ∃ (λ h → assoc (Get.get G (enumerate (Get.ShapeT G) (Get.|gl₁| G i))) v ≡ just h) → ∃ λ u → bff G i s v ≡ just (Get.fmap G just u)
+assoc-enough′ : (G : Get) → {i : Get.|I| G} → (s : Get.SourceContainer G Carrier (Get.|gl₁| G i)) → (v : Get.ViewContainer G Carrier (Get.|gl₂| G i)) → ∃ (λ h → assoc (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.|gl₁| G i)))) (Shaped.content (Get.ViewShapeT G) v) ≡ just h) → ∃ λ u → bff G i s v ≡ just (Get.fmapS G just u)
 assoc-enough′ G {i} s v (h , p) = _ , (begin
   bff G i s v
     ≡⟨ proj₂ (assoc-enough G i s v (h , p)) ⟩
-  just (fmap (flip lookupM (union h (reshape g′ (arity (|gl₁| i))))) t)
+  just (fmapS (flip lookupM (union h (reshape g′ (Shaped.arity SourceShapeT (|gl₁| i))))) t)
     ≡⟨ cong just (begin _
-        ≡⟨ cong ((λ f → fmap f t) ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩
-      fmap (flip lookupM (union h g′)) t
-        ≡⟨ cong ((λ f → fmap f t) ∘ flip lookupM) (proj₂ wp) ⟩
-      fmap (flip lookupM (fromFunc (proj₁ wp))) t
-        ≡⟨ IsFunctor.cong (isFunctor (|gl₁| i)) (lemma-lookupM-fromFunc (proj₁ wp)) t ⟩
-      fmap (Maybe.just ∘ proj₁ wp) t
-        ≡⟨ IsFunctor.composition (isFunctor (|gl₁| i)) just (proj₁ wp) t ⟩
-      fmap Maybe.just (fmap (proj₁ wp) t) ∎) ⟩ _ ∎)
+        ≡⟨ cong ((λ f → fmapS f t) ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩
+      fmapS (flip lookupM (union h g′)) t
+        ≡⟨ cong ((λ f → fmapS f t) ∘ flip lookupM) (proj₂ wp) ⟩
+      fmapS (flip lookupM (fromFunc (proj₁ wp))) t
+        ≡⟨ IsFunctor.cong (Shaped.isFunctor SourceShapeT (|gl₁| i)) (lemma-lookupM-fromFunc (proj₁ wp)) t ⟩
+      fmapS (Maybe.just ∘ proj₁ wp) t
+        ≡⟨ IsFunctor.composition (Shaped.isFunctor SourceShapeT (|gl₁| i)) just (proj₁ wp) t ⟩
+      fmapS Maybe.just (fmapS (proj₁ wp) t) ∎) ⟩ _ ∎)
   where open Get G
-        s′ = enumerate ShapeT (|gl₁| i)
-        g  = fromFunc (denumerate ShapeT s)
-        g′ = delete-many (get s′) g
-        t  = enumerate ShapeT (|gl₁| i)
-        wp = lemma-union-delete-fromFunc (lemma-assoc-domain (get t) v h p)
+        s′ = enumerate SourceShapeT (|gl₁| i)
+        g  = fromFunc (denumerate SourceShapeT s)
+        g′ = delete-many (Shaped.content ViewShapeT (get s′)) g
+        t  = enumerate SourceShapeT (|gl₁| i)
+        wp = lemma-union-delete-fromFunc (lemma-assoc-domain (Shaped.content ViewShapeT (get t)) (Shaped.content ViewShapeT v) h p)
 
 data All-different {A : Set} : List A → Set where
   different-[] : All-different []
-- 
cgit v1.2.3


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.
---
 BFF.agda      |  6 +++---
 GetTypes.agda | 41 ++++-------------------------------------
 2 files changed, 7 insertions(+), 40 deletions(-)

diff --git a/BFF.agda b/BFF.agda
index 12524ca..26d1d5e 100644
--- 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
--- 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