--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cbc/maybe-subtype-sample.agda	Thu Jan 12 01:05:06 2017 +0000
@@ -0,0 +1,13 @@
+module maybe-subtype-sample where
+
+open import subtype 
+
+
+return : {_ : Context A} {_ : Meta (Context A)} {{_ : N.DataSegment A}} {{_ : M.DataSegment A}} -> A -> Meta A
+return {c} {mc} {{nd}} {{md}} a = record {context = con ; maybeElem = just a}
+  where
+    con = record { elem = a }
+
+
+fmap : {B : Set} {{_ : M.DataSegment A}} {{_ : M.DataSegment B}} -> M.CodeSegment A B -> Meta (Context A) -> Meta (Context B)
+fmap code x = {!!} -- exec code x