Move stream to experiments

diff --git a/examples/stream.ctt b/experiments/stream.ctt
similarity index 94%
rename from examples/stream.ctt
rename to experiments/stream.ctt
index db05e08ba65c99a6ca5921436c2a657d477c3398..e7f7c031441c7d11eaf4cfaf9affacd793116157 100644 (file)
--- a/examples/stream.ctt
+++ b/experiments/stream.ctt
@@ -1,6 +1,15 @@
 module stream where
 
-import prelude
+-- Things from the prelude:
+Id (A : U) (a0 a1 : A) : U = IdP (<i> A) a0 a1
+
+refl (A : U) (a : A) : Id A a a = <i> a
+
+isoId (A B : U) (f : A -> B) (g : B -> A)
+      (s : (y:B) -> Id B (f (g y)) y)
+      (t : (x:A) -> Id A (g (f x)) x) : Id U A B =
+      <i> glue B [ (i = 0) -> (A,f,g,s,t) ]
+
 
 -- Let us pretend that Stream is a coinductive type.