--- a/cbc/maybe-subtype.agda	Thu Jan 12 02:48:09 2017 +0000
+++ b/cbc/maybe-subtype.agda	Sat Jan 14 00:00:40 2017 +0000
@@ -1,31 +1,19 @@
-module maybe-subtype (A : Set) where
-
 open import Level
+open import Data.Maybe
 open import Function using (id)
 open import Relation.Binary.PropositionalEquality
 
-data Maybe (A : Set) : Set where
-  nothing : Maybe A
-  just    : A -> Maybe A
+module maybe-subtype (A : Set)  where
 
 
-record Context (A : Set) : Set where
-  field
-    maybeElem : Maybe A
+record Context : Set where
 
-open import subtype (Context A) as N
+open import subtype Context as N
 
 
 record Meta (A : Set) : Set where
   field
-    context : Context A
+    context   : Context
+    maybeElem : Maybe A
 
 
-open import subtype (Meta A) as M
-
-instance
-  MetaIsMetaDataSegment : M.DataSegment (Meta A)
-  MetaIsMetaDataSegment = record {get = (\mc -> mc) ; set = (\_ mc -> mc)}
-  ContextIsMetaDataSegment : M.DataSegment (Context A)
-  ContextIsMetaDataSegment = record {get = Meta.context ; set = (\mc c -> record mc {context = c})}
-