From: Anders Mörtberg <mortberg@chalmers.se>
Date: Mon, 13 Apr 2015 17:41:17 +0000 (+0200)
Subject: Move stream to experiments
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=c02f09b14eb296dc984b52074841b09f8fffb984;p=cubicaltt.git

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 db05e08..e7f7c03 100644
--- 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.