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.
---
 GetTypes.agda | 40 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)

(limited to 'GetTypes.agda')

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