FIBRATIONAL UNIVERSES AND CUBICAL PRETYPES

The type represents a fibrational universe hierarchy indexed by levels , supporting type formation and cumulativity in a predicative setting, following Cubical Agda. The type represents cubical interval pretypes, indexed by , used to model cubical intervals for path types and glue types in homotopy type theory.

In Urs, and provide the foundational type hierarchies for homotopy groups, supporting path types in , glue types in , and enabling higher structures in .

Formation

(Fibrational Universe Formation). The universe is a type indexed by , containing types at level .

def U (n : Nat) : Type := Universe n  -- Universe formation
def U₀ : Type := U 0  -- Level 0 universe
def U₁ : Type := U 1  -- Level 1 universe
(* Fibrational universe formation *)

(Cubical Interval Pretype Formation). The cubical interval pretype is a pretype indexed by , used to model cubical intervals with dimension for path types and glue types.

def V (n : Nat) : PreType := Interval n  -- Cubical interval pretype
def V₀ : PreType := {0, 1}  -- 0-dimensional interval
def V₁ : PreType := {0 → 1}  -- 1-dimensional interval
def dim (n : Nat) : V n → Nat := λ _ : V n, n  -- Dimension of interval
(* Cubical interval pretype formation *)

Introduction

(Fibrational Universe Rules). Fibrational universes support lifting, cumulativity, and product formation, ensuring type-theoretic consistency.

def lift (n m : Nat) (A : U n) : m ≥ n → U m := λ ge : m ≥ n, transport (λ k : Nat, U k) ge A  -- Universe lifting
def univ-type (n : Nat) : U (n + 1) := lift n (n + 1) (U n) (le_succ n)  -- Type-in-type formation
def cumul (n m : Nat) (A : U n) : m ≥ n → U m := lift n m A  -- Cumulativity
def prod-rule (n m : Nat) (A : U n) (B : A → U m) : U (max n m) := Π (x : A), B x  -- Product formation
(* Fibrational universe rules *)

(Cubical Interval Introduction). Cubical interval pretypes introduce endpoints and paths for cubical type theory.

def i0 (n : Nat) : V n := 0  -- Left endpoint
def i1 (n : Nat) : V n := 1  -- Right endpoint
def path (n : Nat) (a b : V n) : V (n + 1) := a → b  -- Path in higher dimension
(* Cubical interval introduction *)

Elimination

(Cubical Interval Eliminators). Eliminators for cubical interval pretypes project to endpoints and evaluate paths.

def eval-i0 (n : Nat) (p : V (n + 1)) : Path (V n) (p (i0 n)) (i0 n) := refl  -- Evaluate at i0
def eval-i1 (n : Nat) (p : V (n + 1)) : Path (V n) (p (i1 n)) (i1 n) := refl  -- Evaluate at i1
(* Cubical interval eliminators *)

Theorems

(Universe Cumulativity Properties). Fibrational universes satisfy lifting and cumulativity laws.

def lift-id (n : Nat) (A : U n) : Path (U n) (lift n n A refl) A := refl  -- Lift identity
def cumul-trans (n m k : Nat) (A : U n) (ge1 : m ≥ n) (ge2 : k ≥ m)
  : Path (U k) (cumul n k A (trans ge1 ge2)) (cumul m k (cumul n m A ge1) ge2) := refl
(* Universe cumulativity properties *)

(Cubical Interval Properties). Cubical interval pretypes satisfy path and dimension laws, supporting path types in \mathbf{path.pug}.

def path-dim (n : Nat) (a b : V n) : Path Nat (dim (n + 1) (path n a b)) (n + 1) := refl  -- Path dimension
def path-comp-i0 (n : Nat) (a b : V n) : Path (V n) ((path n a b) (i0 n)) a := refl  -- Path at i0
def path-comp-i1 (n : Nat) (a b : V n) : Path (V n) ((path n a b) (i1 n)) b := refl  -- Path at i1
(* Cubical interval properties *)

(Test Cases). Examples illustrate fibrational universes and cubical intervals, applicable to path types in .

def test-bool : U 0 := Bool  -- Bool in U₀
def test-bool-lift : U 1 := lift 0 1 Bool (le_succ 0)  -- Lift Bool to U₁
def test-interval (i : V 1) : V 0 := i  -- Interval path
def test-interval-eval : Path (V 0) (test-interval (i0 0)) (i0 0) := refl  -- Evaluate interval at i0
(* Test cases for universes and intervals *)