diff --git a/ahmed/LogicalRelations.agda b/ahmed/LogicalRelations.agda
deleted file mode 100644
index 8edd0be..0000000
--- a/ahmed/LogicalRelations.agda
+++ /dev/null
@@ -1,78 +0,0 @@
-module Ahmed.LogicalRelations where
-
-open import Data.Empty
-open import Data.Unit
-open import Data.Bool
-open import Data.Nat
-open import Data.Fin
-open import Data.Product
-open import Relation.Nullary using (Dec; yes; no)
-
-data type : Set where
-  bool : type
-  _-→_ : type → type → type
-
-data ctx : Set where
-  nil : ctx
-  _,_ : ctx → type → ctx
-
-data var : ctx → type → Set where
-  zero : ∀ {Γ τ} → var (Γ , τ) τ
-  suc : ∀ {Γ τ₁ τ₂} → var Γ τ₂ → var (Γ , τ₁) τ₂
-
-data term : ctx → type → Set where
-  true : ∀ {Γ} → term Γ bool
-  false : ∀ {Γ} → term Γ bool
-  `_ : ∀ {Γ τ} → var Γ τ → term Γ τ
-  λ[_]_ : ∀ {Γ τ₂} → (τ₁ : type) → (e : term (Γ , τ₁) τ₂) → term Γ (τ₁ -→ τ₂)
-  _∙_ : ∀ {Γ τ₁ τ₂} → term Γ (τ₁ -→ τ₂) → term Γ τ₁ → term Γ τ₂
-
-length : ctx → ℕ
-length nil = zero
-length (ctx , _) = suc (length ctx)
-
-extend : ∀ {Γ Δ}
-  → (∀ {τ} → var Γ τ → var Δ τ)
-  → (∀ {τ₁ τ₂} → var (Γ , τ₂) τ₁ → var (Δ , τ₂) τ₁)
-extend ρ zero = zero
-extend ρ (suc c) = suc (ρ c)
-
-rename : ∀ {Γ Δ}
-  → (∀ {τ} → var Γ τ → var Δ τ)
-  → (∀ {τ} → term Γ τ → term Δ τ)
-rename ρ true = true
-rename ρ false = false
-rename ρ (` x) = ` (ρ x)
-rename ρ (λ[ τ₁ ] c) = λ[ τ₁ ] rename (extend ρ) c
-rename ρ (c ∙ c₁) = rename ρ c ∙ rename ρ c₁
-
-extends : ∀ {Γ Δ}
-  → (∀ {τ} → var Γ τ → term Δ τ)
-  → (∀ {τ₁ τ₂} → var (Γ , τ₂) τ₁ → term (Δ , τ₂) τ₁)
-extends σ zero = ` zero
-extends σ (suc x) = rename suc (σ x)
-
-subst : ∀ {Γ Δ}
-  → (∀ {τ} → var Γ τ → term Δ τ)
-  → (∀ {τ} → term Γ τ → term Δ τ)
-subst ρ true = true
-subst ρ false = false
-subst ρ (` x) = ρ x
-subst ρ (λ[ τ₁ ] x) = λ[ τ₁ ] subst (extends ρ) x
-subst ρ (x ∙ x₁) = subst ρ x ∙ subst ρ x₁
-
-_[_] : ∀ {Γ τ₁ τ₂} → term (Γ , τ₂) τ₁ → term Γ τ₂ → term Γ τ₁
-_[_] {Γ} {τ₁} {τ₂} e e₁ = subst σ e
-  where
-    σ : ∀ {τ} → var (Γ , τ₂) τ → term Γ τ 
-    σ zero = e₁
-    σ (suc x) = ` x
-
-data value : ∀ {Γ τ} → term Γ τ → Set where
-  true : ∀ {Γ} → value {Γ} true
-  false : ∀ {Γ} → value {Γ} false
-  λ[_]_ : ∀ {Γ τ₁ τ₂} {e : term (Γ , τ₁) τ₂} → value (λ[ τ₁ ] e)
-
-data step : ∀ {Γ τ} → term Γ τ → term Γ τ → Set where 
-  β-λ : ∀ {Γ τ₁ τ₂ v} → (e : term (Γ , τ₁) τ₂) → value v
-    → step ((λ[ τ₁ ] e) ∙ v) (e [ v ])
\ No newline at end of file
diff --git a/ahmed/day1.agda b/ahmed/day1.agda
index 4a3e281..60712c7 100644
--- a/ahmed/day1.agda
+++ b/ahmed/day1.agda
@@ -1,4 +1,3 @@
-{-# OPTIONS --prop #-}
 module Ahmed.Day1 where
 
 open import Agda.Builtin.Sigma
diff --git a/ahmed/day1.fst b/ahmed/day1.fst
deleted file mode 100644
index e6faa42..0000000
--- a/ahmed/day1.fst
+++ /dev/null
@@ -1,77 +0,0 @@
-module Day1
-
-let var = int
-
-type ty =
-  | TyBool
-  | TyArrow of ty * ty
-
-type term =
-  | EVar of int
-  | ETrue
-  | EFalse
-  | EIfThenElse of term * term * term
-  | ELambda of ty * term
-  | EApp of term * term
-
-type value =
-  | VTrue
-  | VFalse
-  | VLambda of ty * term
-
-type evalctx =
-  | ECDot
-  | ECIfThenElse of evalctx * term * term
-  | ECAppL of evalctx * term
-  | ECAppR of value * evalctx
-
-type step : term -> term -> Type =
-  | StepIfTrue : (e1 : term) -> (e2 : term) -> step (EIfThenElse (ETrue, e1, e2)) e1
-  | StepIfFalse : (e1 : term) -> (e2 : term) -> step (EIfThenElse (EFalse, e1, e2)) e2
-
-let ctx = var -> option ty
-let empty : ctx = fun _ -> None
-let extend (t : ty) (g : ctx) : ctx = fun y -> if y = 0 then Some t else g (y - 1)
-
-noeq type typing : ctx -> term -> ty -> Type =
-  | TypeTrue : (ctx : ctx) -> typing ctx ETrue TyBool
-  | TypeFalse : (ctx : ctx) -> typing ctx EFalse TyBool
-  | TypeIfThenElse : (ctx : ctx) -> (ty : ty)
-    -> (c : term) -> (e1 : term) -> (e2 : term)
-    -> typing ctx c TyBool
-    -> typing ctx e1 ty -> typing ctx e2 ty
-    -> typing ctx (EIfThenElse (c, e1, e2)) ty
-
-let vRelation (ty : ty) (term : term) : prop =
-  match ty, term with
-  | (TyBool, ETrue) -> True
-  | (TyBool, EFalse) -> True
-  | _ -> False
-
-let irred (term : term) : prop = admit()
-
-let rec stepsToInNSteps (e1 : term) (e2 : term) (n : nat) : prop =
-  if n = 0 then False
-  else exists e' . (stepsToInNSteps e' e2 (n - 1) /\ (step e1 e'))
-
-// let stepsTo (e1 : term) (e2 : term) : prop =
-
-
-let eRelation (ty : ty) (term : term) : prop =
-  exists e' . irred e' /\ vRelation ty e'
-
-let goodRelation (g : ctx) =
-  admit()
-
-let subst (#ctx:ctx) (g : goodRelation ctx) (term : term) =
-  admit()
-
-// let typeSoundness (ctx : ctx) (term : term) (ty : ty) : prop =
-//   forall (e' : )
-
-let semanticSoundness (ctx : ctx) (term : term) (ty : ty) : prop =
-  forall (y : goodRelation ctx) . eRelation ty (subst y term)
-
-let fundamentalProperty (#ctx : ctx) (#term : term) (#ty : ty)
-  (_ : typing ctx term ty) : semanticSoundness ctx term ty =
-  admit()
\ No newline at end of file
diff --git a/ahmed/day2.agda b/ahmed/day2.agda
new file mode 100644
index 0000000..a45a22f
--- /dev/null
+++ b/ahmed/day2.agda
@@ -0,0 +1,135 @@
+module Ahmed.Day2 where
+
+open import Agda.Builtin.Sigma
+open import Data.Bool
+open import Data.Empty
+open import Data.Fin hiding (fold)
+open import Data.Maybe
+open import Data.Nat
+open import Data.Product
+open import Data.Sum
+open import Relation.Nullary
+
+id : {A : Set} → A → A
+id {A} x = x
+
+data type : Set where
+  unit : type
+  bool : type
+  _-→_ : type → type → type
+  `_ : ℕ → type
+  μ_ : type → type
+
+data term : Set where
+  `_ : ℕ → term
+  `true : term
+  `false : term
+  `if_then_else_ : term → term → term → term
+  `λ[_]_ : (τ : type) → (e : term) → term
+  _∙_ : term → term → term
+  `fold : term → term
+  `unfold : term → term
+
+data ctx : Set where
+  nil : ctx
+  cons : ctx → type → ctx
+
+lookup : ctx → ℕ → Maybe type
+lookup nil _ = nothing
+lookup (cons ctx₁ x) zero = just x 
+lookup (cons ctx₁ x) (suc n) = lookup ctx₁ n
+
+data type-sub : Set where
+  nil : type-sub
+
+type-subst : type → type → type
+type-subst unit v = unit
+type-subst bool v = bool
+type-subst (τ -→ τ₁) v = (type-subst τ v) -→ (type-subst τ₁ v)
+type-subst (` zero) v = v
+type-subst (` suc x) v = ` x
+type-subst (μ τ) v = μ (type-subst τ v)
+
+data sub : Set where
+  nil : sub
+  cons : sub → term → sub
+
+subst : term → term → term
+subst (` zero) v = v
+subst (` suc x) v = ` x
+subst `true v = `true
+subst `false v = `false
+subst (`if x then x₁ else x₂) v = `if (subst x v) then (subst x₁ v) else (subst x₂ v)
+subst (`λ[ τ ] x) v = `λ[ τ ] subst x v
+subst (x ∙ x₁) v = (subst x v) ∙ (subst x₁ v)
+subst (`fold x) v = `fold (subst x v)
+subst (`unfold x) v = `unfold (subst x v)
+
+data value-rel : type → term → Set where 
+  v-`true : value-rel bool `true
+  v-`false : value-rel bool `false
+  v-`λ[_]_ : ∀ {τ e} → value-rel τ (`λ[ τ ] e)
+  v-`fold : ∀ {τ e} → value-rel (type-subst τ (μ τ)) e → value-rel (μ τ) (`fold e)
+
+data good-subst : ctx → sub → Set where
+  nil : good-subst nil nil
+  cons : ∀ {ctx τ γ v}
+    → good-subst ctx γ
+    → value-rel τ v
+    → good-subst (cons ctx τ) γ
+
+data step : term → term → Set where
+  step-if-1 : ∀ {e₁ e₂} → step (`if `true then e₁ else e₂) e₁
+  step-if-2 : ∀ {e₁ e₂} → step (`if `false then e₁ else e₂) e₂
+  step-`λ : ∀ {τ e v} → step ((`λ[ τ ] e) ∙ v) (subst e v)
+  step-`fold : ∀ {v} → step (`unfold (`fold v)) v
+
+data steps : ℕ → term → term → Set where
+  zero : ∀ {e} → steps zero e e
+  suc : ∀ {e e' e''} → (n : ℕ) → step e e' → steps n e' e'' → steps (suc n) e e''
+
+data _⊢_∶_ : ctx → term → type → Set where
+  type-`true : ∀ {ctx} → ctx ⊢ `true ∶ bool
+  type-`false : ∀ {ctx} → ctx ⊢ `false ∶ bool
+  type-`ifthenelse : ∀ {ctx e e₁ e₂ τ}
+    → ctx ⊢ e ∶ bool
+    → ctx ⊢ e₁ ∶ τ
+    → ctx ⊢ e₂ ∶ τ
+    → ctx ⊢ (`if e then e₁ else e₂) ∶ τ
+  type-`x : ∀ {ctx x}
+    → (p : Is-just (lookup ctx x))
+    → ctx ⊢ (` x) ∶ (to-witness p)
+  type-`λ : ∀ {ctx τ τ₂ e}
+    → (cons ctx τ) ⊢ e ∶ τ₂
+    → ctx ⊢ (`λ[ τ ] e) ∶ (τ -→ τ₂)
+  type-∙ : ∀ {ctx τ₁ τ₂ e₁ e₂}
+    → ctx ⊢ e₁ ∶ (τ₁ -→ τ₂)
+    → ctx ⊢ e₂ ∶ τ₂
+    → ctx ⊢ (e₁ ∙ e₂) ∶ τ₂
+
+  type-`fold : ∀ {ctx τ e}
+    → ctx ⊢ e ∶ (type-subst τ (μ τ))
+    → ctx ⊢ (`fold e) ∶ (μ τ)
+  type-`unfold : ∀ {ctx τ e}
+    → ctx ⊢ e ∶ (μ τ)
+    → ctx ⊢ (`unfold e) ∶ (type-subst τ (μ τ))
+
+irreducible : term → Set
+irreducible e = ¬ (∃ λ e' → step e e')
+
+data term-relation : type → term → Set where
+  e-term : ∀ {τ e}
+    → (∀ {n} → (e' : term) → steps n e e' → irreducible e' → value-rel τ e')
+    → term-relation τ e
+
+type-sound : ∀ {Γ e τ} → Γ ⊢ e ∶ τ → Set
+type-sound {Γ} {e} {τ} s = ∀ {n} → (e' : term) → steps n e e' → value-rel τ e' ⊎ ∃ λ e'' → step e' e''
+
+_⊨_∶_ : (Γ : ctx) → (e : term) → (τ : type) → Set
+_⊨_∶_ Γ e τ = (γ : sub) → (good-subst Γ γ) → term-relation τ e
+
+fundamental : ∀ {Γ e τ} → (well-typed : Γ ⊢ e ∶ τ) → type-sound well-typed → Γ ⊨ e ∶ τ
+fundamental {Γ} {e} {τ} well-typed type-sound γ good-sub = e-term f
+  where
+    f : {n : ℕ} (e' : term) → steps n e e' → irreducible e' → value-rel τ e'
+    f e' steps irred = [ id , (λ exists → ⊥-elim (irred exists)) ] (type-sound e' steps)
diff --git a/chong/notes.typ b/chong/notes.typ
index f14d030..9ab53ee 100644
--- a/chong/notes.typ
+++ b/chong/notes.typ
@@ -2,3 +2,46 @@
 #import "@preview/prooftrees:0.1.0": *
 #show: doc => conf("Language-Based Security", doc)
 
+Security labels
+
+Flow relations
+
+- If $l_1 subset.sq.eq l_2$ then information is allowed to flow from $l_1$ to $l_2$
+  - This should be reflexive and transitive
+  - *NOT* be symmetric
+  - This is known as a _pre-order_
+  - We may also want to add anti-symmetry, which makes it a _partial order_
+
+- Actually, we could use a join-semi-lattice. (Denning 1978)
+  - _Unique_ least upper bound operation
+  - If we didn't have least upper bound, then $c = a plus.circle b ; d_1 = c; d_2 = c$ may not work
+
+More general form of non-interference:
+
+- Lattice $(Lambda, subset.sq.eq)$ of security levels
+- Using this, Program $c$ is non-interfering if:
+  - $forall sigma_1, sigma_2, sigma'_1, sigma'_2, l in Lambda => \
+  "if" sigma_1 op(=)_l sigma_2 "and" angle.l c, sigma_1 angle.r arrow.b.double sigma'_1 "and" angle.l c, sigma_2 angle.r arrow.b.double sigma'_2 \
+  "then" sigma'_1 op(=)_l sigma'_2$
+
+=== Threat model
+
+Information channels convey information
+
+Categorized into (Lampson 1973)
+
+- Legitimate channels
+- Covert channels (and side channels)
+
+=== Interaction
+
+Adding to IMP:
+
+$
+x := ... | "input from" l | "output" x "to" l \
+"Trace" in.rev tau ::= epsilon | tau dot "in"(n, l) | tau dot "out"(n, l)
+$
+
+Trace is a sequence of events
+
+New non-interference, based on traces. The execution trace needs to be the same!
\ No newline at end of file
diff --git a/experiments/tc.agda b/experiments/tc.agda
new file mode 100644
index 0000000..a0e180c
--- /dev/null
+++ b/experiments/tc.agda
@@ -0,0 +1,2 @@
+module Experiments.Tc where
+
diff --git a/holtzen/notes.typ b/holtzen/notes.typ
index bfb1923..9ce465d 100644
--- a/holtzen/notes.typ
+++ b/holtzen/notes.typ
@@ -135,4 +135,64 @@ _Answer._ Any time you add a syntactic construct, it comes at a price.
 
 - Stan https://en.wikipedia.org/wiki/Stan_(software)
 - https://www.tensorflow.org/probability Google
-- https://pyro.ai/ Uber
\ No newline at end of file
+- https://pyro.ai/ Uber
+
+=== Tiny Cond
+
+Observe, can prune worlds that can't happen.
+
+Un-normalized semantics where the probabilities of things don't sum to 1.
+
+#let observe = "observe"
+
+$ db(observe p \; e) (rho) (v) = cases(
+  db(e) (rho) (v) "if" db(p) (rho) = tt,
+  0 "else",
+) $
+
+To normalize, divide by the sum
+
+$ db(e)(rho)(v) = frac(db(e) (rho) (v), db(e) (rho) (tt) + db(e) (rho) (ff)) $
+
+== Operational sampling semantics
+
+Expectation of a random variable, $EE$
+
+$ EE_Pr[f] = sum^N_w Pr(w) times f(w) \
+approx 1/N sum^N_(w tilde Pr) f(w)
+$
+
+Approximate with a finite sample, where $w$ ranges over the sample
+
+To prove our runtime strategy sound, we're going to relate it to an _expectation_.
+
+https://en.wikipedia.org/wiki/Concentration_inequality
+
+=== Big step semantics
+
+#let bigstep(sigma, e, v) = $#sigma tack.r #e arrow.b.double #v$
+
+$ sigma tack.r angle.l e . rho angle.r arrow.b.double v $
+
+$tack.r$ read as "in the context of"
+
+We externalized the randomness and put it all in $sigma$
+
+This is like pattern matching:
+
+$ v :: bigstep(sigma, flip 1/2, v )$
+
+== Lecture 3
+
+=== Rejection sampling
+
+=== Search
+
+$x <- flip 1/2 \
+y <- ifthenelse(x, flip 1/3, flip 1/4) \
+z <- ifthenelse(y, flip 1/6, flip 1/7) \
+ret z$
+
+You can draw a search tree of probabilities. Add up the probabilities to get the probability that a program returns a specific value.
+
+You can share $z$ since it doesn't depend directly on $x$. This builds a *binary decision diagram*.
\ No newline at end of file
diff --git a/zdancewic/monads.agda b/zdancewic/monads.agda
new file mode 100644
index 0000000..e8d2b5a
--- /dev/null
+++ b/zdancewic/monads.agda
@@ -0,0 +1,15 @@
+{-# OPTIONS --guardedness #-}
+{-# OPTIONS --type-in-type #-}
+
+module Zdancewic.Monads where
+
+open import Agda.Primitive
+open import Data.Nat
+
+record ITree (E : Set → Set) (R : Set) : Set where
+  coinductive
+  field
+    ret : R
+    tau : ITree E R
+    vis : ∀ {A} → (e : E A) → (A → ITree E R)
+