implementing 𝟙-induction

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

agda-experiments/MLTT/Universes.agda

@@ -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 _̇
-

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 _̇

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
+