From 20c176d383e59a0345f7425c5f14679906159a59 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Tue, 4 Feb 2014 10:52:49 +0100
Subject: add convenience members to PartialVecVec.Get

---
 GetTypes.agda | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'GetTypes.agda')

diff --git a/GetTypes.agda b/GetTypes.agda
index a52ec24..eb72cea 100644
--- a/GetTypes.agda
+++ b/GetTypes.agda
@@ -32,8 +32,14 @@ module PartialVecVec where
       I : Setoid ℓ₀ ℓ₀
       gl₁ : I ↪ EqSetoid ℕ
       gl₂ : I ⟶ EqSetoid ℕ
-      get : {A : Set} {i : Setoid.Carrier I} → Vec A (to gl₁ ⟨$⟩ i) → Vec A (gl₂ ⟨$⟩ i)
-      free-theorem : {α β : Set} → (f : α → β) → {i : Setoid.Carrier I} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get
+
+    |I|   = Setoid.Carrier I
+    |gl₁| = _⟨$⟩_ (to gl₁)
+    |gl₂| = _⟨$⟩_ gl₂
+
+    field
+      get : {A : Set} {i : |I|} → Vec A (|gl₁| i) → Vec A (|gl₂| i)
+      free-theorem : {α β : Set} → (f : α → β) → {i : |I|} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get
 
 VecVec-to-PartialVecVec : VecVec.Get → PartialVecVec.Get
 VecVec-to-PartialVecVec G = record
-- 
cgit v1.2.3