@@ -3,101 +3,202 @@ include ../../header
33html
44 head
55 meta( property ='og:title' content ='UNIVERSE' )
6- meta( property ='og:description' content ='Type Universes and Prop ' )
7- meta( property ='og:url' content ='https://laurent .groupoid.space/foundations/universe/' )
6+ meta( property ='og:description' content ='Fibrational Universes and Cubical Interval Pretypes for Homotopy Type Theory ' )
7+ meta( property ='og:url' content ='https://urs .groupoid.space/foundations/universe/' )
88
99block title
1010 title UNIVERSE
1111
1212block content
1313 nav
14- <a href =' ../../index.html' LAURENT </a >
14+ <a href =' ../../index.html' URS </a >
1515 <a href =' #' a >
1616 article.main
1717 .exe
1818 section
19- h1 TYPE UNIVERSES
19+ h1 FIBRATIONAL UNIVERSES AND CUBICAL PRETYPES
2020 span.
2121 aside
22- time Published: 21 MAR 2025
22+ time Published: 14 APR 2025
2323 .exe
2424 section
2525 + tex.
26- The type system employs a limited hierarchy of universes, $U_0 : U_1$,
27- alongside $\text{Prop}$, to manage types and propositions. This structure balances
28- expressiveness with simplicity, drawing analogies to Coq and Lean while serving
29- Schwartz’s analysis framework.
26+ The $\mathbf{U}_n$ type represents a fibrational universe hierarchy indexed by
27+ levels $n : \mathbb{N}$, supporting type formation and cumulativity in a predicative
28+ setting, following Cubical Agda. The $\mathbf{V}_n$ type represents cubical
29+ interval pretypes, indexed by $n : \mathbb{N}$, used to model cubical intervals
30+ for path types and glue types in homotopy type theory.
3031 + tex.
31- $U_0$ contains small types (e.g. , $\mathbb{R}$, $\text{Set}(A)$), while $U_1$
32- classifies $U_0$ and higher constructs (e.g., $\text{Power}(A)$). $\text{Prop}$
33- is a distinct universe for 0-truncated propositions, supporting classical logic .
32+ In Urs , $\mathbf{U}_n$ and $\mathbf{V}_n$ provide the foundational type hierarchies for homotopy groups,
33+ supporting path types in $\mathbf{Path}$, glue types
34+ in $\mathbf{Glue}$, and enabling higher structures in $\mathbf{SupSmthSet}$ .
3435
3536 h2 Formation
3637 + tex.
37- $\mathbf{Definition\ 1.2.1}$ (Universe Hierarchy). The system defines two universes:
38- $U_0$, the type of small types, and $U_1$, the type of $U_0$, with $\text{Prop}$ as
39- a separate propositional universe.
38+ $\mathbf{Definition\ 1.1.1}$ (Fibrational Universe Formation). The universe
39+ $\mathbf{U}_n$ is a type indexed by $n : \mathbb{N}$, containing types at level $n$.
4040 + tex(true ).
4141 $$
42- U_0 : U_1, \quad \text{Prop} : U_0.
42+ \mathbf{U} : \mathbb{N} \to \mathbf{Type},
4343 $$
44- + code.
45- type exp =
46- | Univrse i (* i in [0,1] *)
47- | Prop
44+ $$
45+ \mathbf{U}_n : \mathbf{Type} \equiv \mathbf{U}\ n.
46+ $$
47+ + code('urs' ).
48+ def U (n : Nat) : Type := Universe n -- Universe formation
49+ def U₀ : Type := U 0 -- Level 0 universe
50+ def U₁ : Type := U 1 -- Level 1 universe
51+ (* Fibrational universe formation *)
4852
49- h2 Nuances of U<sub >0</sub > : U<sub >1</sub >
5053 + tex.
51- $U_0$ includes base types like $\mathbb{N}$, $\mathbb{R}$, and $\text{Set}(\mathbb{R})$,
52- sufficient for most analysis constructs. $U_1$ enables higher types like
53- $\text{Power}(\mathbb{R})$ or $\text{Measure}(A, \Sigma)$, but the hierarchy stops
54- here to avoid Russell-style paradoxes and maintain decidability.
54+ $\mathbf{Definition\ 1.1.2}$ (Cubical Interval Pretype Formation). The cubical
55+ interval pretype $\mathbf{V}_n$ is a pretype indexed by $n : \mathbb{N}$, used to
56+ model cubical intervals with dimension $n$ for path types and glue types.
5557 + tex(true ).
5658 $$
57- \mathbb{R } : U_0, \quad \text{Set}(\ mathbb{R}) : U_0, \quad \mathcal{P}(\mathbb{R}) : U_1.
59+ \mathbf{V } : \ mathbb{N} \to \mathbf{PreType},
5860 $$
59- + tex.
60- Unlike Coq’s cumulative $U_i : U_{i+1}$ or Lean’s infinite hierarchy, this limited
61- $U_0 : U_1$ avoids universe polymorphism, simplifying type checking while limiting
62- higher inductive types or complex type families.
61+ $$
62+ \mathbf{V}_n : \mathbf{PreType} \equiv \mathbf{V}\ n,
63+ $$
64+ $$
65+ \mathbf{V}_0 : \mathbf{PreType} \equiv \{0, 1\},
66+ $$
67+ $$
68+ \mathbf{V}_1 : \mathbf{PreType} \equiv \{0 \to 1\},
69+ $$
70+ $$
71+ \mathbf{dim} : \prod_{n : \mathbb{N}} \mathbf{V}_n \to \mathbb{N},
72+ $$
73+ $$
74+ \mathbf{dim}\ n \equiv n.
75+ $$
76+ + code('urs' ).
77+ def V (n : Nat) : PreType := Interval n -- Cubical interval pretype
78+ def V₀ : PreType := {0, 1} -- 0-dimensional interval
79+ def V₁ : PreType := {0 → 1} -- 1-dimensional interval
80+ def dim (n : Nat) : V n → Nat := λ _ : V n, n -- Dimension of interval
81+ (* Cubical interval pretype formation *)
6382
64- h2 Prop and Classical Logic
83+ h2 Introduction
6584 + tex.
66- $\text{Prop}$ is 0-truncated, meaning any $P : \text{Prop}$ has at most one proof,
67- aligning with classical logic via Z3 integration. This contrasts with Coq’s
68- constructive $\text{Prop}$ (proof-relevant) and Lean’s flexible $\text{Prop}$ with
69- optional classical axioms.
85+ $\mathbf{Definition\ 1.1.3}$ (Fibrational Universe Rules). Fibrational universes
86+ support lifting, cumulativity, and product formation, ensuring type-theoretic consistency.
7087 + tex(true ).
7188 $$
72- P : \text{Prop}, \ p, q : P \implies p = q, \quad P \lor \neg P.
89+ \mathbf{lift} : \prod_{n, m : \mathbb{N}} \mathbf{U}_n \to (m \geq n) \to \mathbf{U}_m,
90+ $$
7391 $$
74- + code.
75- let prop_true : exp = Prop (* Classical Prop *)
92+ \mathbf{univ} : \prod_{n : \mathbb{N}} \mathbf{U}_{n+1},
93+ $$
94+ $$
95+ \mathbf{cumul} : \prod_{n, m : \mathbb{N}} \prod_{A : \mathbf{U}_n} (m \geq n) \to \mathbf{U}_m,
96+ $$
97+ $$
98+ \mathbf{prod} : \prod_{n, m : \mathbb{N}} \prod_{A : \mathbf{U}_n} \prod_{B : A \to \mathbf{U}_m} \mathbf{U}_{\max(n,m)}.
99+ $$
100+ + code('urs' ).
101+ def lift (n m : Nat) (A : U n) : m ≥ n → U m := λ ge : m ≥ n, transport (λ k : Nat, U k) ge A -- Universe lifting
102+ def univ-type (n : Nat) : U (n + 1) := lift n (n + 1) (U n) (le_succ n) -- Type-in-type formation
103+ def cumul (n m : Nat) (A : U n) : m ≥ n → U m := lift n m A -- Cumulativity
104+ def prod-rule (n m : Nat) (A : U n) (B : A → U m) : U (max n m) := Π (x : A), B x -- Product formation
105+ (* Fibrational universe rules *)
76106
77- h2 Coq and Lean Analogies
78107 + tex.
79- In Coq, $\text{Prop}$ is impredicative and constructive, allowing $P : \text{Prop}$
80- to define types inductively, whereas our $\text{Prop}$ is predicative within $U_0$
81- and classical. Lean’s $\text{Prop}$ is similar but supports quotient types natively,
82- which we defer to future extensions (e.g., Dedekind cuts in $\mathbb{R}$).
108+ $\mathbf{Definition\ 1.1.4}$ (Cubical Interval Introduction). Cubical interval pretypes
109+ introduce endpoints and paths for cubical type theory.
110+ + tex(true ).
111+ $$
112+ \mathbf{i0} : \prod_{n : \mathbb{N}} \mathbf{V}_n,
113+ $$
114+ $$
115+ \mathbf{i1} : \prod_{n : \mathbb{N}} \mathbf{V}_n,
116+ $$
117+ $$
118+ \mathbf{path} : \prod_{n : \mathbb{N}} \mathbf{V}_n \to \mathbf{V}_n \to \mathbf{V}_{n+1}.
119+ $$
120+ + code('urs' ).
121+ def i0 (n : Nat) : V n := 0 -- Left endpoint
122+ def i1 (n : Nat) : V n := 1 -- Right endpoint
123+ def path (n : Nat) (a b : V n) : V (n + 1) := a → b -- Path in higher dimension
124+ (* Cubical interval introduction *)
125+
126+ h2 Elimination
83127 + tex.
84- Our $U_0 : U_1$ mirrors Coq’s minimal hierarchy for analysis but avoids Lean’s
85- full cumulativity, prioritizing Z3-driven decidability over proof complexity.
128+ $\mathbf{Definition\ 1.1.5}$ (Cubical Interval Eliminators). Eliminators for cubical
129+ interval pretypes project to endpoints and evaluate paths.
130+ + tex(true ).
131+ $$
132+ \mathbf{eval\text{-}i0} : \prod_{n : \mathbb{N}} \prod_{p : \mathbf{V}_{n+1}} (p\ \mathbf{i0}) = \mathbf{i0},
133+ $$
134+ $$
135+ \mathbf{eval\text{-}i1} : \prod_{n : \mathbb{N}} \prod_{p : \mathbf{V}_{n+1}} (p\ \mathbf{i1}) = \mathbf{i1}.
136+ $$
137+ + code('urs' ).
138+ def eval-i0 (n : Nat) (p : V (n + 1)) : Path (V n) (p (i0 n)) (i0 n) := refl -- Evaluate at i0
139+ def eval-i1 (n : Nat) (p : V (n + 1)) : Path (V n) (p (i1 n)) (i1 n) := refl -- Evaluate at i1
140+ (* Cubical interval eliminators *)
86141
87- h2 Advantages and Limitations
142+ h2 Theorems
88143 + tex.
89- $\mathbf{Advantages}$: The limited hierarchy ensures type checking is straightforward,
90- and $\text{Prop}$’s classical nature aligns with Schwartz’s analysis, enabling
91- efficient Z3 verification for real arithmetic and set equality.
144+ $\mathbf{Theorem\ 1.1.6}$ (Universe Cumulativity Properties). Fibrational universes
145+ satisfy lifting and cumulativity laws.
146+ + tex(true ).
147+ $$
148+ \mathbf{lift\text{-}id} : \prod_{n : \mathbb{N}} \prod_{A : \mathbf{U}_n} (\mathbf{lift}\ n\ n\ A\ \mathbf{refl}) = A,
149+ $$
150+ $$
151+ \mathbf{cumul\text{-}trans} : \prod_{n, m, k : \mathbb{N}} \prod_{A : \mathbf{U}_n}
152+ (m \geq n) \to (k \geq m) \to (\mathbf{cumul}\ n\ k\ A) = (\mathbf{cumul}\ m\ k\ (\mathbf{cumul}\ n\ m\ A)).
153+ $$
154+ + code('urs' ).
155+ def lift-id (n : Nat) (A : U n) : Path (U n) (lift n n A refl) A := refl -- Lift identity
156+ def cumul-trans (n m k : Nat) (A : U n) (ge1 : m ≥ n) (ge2 : k ≥ m)
157+ : Path ( U k ) ( cumul n k A (trans ge1 ge2 ) ) ( cumul m k (cumul n m A ge1 ) ge2 ) := refl
158+ (* Universe cumulativity properties *)
159+
92160 + tex.
93- $\mathbf{Limitations}$: Higher universes ($U_2, U_3, \ldots$) are absent, restricting
94- nested type constructions beyond $U_1$ (e.g., $\text{Power}(\text{Power}(A))$ requires
95- careful encoding). Impredicativity is sacrificed for simplicity.
161+ $\mathbf{Theorem\ 1.1.7}$ (Cubical Interval Properties). Cubical interval pretypes
162+ satisfy path and dimension laws, supporting path types in \mathbf{path.pug}.
163+ + tex(true ).
164+ $$
165+ \mathbf{path\text{-}dim} : \prod_{n : \mathbb{N}} \prod_{a, b : \mathbf{V}_n}
166+ (\mathbf{dim}\ (\mathbf{path}\ n\ a\ b)) = (n + 1),
167+ $$
168+ $$
169+ \mathbf{path\text{-}comp} : \prod_{n : \mathbb{N}} \prod_{a, b : \mathbf{V}_n}
170+ (\mathbf{path}\ n\ a\ b\ \mathbf{i0}) = a,
171+ $$
172+ $$
173+ (\mathbf{path}\ n\ a\ b\ \mathbf{i1}) = b.
174+ $$
175+ + code('urs' ).
176+ def path-dim (n : Nat) (a b : V n) : Path Nat (dim (n + 1) (path n a b)) (n + 1) := refl -- Path dimension
177+ def path-comp-i0 (n : Nat) (a b : V n) : Path (V n) ((path n a b) (i0 n)) a := refl -- Path at i0
178+ def path-comp-i1 (n : Nat) (a b : V n) : Path (V n) ((path n a b) (i1 n)) b := refl -- Path at i1
179+ (* Cubical interval properties *)
96180
97- h2 Future Directions
98181 + tex.
99- Future support for quotient types (e.g., Lean-style $\text{Quotient}$) could enrich
100- $U_0$, enabling constructions like Dedekind reals directly within the system, though
101- current focus remains on Z3-backed real analysis without such granularity.
182+ $\mathbf{Theorem\ 1.1.8}$ (Test Cases). Examples illustrate fibrational universes
183+ and cubical intervals, applicable to path types in $\mathbf{Path}$.
184+ + tex(true ).
185+ $$
186+ \mathbf{bool} : \mathbf{U}_0,
187+ $$
188+ $$
189+ \mathbf{bool\text{-}lift} : \mathbf{U}_1,
190+ $$
191+ $$
192+ \mathbf{interval} : \prod_{i : \mathbf{V}_1} \mathbf{V}_0,
193+ $$
194+ $$
195+ \mathbf{interval\text{-}eval} : (\mathbf{interval}\ \mathbf{i0}) = \mathbf{i0}.
196+ $$
197+ + code('urs' ).
198+ def test-bool : U 0 := Bool -- Bool in U₀
199+ def test-bool-lift : U 1 := lift 0 1 Bool (le_succ 0) -- Lift Bool to U₁
200+ def test-interval (i : V 1) : V 0 := i -- Interval path
201+ def test-interval-eval : Path (V 0) (test-interval (i0 0)) (i0 0) := refl -- Evaluate interval at i0
202+ (* Test cases for universes and intervals *)
102203
103204include ../../footer
0 commit comments