diff --git a/examples/misc.quox b/examples/misc.quox
new file mode 100644
index 0000000..4d540f1
--- /dev/null
+++ b/examples/misc.quox
@@ -0,0 +1,25 @@
+
+def0 Pred : 0.★₀ → ★₁ = λ A ⇒ 0.A → ★₀;
+
+def0 All : 0.(A : ★₀) → 0.(Pred A) → ★₁ =
+  λ A P ⇒ 1.(x : A) → P x;
+
+defω cong :
+    0.(A : ★₀) → 0.(P : Pred A) →
+    1.(p : All A P) →
+    0.(x : A) → 0.(y : A) → 1.(xy : x ≡ y : A) →
+    Eq [i ⇒ P (xy @i)] (p x) (p y) =
+  λ A P p x y xy ⇒ δ i ⇒ p (xy @i);
+
+def0 eq-f :
+    0.(A : ★₀) → 0.(P : Pred A) →
+    0.(p : All A P) → 0.(q : All A P) →
+    0.A → ★₀ =
+  λ A P p q x ⇒ p x ≡ q x : P x;
+
+defω funext :
+    0.(A : ★₀) → 0.(P : Pred A) →
+    0.(p : All A P) → 0.(q : All A P) →
+    1.(All A (eq-f A P p q)) →
+    p ≡ q : All A P =
+  λ A P p q eq ⇒ δ i ⇒ λ x ⇒ eq x @i;