--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cbc/subtype.agda	Mon Jan 02 04:40:48 2017 +0000
@@ -0,0 +1,35 @@
+module subtype where
+
+open import Level
+open import Function
+open import Data.Nat hiding (_⊔_)
+open import Data.Bool
+
+data DataSegment  (X : Set -> Set) : Set₁  where
+  ds : {x : Set} -> X x -> DataSegment X
+
+
+record DS1 (A : Set) : Set where
+  field
+    counter : A -> ℕ
+
+record DS2 (A : Set) : Set where
+  field
+    useSum : A -> Bool
+
+record Context : Set where
+  field
+    loopCounter : ℕ
+    flag        : Bool
+
+instance
+  ds1 : DS1 Context
+  ds1 = record {counter = Context.loopCounter}
+
+hoge :  Context -> {{ins : DS1 Context}} -> DataSegment DS1
+hoge _ {{i}}  = ds i
+
+
+
+data CodeSegment (I O : (Set -> Set)) : Set₁ where
+  cs : (DataSegment I -> DataSegment O) -> CodeSegment I O