# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1483496471 0
# Node ID 0a780145c5ff53253160f38c6a64ce847a2c6095
# Parent  f7916d13e2b149a104658bd8429f855eaec3dd7c
Define compose operator using list of subtype

diff -r f7916d13e2b1 -r 0a780145c5ff cbc/named-product.agda
--- a/cbc/named-product.agda	Tue Jan 03 09:04:11 2017 +0000
+++ b/cbc/named-product.agda	Wed Jan 04 02:21:11 2017 +0000
@@ -64,7 +64,9 @@
 
 
 data CodeSegment (A B : Set) : (List Set) -> Set where
-  cs : {l : List Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B l
+  cs : {l : List Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B (A ∷ B ∷ l)
+
+
   
 
 exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context
@@ -75,8 +77,8 @@
 equiv-exec = refl
 
 
-_◎_ : {A B C : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {l ll : List Set}
-       -> CodeSegment B C l -> CodeSegment A B ll -> CodeSegment A C (l ++ ll)
-_◎_ {{da}} {{_}} {{dc}} {l = l} {ll = ll} (cs g) (cs f) = cs  {l = l ++ ll} {{da}} {{dc}} (g ∘ f)
+_◎_ : {A B C : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {l ll  : List Set}
+       -> CodeSegment B C (B ∷ C ∷ l) -> CodeSegment A B (A ∷ B ∷ ll) -> CodeSegment A C (A ∷ C ∷ B ∷ (l ++ ll))
+_◎_ {A} {B} {C} {{da}} {{_}} {{dc}} {l} {ll} (cs g) (cs f) =  cs {l = (B ∷ (l ++ ll))} {{da}} {{dc}} (g ∘ f)