(Infinitesimal Shape Modality or de Rham stack). The two maps and are called shape modality if i) is an equivalence, the type is then called coreduced.; ii) identity types of coreduced types are coreduced; iii) if is a dependent type such that for all the type is coreduced, then we can define a section of by induction. The is called de Rham space.

def ι (A : U) (a : A) : ℑ A := ℑ-unit a def is-coreduced (A : U) : U := isEquiv A (ℑ A) (ι A) def ℑ-coreduced (A : U) : is-coreduced (ℑ A) := isoToEquiv (ℑ A) ((ℑ A)) (ι (ℑ A)) (μ A) (λ (x :(ℑ A)), <_> x) (λ (y : ℑ A), <_> y) def ℑ-rec (A B : U) (c : is-coreduced B) (f : A B) : ℑ A B := ℑ-ind A (λ (_ : ℑ A), B) (λ (_ : ℑ A), c) f def ℑ-ind (A : U) (B : ℑ A U) (c : Π (a : ℑ A), is-coreduced (B a)) (f : Π (a : A), B (ι A a)) (a : ℑ A) : B a := (c a (ind-ℑ A B (λ (x : A), ι (B (ι A x)) (f x)) a)).1.1


(Étale map). A map is formally étale if its naturality square is a pullback: with induced naturality equation:

def ℑ-app (A B : U) (f : A B) : ℑ A ℑ B := ℑ-rec A (ℑ B) (ℑ-coreduced B) (∘ A B (ℑ B) (ι B) f) def ℑ-naturality (A B : U) (f : A B) (a : A) : Path (ℑ B) ((ι B) (f a)) ((ℑ-app A B f) (ι A a)) := <_> ℑ-unit (f a)
def isÉtaleMap (A B : U) (f : A B) : U := isPullbackSq A (ℑ A) B (ℑ B) (ℑ-app A B f) (ι B) (ι A) f (λ (a : A), <_> ℑ-unit (f a))
def ÉtaleMap (A B : U) : U := Σ (f : A B), isÉtaleMap A B f

(Infinitesimal Close). Let , then we have a type which could be read x is infinitesimally close to y and is given as:

def ~ (X : U) (a x′ : X) : U := Path (ℑ X) (ι X a) (ι X x′)


(Formal Disk). Let be a type and . The type defined below in three equivalent ways is called the formal disk at a: i) is the sum of all point infinitesimal close to a; ii) is a fiber of at ; iii) is defined as a pullback square:

def 𝔻 (X : U) (a : X) : U := Σ (x′ : X), ~ X a x′

(Differential). If is a type, there is a dependent function defined as

def inf-prox-ap (X Y : U) (f : X Y) (x x′ : X) (p : ~ X x x′) : ~ Y (f x) (f x′) := <i> ℑ-app X Y f (p @ i) def d (X Y : U) (f : X Y) (x : X) (ε : 𝔻 X x) : 𝔻 Y (f x) := (f ε.1, inf-prox-ap X Y f x ε.1 ε.2)

(Formal Disk Bundle). Let be a type. The type defined in one of the equivalent ways below is called the formal disk bundle of : i) is the sum over all formal disks in A: ii) is defined by pullback square:

def T∞ (A : U) : U := Σ (a : A), 𝔻 A a

(Hennion). The tangent complex of a derived algebraic stack is equivalently the (sheaf of modules of) sections of the formal neighbourhood of the diagonal of . We may think of as being the tangent complex of .

(Kock). The infinitesimal disk bundle construction is left adjoint to the jet comonad:

(Induced map). For a map there is an induced map on the formal disk bundles, given as


(Homogeneous structure). A type is homogeneous, if there are terms of the following types: i) ; ii) ; iii) .

def is-homogeneous (A : U) := Σ (e : A) (t : A equiv A A), Π (x : A), Path A ((t x).1 e) x


[1]. Felix Cherubini Formalizing Cartan Geometry in Modal Homotopy Type Theory.