diff --git a/agda/Data/Fin/MoreProps.agda b/agda/Data/Fin/MoreProps.agda
index 0481344..d7c2c21 100644
--- a/agda/Data/Fin/MoreProps.agda
+++ b/agda/Data/Fin/MoreProps.agda
@@ -4,11 +4,22 @@ module Data.Fin.MoreProps where
 open import Data.Nat hiding (_>_) renaming (_<_ to _<ℕ_)
 open import Data.Fin
 open import Data.Fin.Properties
+open import Data.Unit
+open import Data.Empty
 open import Relation.Binary.PropositionalEquality
 open import Relation.Binary.PropositionalEquality.WithK
 open import Algebra.Structures.Propositional
 open import Function
 
+IsMax : ∀ {n} → Fin n → Set
+IsMax {(suc zero)} zero = ⊤
+IsMax {(suc (suc _))} zero = ⊥
+IsMax (suc x) = IsMax x
+
+fromℕ-ismax : ∀ n → IsMax (fromℕ n)
+fromℕ-ismax zero = tt
+fromℕ-ismax (suc n) = fromℕ-ismax n
+
 <-isPropStrictTotalOrder : ∀ n → IsPropStrictTotalOrder (_≡_ {A = Fin n}) _<_
 IsPropStrictTotalOrder.isSTO (<-isPropStrictTotalOrder n) = <-isStrictTotalOrder
 IsPropStrictTotalOrder.≈-prop (<-isPropStrictTotalOrder n) = ≡-irrelevant
diff --git a/agda/Data/List/Snoc.agda b/agda/Data/List/Snoc.agda
new file mode 100644
index 0000000..9b4f3c6
--- /dev/null
+++ b/agda/Data/List/Snoc.agda
@@ -0,0 +1,44 @@
+{-# OPTIONS --safe --cubical-compatible #-}
+
+-- Working with snoc lists.
+module Data.List.Snoc where
+open import Data.Product
+open import Relation.Nullary
+
+private variable
+  X : Set
+
+data List (X : Set) : Set where
+  [] : List X
+  _,-_ : X → List X → List X
+
+data Empty {X : Set} : List X → Set where
+  instance [] : Empty []
+
+data NonEmpty {X : Set} : List X → Set where
+  instance cons : ∀ {x xs} → NonEmpty (x ,- xs)
+
+¬Empty&NonEmpty : ∀ {X} {xs : List X} → ¬ (Empty xs × NonEmpty xs)
+¬Empty&NonEmpty ([] , ())
+
+data Tsil (X : Set) : Set where
+  [] : Tsil X
+  _-,_ : Tsil X → X → Tsil X
+
+head : (xs : List X) → {{_ : NonEmpty xs}} → X
+head (x ,- xs) = x
+
+_><<_ : Tsil X → List X → List X
+[] ><< ys = ys
+(sx -, x) ><< ys = sx ><< (x ,- ys)
+
+_><>_ : Tsil X → List X → Tsil X
+sx ><> [] = sx
+sx ><> (x ,- xs) = (sx -, x) ><> xs
+
+record Zipper (X : Set) : Set where
+  constructor _,_
+  field
+    front : Tsil X
+    back : List X
+open Zipper
diff --git a/agda/Data/Nat/MoreProps.agda b/agda/Data/Nat/MoreProps.agda
index fbc42c1..5299f59 100644
--- a/agda/Data/Nat/MoreProps.agda
+++ b/agda/Data/Nat/MoreProps.agda
@@ -3,7 +3,15 @@ module Data.Nat.MoreProps where
 open import Algebra.Structures.Propositional
 open import Data.Nat
 open import Data.Nat.Properties
+open import Data.Product
 open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary
+
+data Zero : ℕ → Set where
+  instance zero : Zero zero
+
+¬Z&NZ : {n : ℕ} → ¬ (Zero n × NonZero n)
+¬Z&NZ (zero , ())
 
 ≤-stepL : ∀ {x y} → suc x ≤ y → x ≤ y
 ≤-stepL (s≤s z≤n) = z≤n
diff --git a/agda/Data/Vec/Snoc.agda b/agda/Data/Vec/Snoc.agda
new file mode 100644
index 0000000..1ee4aed
--- /dev/null
+++ b/agda/Data/Vec/Snoc.agda
@@ -0,0 +1,48 @@
+
+{-# OPTIONS --safe --cubical-compatible #-}
+
+-- Working with snoc lists.
+module Data.Vec.Snoc where
+open import Data.Product
+open import Data.Nat
+open import Data.Nat.Properties
+open import Data.List.Snoc using (List; Tsil; []; _,-_; _-,_)
+open import Relation.Nullary
+open import Relation.Binary.PropositionalEquality
+
+private variable
+  X : Set
+
+data Vec (X : Set) : ℕ → Set where
+  [] : Vec X 0
+  _,-_ : ∀ {n} → X → Vec X n → Vec X (suc n)
+
+data Cev (X : Set) : ℕ → Set where
+  [] : Cev X 0
+  _-,_ : ∀ {n} → Cev X n → X → Cev X (suc n)
+
+head : ∀ {n} → (xs : Vec X n) {{_ : NonZero n}} → X
+head (x ,- xs) = x
+
+_><<_ : ∀ {n m} → Cev X n → Vec X m → Vec X (n + m)
+[] ><< ys = ys
+_><<_ {n = suc n} {m} (sx -, x) ys rewrite sym (+-suc n m) = sx ><< (x ,- ys)
+
+_><>_ : ∀ {n m} → Cev X n → Vec X m → Cev X (n + m)
+_><>_ {n = n} sx [] rewrite +-identityʳ n = sx
+_><>_ {n = n} {suc m} sx (x ,- xs) rewrite (+-suc n m) = (sx -, x) ><> xs
+
+_<<<_ : ∀ {n m} → Vec X n → Vec X m → Vec X (n + m)
+_<<<_ [] ys = ys
+_<<<_ (x ,- xs) ys = x ,- (xs <<< ys)
+
+repeat : ∀ {n} → (k : ℕ) → Vec X n → Vec X (k * n)
+repeat zero xs = []
+repeat (suc k) xs = xs <<< repeat k xs
+
+-- record Zipper (X : Set) : Set where
+--   constructor _,_
+--   field
+--     front : Tsil X
+--     back : List X
+-- open Zipper
diff --git a/agda/Rational/Stream.agda b/agda/Rational/Stream.agda
index cfbbb00..e5cc087 100644
--- a/agda/Rational/Stream.agda
+++ b/agda/Rational/Stream.agda
@@ -1,11 +1,25 @@
-{-# OPTIONS --safe --guardedness #-}
+{-# OPTIONS --guardedness #-}
 module Rational.Stream where
 
+open import Data.Bool using (Bool; true; false)
 open import Data.Nat
+open import Data.Nat.Properties using (m*n≢0; +-comm)
+open import Data.Nat.MoreProps using (Zero; zero; ¬Z&NZ)
 open import Data.Fin as F using (Fin)
-open import Data.Maybe
+open import Data.Fin.MoreProps using (IsMax; fromℕ-ismax)
+open import Data.Maybe hiding (map)
+open import Data.Maybe.Relation.Unary.Any using (just)
+-- open import Data.Vec as V using (Vec; []; _∷_)
+-- open import Data.List.Snoc as L using (List)
+open import Data.Vec.Snoc as V hiding (head)
+
+open import Data.Product hiding (map)
 open import Data.Unit
+open import Data.Empty
+open import Relation.Nullary
 open import Relation.Binary.Isomorphism
+open import Relation.Binary.PropositionalEquality
+open import Function
 
 {-
 The idea is that rational fixpoints of containers (rational data types) are syntaxes with binding.
@@ -16,73 +30,228 @@ In the case of rational streams, they are lists where every cons is a binder, an
 we have a variable.
 -}
 
+private variable
+  X : Set
+
 -- The well-scoped de Bruijn version
-data RStream' (X : Set) (n : ℕ) : Set where
-  loop : Fin n → RStream' X n
-  cons : X → RStream' X (suc n) → RStream' X n
+data RStream (X : Set) (n : ℕ) : Set where
+  loop : Fin n → RStream X n
+  cons : X → RStream X (suc n) → RStream X n
 
-data IsCons {X : Set} {n : ℕ} : RStream' X n → Set where
+data IsCons {X : Set} {n : ℕ} : RStream X n → Set where
   instance cons : ∀ {x xs} → IsCons (cons x xs)
 
--- The richer contexts for the sublime scopes
+-- Telescopic contexts for sublimely scoped streams.
 data Ctx (X : Set) : ℕ → Set where
   [] : Ctx X 0
-  _-,_ : ∀ {n} → Ctx X n → (xs : RStream' X n) → {{_ : IsCons xs}} → Ctx X (suc n)
+  _-,_ : ∀ {n} → Ctx X n → (xs : RStream X n) → {{_ : IsCons xs}} → Ctx X (suc n)
 
--- Sublimely scoped RStreams
-mutual
-  data RStream {X : Set} {n : ℕ} (Γ : Ctx X n) : Set where
-    loop : Fin n → RStream Γ
-    cons : (x : X) → {xs' : RStream' X (suc n)} → (xs : RStream (Γ -, (cons x xs'))) → xs' ≈ xs → RStream Γ
+infixl 10 _-,_
 
-  data _≈_ {X : Set} {n : ℕ} {Γ : Ctx X n} : RStream' X n → RStream Γ → Set where
-    loop : ∀ {x} → loop x ≈ loop x
-    _∷_ : ∀ {x xs' xs} → (p : xs' ≈ xs) → (cons x xs') ≈ (cons x xs p)
+inject₁ : ∀ {X n} → RStream X n → RStream X (suc n)
+inject₁ (loop x) = loop (F.inject₁ x)
+inject₁ (cons x xs) = cons x (inject₁ xs)
 
--- We can annotate with fancy contexts
-WS→SS : ∀ {X n} → (Γ : Ctx X n) → RStream' X n → RStream Γ
-WS→SS Γ (loop x) = loop x
-WS→SS Γ (cons x xs) = cons x (WS→SS {!!} xs) {!!}
+lookup : ∀ {X n} (Γ : Ctx X n) → Fin n → RStream X n
+lookup (Γ -, xs) F.zero = inject₁ xs
+lookup (Γ -, xs) (F.suc x) = inject₁ (lookup Γ x)
 
--- We can forget the fancy contexts
-SS→WS : ∀ {X n} {Γ : Ctx X n} → RStream Γ → RStream' X n
-SS→WS (loop x) = loop x
-SS→WS (cons x {xs'} xs _) = cons x xs'
+inject₁-preserves-IsCons : ∀ {X n} {xs : RStream X n} → IsCons xs → IsCons (inject₁ xs)
+inject₁-preserves-IsCons cons = cons
 
--- And we get an isomorphism between the WS and SS versions
-iso : ∀ {X n} → (Γ : Ctx X n) → RStream' X n ≃ RStream Γ
-iso = {!!}
+lookup-IsCons : ∀ {X n} (Γ : Ctx X n) (x : Fin n) → IsCons (lookup Γ x)
+lookup-IsCons (Γ -, cons x xs) F.zero = cons
+lookup-IsCons (Γ -, cons x xs) (F.suc y) = inject₁-preserves-IsCons (lookup-IsCons Γ y)
 
-lookup : ∀ {X n} (Γ : Ctx X n) → Fin n → RStream' X n
-lookup Γ x = {!!}
+lookup-elem : ∀ {X n} (Γ : Ctx X n) → Fin n → X
+lookup-elem Γ x with lookup Γ x | lookup-IsCons Γ x
+... | cons y ys | cons = y
 
-lookup-iscons : ∀ {X n} (Γ : Ctx X n) → (x : Fin n) → IsCons (lookup Γ x)
-lookup-iscons = {!!}
+----------------------
+-- Ordinary streams --
+----------------------
 
--- Ordinary streams
 record Stream (X : Set) : Set where
   coinductive
   constructor _∷_
   field
     head : X
     tail : Stream X
+open Stream
 
--- We can unfold RStream to a Stream, so long as we leave in dummies where the variables were.
--- The termination checker gets cross otherwise :(
-unfold : ∀ {X n} {Γ : Ctx X n} → RStream Γ → Stream (Maybe X)
-Stream.head (unfold (loop x)) = nothing
-Stream.head (unfold (cons x xs p)) = just x
-Stream.tail (unfold {Γ = Γ} (loop x)) = unfold {Γ = Γ} (WS→SS _ (lookup Γ x))
-Stream.tail (unfold (cons x xs p)) = unfold xs
+-- P becomes true in finitely many steps.
+-- We want this to specifically point to nearest witness, hence the ¬ P head in the `there` case.
+data Eventually {X : Set} (P : X → Set) (xs : Stream X) : Set where
+  here  : P (head xs) → Eventually P xs
+  there : ¬ (P (head xs)) → Eventually P (tail xs) → Eventually P xs
+
+-- Predicate transformer for streams that extends a predicate P to be always true after every unfolding.
+record Always {X : Set} (P : Stream X → Set) (xs : Stream X) : Set where
+  coinductive
+  field
+    now     : P xs
+    forever : Always P (tail xs)
+open Always
 
+-- If we know something is Eventually true, we can look ahead to the next witness.
+next : {X : Set} {P : X → Set} {xs : Stream X} → Eventually P xs → X
+next {xs = xs} (here px) = head xs
+next {xs = xs} (there ¬px pxs) = next pxs
 
--- Liveness : given a (xs : Stream X) and a (P : X → Set), there's some upper bound (n : ℕ) such that we
--- can take always take fewer than n steps in xs to reach the next P x.
-Live : {X : Set} → (P : X → Set) → Stream X → Set
-Live P xs = {!!}
+next-IsP : {X : Set} {P : X → Set} {xs : Stream X} (pxs : Eventually P xs) → P (next pxs)
+next-IsP (here px) = px
+next-IsP (there ¬px pxs) = next-IsP pxs
 
+-- If we know that there are infinitely many P's, we can filter them out into a new stream.
+filter' : {X : Set} {P : X → Set} → {xs : Stream X} → (pxs : Always (Eventually P) xs) → Stream (Σ[ x ∈ X ] (P x))
+head (filter' pxs) = next (now pxs) , next-IsP (now pxs)
+tail (filter' pxs) = filter' (forever pxs)
+
+map : {X Y : Set} → (X → Y) → Stream X → Stream Y
+head (map f xs) = f (head xs)
+tail (map f xs) = map f (tail xs)
+
+filter : {X : Set} {P : X → Set} → {xs : Stream X} → Always (Eventually P) xs → Stream X
+filter = map proj₁ ∘ filter'
+
+---------------
+-- Unfolding --
+---------------
+
+-- We can unfold RStream to a Stream, so long as we leave in dummies where the variables were.
+-- The termination checker gets cross otherwise :(
+unfold' : ∀ {X n} → (Γ : Ctx X n) → RStream X n → Stream (Maybe X)
+head (unfold' Γ (loop x)) = nothing
+head (unfold' Γ (cons x xs)) = just x
+tail (unfold' Γ (loop x)) = unfold' Γ (lookup Γ x)
+tail (unfold' Γ (cons x xs)) = unfold' (Γ -, cons x xs) xs
 
 -- As long as we can guarantee that we're always
 -- only finitely many steps away from an X, we can remove all the 1's.
-remove-dummies : ∀ {X} → (xs : Stream (Maybe X)) → Live {!!} xs → Stream X
-remove-dummies = {!!}
+remove-dummies : ∀ {X} → {xs : Stream (Maybe X)} → Always (Eventually Is-just) xs → Stream X
+remove-dummies pxs = map (λ px → to-witness (proj₂ px)) (filter' pxs)
+
+unfold-lem : ∀ {X n} → (Γ : Ctx X n) (x : Fin n) → Is-just (head (unfold' Γ (lookup Γ x)))
+unfold-lem Γ x with lookup Γ x | lookup-IsCons Γ x
+... | .(cons _ _) | cons = just tt
+
+-- And unfolding in particular does always eventually produce an X.
+unfold-productive : ∀ {X n} → (Γ : Ctx X n) → (xs : RStream X n) → Always (Eventually Is-just) (unfold' Γ xs)
+now (unfold-productive Γ (loop x)) = there (λ ()) (here (unfold-lem Γ x))
+now (unfold-productive Γ (cons x xs)) = here (just tt)
+forever (unfold-productive Γ (loop x)) = unfold-productive _ _
+forever (unfold-productive Γ (cons x xs)) = unfold-productive _ _
+
+-- Put the pieces together to get the real unfolding
+unfold : ∀ {X n} → (Γ : Ctx X n) → RStream X n → Stream X
+unfold Γ xs = remove-dummies (unfold-productive Γ xs)
+
+-----------------------------------
+-- Bisimilarity and Bisimulation --
+-----------------------------------
+
+-- Pointwise lifting of a binary relation to streams (from stdlib)
+record Pointwise {X Y : Set} (_~_ : X → Y → Set) (xs : Stream X) (ys : Stream Y) : Set where
+  coinductive
+  field
+    head : head xs ~ head ys
+    tail : Pointwise _~_ (tail xs) (tail ys)
+
+-- Bisimilarity is the pointwise lifting of equality
+Bisimilar : ∀ {X} → Stream X → Stream X → Set
+Bisimilar xs ys = Pointwise _≡_ xs ys
+
+-- Bisimilarity of rational streams is bisimilarity of their unfoldings
+BisimilarR' : ∀ {X i j} → Ctx X i → RStream X i → Ctx X j → RStream X j → Set
+BisimilarR' Γ xs Δ ys = Bisimilar (unfold Γ xs) (unfold Δ ys)
+
+BisimilarR : ∀ {X} → RStream X 0 → RStream X 0 → Set
+BisimilarR xs ys = BisimilarR' [] xs [] ys
+
+
+
+-----------
+-- Loops --
+-----------
+
+-- An RStream is a loop if it loops back to the very start.
+-- NB: This is not preserved by weakening.
+IsLoop : {n : ℕ} → RStream X n → Set
+IsLoop (loop x) = IsMax x
+IsLoop (cons x l) = IsLoop l
+
+-- As long as we know how far we've come, and that we've made at least some progress by the time we reach the end,
+-- we can fold the list into a loop.
+loopify' : ∀ {c} → (n : ℕ) → (xs : Vec X c) → (Zero c → NonZero n) → RStream X n
+loopify' n [] p with p zero
+loopify' (suc n) [] p | n' = loop (F.fromℕ n)
+loopify' n (x ,- xs) p = cons x (loopify' (suc n) xs (const nonZero))
+
+loopify : ∀ {c} (xs : Vec X c) → {{_ : NonZero c}} → RStream X 0
+loopify xs {{nz}} = loopify' 0 xs (λ z → ⊥-elim (¬Z&NZ (z , nz)))
+
+loopify-isloop : ∀ {c} n (xs : Vec X c) p → IsLoop (loopify' n xs p)
+loopify-isloop n [] p with p zero
+loopify-isloop (suc n) [] p | n' = fromℕ-ismax n
+loopify-isloop n (x ,- xs) p = loopify-isloop (suc n) xs _
+
+
+
+-------------------------
+-- Algebraic Structure --
+-------------------------
+
+-- Two operations: unrolling, and loosening.
+-- If two RStreams can be equalised by applications of these, then they
+-- represent the same stream (ie, are bisimilar).
+
+
+-- first, a definition on vectors.
+-- And they all rolled over and one fell out...
+rotate : ∀ {n} → Vec X n → Vec X n
+rotate [] = []
+rotate {n = suc n} (x ,- xs) rewrite +-comm 1 n = xs <<< (x ,- [])
+
+extend : ∀ {p n} → Cev X p → RStream X n → RStream X n
+extend = {!!}
+
+-- We can view an RStream as a "lasso" - a finite prefix, and a nonempty looping section.
+-- The explicit separation removes the need for a variable
+record Lasso (X : Set) (|prefix| : ℕ) (|cycle| : ℕ) {{_ : NonZero |cycle|}} : Set where
+  constructor _-∘_
+  field
+    prefix : Cev X |prefix|
+    cycle  : Vec X |cycle|
+
+  unroll : Lasso X (suc |prefix|) |cycle|
+  prefix unroll = prefix -, V.head cycle
+  cycle unroll = rotate cycle
+
+  loosen : (k : ℕ) {{_ : NonZero k}} → Lasso X |prefix| (k * |cycle|) {{m*n≢0 _ _}}
+  prefix (loosen k) = prefix
+  cycle (loosen k) = repeat k cycle
+
+  toRStream : RStream X 0
+  toRStream = extend prefix (loopify cycle)
+
+open Lasso
+
+
+
+-- split rstream intp prefix and loop, for which the other view of RStreams would be *lovely*
+toLasso : ∀ {X n p c} {{_ : NonZero c}} →  RStream X n → Lasso X p c
+toLasso = {!!}
+
+
+
+--------------------------------------
+-- Proof that sqrt(2) is Irrational --
+--------------------------------------
+
+Digit = Fin 10
+
+-- The unit interval of real numbers [0,1].
+-- The stream contains the digits right of the decimal point.
+I = Stream Digit
+
+