SMOOTH SETS TYPE

The type models smooth sets, sheaves on the site of Cartesian spaces , representing generalized smooth manifolds. Smooth sets underpin differential geometry, gauge theory, and smooth homotopy in the cohesive type system of .

The type is a parameterless type in , with plots defining smooth maps for a smooth set , capturing its smooth structure.

Formation

(-Formation). The type is a base type in the universe , the category of sheaves on Cartesian spaces for .

def SmthSet : U_1

Introduction

(-Introduction). The plot constructor introduces terms of type for a smooth set , representing smooth maps from to for each .

def plt (n : Nat) (X : SmthSet) : Set
(* Smooth maps from ℝ^n to X *)

Elimination

(-Elimination). The eliminator for plots reasons about smooth maps by mapping them to properties in , preserving the smooth structure of .

def plt_ind (n : Nat) (X : SmthSet) (beta : plt n X -> Set) (h : Π (phi : plt n X), beta phi) : Π (phi : plt n X), beta phi
(* Eliminator for plots *)

Theorems

(Plot Composition). For , plots compose with smooth maps to yield plots , functorially.

def precomp (m n : Nat) (X : SmthSet) (f : ℝ^m -> ℝ^n) : plt n X -> plt m X
(* Composition of plots *)

(Plot Evaluation). Plots evaluate to terms of , recovering points of the smooth set.

def eval (n : Nat) (X : SmthSet) : plt n X -> X
(* Evaluation to smooth set *)

(Yoneda Embedding). The plots embed into the presheaf of smooth maps, equating plots with natural transformations via the Yoneda lemma.

def yoneda (n : Nat) (X : SmthSet)
  : Path (plt n X) (Π (m : Nat), Hom_SmthSet (ℝ^m, ℝ^n) -> plt m X)