INFINITESIMAL MODALITY

(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

(É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 BUNDLE

(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

MANIFOLDS

(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

LITERATURE

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