From f5b0c2b7c3ea55377885fedc7c0ba2c493bb7add Mon Sep 17 00:00:00 2001
From: Felix Dilke <felix.dilke@obsidian.systems>
Date: Mon, 12 Jan 2026 18:01:36 +0000
Subject: [PATCH] =?UTF-8?q?implementing=20=F0=9D=9F=99-induction?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 agda-experiments/HoTT-UF-Agda.agda         | 28 ++++++++++++++++++++
 agda-experiments/MLTT/Universes.agda       | 27 -------------------
 agda-experiments/Universes.agda            | 30 ++++++++++++++++++++++
 agda-experiments/about-agda-experiments.md |  4 +++
 4 files changed, 62 insertions(+), 27 deletions(-)
 create mode 100644 agda-experiments/HoTT-UF-Agda.agda
 delete mode 100644 agda-experiments/MLTT/Universes.agda
 create mode 100644 agda-experiments/Universes.agda

diff --git a/agda-experiments/HoTT-UF-Agda.agda b/agda-experiments/HoTT-UF-Agda.agda
new file mode 100644
index 0000000..5c3d886
--- /dev/null
+++ b/agda-experiments/HoTT-UF-Agda.agda
@@ -0,0 +1,28 @@
+{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}
+
+module HoTT-UF-Agda where
+  open import Universes public
+
+  -- variable
+  --   𝓤 𝓥 𝓦 𝓣 : Universe
+
+  -- data 𝟙 : 𝓤₀ ̇ where
+  --   ⋆ : 𝟙
+
+  -- 𝟙-induction : (A : 𝟙 → 𝓤̇  ) → A ⋆ → (x : 𝟙) → A x
+  --   𝟙-induction A a ⋆ = a
+
+  -- 𝟙-induction : (A : 𝟙 → 𝓤 ̇) → A ⋆ → (x : 𝟙) → A x
+  --   𝟙-induction A a ⋆ = a
+
+  -- 𝟙-induction : (A : 𝟙 → 𝓤 ̇) → A ⋆ → (x : 𝟙) → A x
+  --   𝟙-induction A a ⋆ = a
+
+  variable
+    𝓤 𝓥 𝓦 𝓣 : Universe
+
+  data 𝟙 : 𝓤₀ ̇  where
+    ⋆ : 𝟙
+
+  𝟙-induction : (A : 𝟙 → 𝓤 ̇ ) → A ⋆ → (x : 𝟙) → A x
+  𝟙-induction A a ⋆ = a
\ No newline at end of file
diff --git a/agda-experiments/MLTT/Universes.agda b/agda-experiments/MLTT/Universes.agda
deleted file mode 100644
index cc20f00..0000000
--- a/agda-experiments/MLTT/Universes.agda
+++ /dev/null
@@ -1,27 +0,0 @@
-{-# 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/Universes.agda b/agda-experiments/Universes.agda
new file mode 100644
index 0000000..4babafd
--- /dev/null
+++ b/agda-experiments/Universes.agda
@@ -0,0 +1,30 @@
+{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}
+
+module Universes where
+
+open import Agda.Primitive public
+ renaming (
+            Level to Universe -- We speak of universes rather than of levels.
+          ; lzero to 𝓤₀       -- Our first universe is called 𝓤₀
+          ; lsuc to _⁺        -- The universe after 𝓤 is 𝓤 ⁺
+          ; Setω to 𝓤ω        -- There is a universe 𝓤ω strictly above 𝓤₀, 𝓤₁, ⋯ , 𝓤ₙ, ⋯
+          )
+ using    (_⊔_)               -- Least upper bound of two universes, e.g. 𝓤₀ ⊔ 𝓤₁ is 𝓤₁
+
+Type = λ ℓ → Set ℓ
+
+_̇   : (𝓤 : Universe) → Type (𝓤 ⁺)
+
+𝓤 ̇  = Type 𝓤
+
+𝓤₁ = 𝓤₀ ⁺
+𝓤₂ = 𝓤₁ ⁺
+𝓤₃ = 𝓤₂ ⁺
+
+_⁺⁺ : Universe → Universe
+𝓤 ⁺⁺ = 𝓤 ⁺ ⁺
+
+universe-of : {𝓤 : Universe} (X : 𝓤 ̇ ) → Universe
+universe-of {𝓤} X = 𝓤
+
+infix  1 _̇
diff --git a/agda-experiments/about-agda-experiments.md b/agda-experiments/about-agda-experiments.md
index e3db9ff..a875120 100644
--- a/agda-experiments/about-agda-experiments.md
+++ b/agda-experiments/about-agda-experiments.md
@@ -25,3 +25,7 @@ Compile with:
 Escardo defines everything from the ground up with his own concepts of sets, universes etc.,
 independently of the standard library.
 
+Got as far as the definition of 𝟙-induction for a single-valued type 𝟙.
+The sources (in more consistent versions than in the notes) are here:
+https://github.com/martinescardo/HoTT-UF-Agda-Lecture-Notes
+