From f809bde68d5124120d91f3f69aa1e862ce85477f Mon Sep 17 00:00:00 2001
From: Felix Dilke <felix.dilke@obsidian.systems>
Date: Mon, 12 Jan 2026 15:22:32 +0000
Subject: [PATCH] additional files

---
 agda-experiments/MLTT/Universes.agda       | 27 ++++++++++++++++++++++
 agda-experiments/about-agda-experiments.md | 27 ++++++++++++++++++++++
 2 files changed, 54 insertions(+)
 create mode 100644 agda-experiments/MLTT/Universes.agda
 create mode 100644 agda-experiments/about-agda-experiments.md

diff --git a/agda-experiments/MLTT/Universes.agda b/agda-experiments/MLTT/Universes.agda
new file mode 100644
index 0000000..cc20f00
--- /dev/null
+++ b/agda-experiments/MLTT/Universes.agda
@@ -0,0 +1,27 @@
+{-# OPTIONS --safe --without-K #-}
+
+module MLTT.Universes where
+
+open import Agda.Primitive public
+  using (_⊔_)
+  renaming (lzero to 𝓤₀
+          ; lsuc to _⁺
+          ; Level to Universe
+          ; Setω to 𝓤ω
+          )
+
+variable
+ 𝓤 𝓥 𝓦 𝓣 𝓤' 𝓥' 𝓦' 𝓣' : Universe
+
+
+_̇ : (𝓤 : Universe) → Set (𝓤 ⁺)
+𝓤 ̇ = Set 𝓤
+
+𝓤₁ = 𝓤₀ ⁺
+𝓤₂ = 𝓤₁ ⁺
+
+_⁺⁺ : Universe → Universe
+𝓤 ⁺⁺ = 𝓤 ⁺ ⁺
+
+infix  1 _̇
+
diff --git a/agda-experiments/about-agda-experiments.md b/agda-experiments/about-agda-experiments.md
new file mode 100644
index 0000000..e3db9ff
--- /dev/null
+++ b/agda-experiments/about-agda-experiments.md
@@ -0,0 +1,27 @@
+# Installing Agda
+
+I added these lines to my configuration.nixos to get a workable Agda installation:
+
+  (agda.withPackages (p: [ p.standard-library ]))
+
+but there were a few issues, so I removed that and installed with
+    cabal update
+    cabal install Agda
+which seemed to work nicely after some hackery with zlib, and installing the standard libraries.
+
+# Owen's Geolog definitions
+
+Owen.agda : Definitions fom Owen's first two lectures about Geolog.
+
+These set up the basic machinery for contexts (signatures), theories and interpolation.
+
+Compile with:
+  agda -c --no-main Owen.agda
+
+# HoTT definitions from Martin Escardo's book "Univalent Foundations" https://arxiv.org/pdf/1911.00580 
+
+  agda -c --no-main MLTT/Universe.agda
+
+Escardo defines everything from the ground up with his own concepts of sets, universes etc.,
+independently of the standard library.
+