Here is very short intro to formal differential geometry. It contains the notion of étale maps and formal disk bundles.

$$\def\mapright#1{\xrightarrow{{#1}}} \def\mapdown#1{\Big\downarrow\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapdiagl#1{\vcenter{\searrow}\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapdiagr#1{\vcenter{\swarrow}\rlap{\raise2pt{\scriptstyle{#1}}}} $$


Definition (Infinitesimal Shape Modality). The two maps $Im∶ U \rightarrow U$ and $\iota_A ∶ A \rightarrow Im(A)$ are called shape modality if i) $\iota_A$ is an equivalence, the type $A$ is then called coreduced.; ii) identity types of coreduced types are coreduced; iii) if $B∶Im(A)\rightarrow U$ is a dependent type such that for all $a∶Im(A)$ the type $B(a)$ is coreduced, then we can define a section of $B$ by induction. The $Im(A)$ is called de Rham space.

Im : U -> U ImUnit (A: U) : A -> Im A isCoreduced (A:U): U = isEquiv A (Im A) (ImUnit A) ImCoreduced (A:U): isCoreduced (Im A) ImRecursion (A B: U) (c: isCoreduced B) (f: A -> B) : Im A -> B ImInduction (A: U) (B: Im A -> U) (x: (a: Im A) -> isCoreduced (B a)) (y: (a: A) -> B (ImUnit A a)) : (a: Im A) -> B a


Definition (Étale map). A map $f:A \rightarrow B$ is formally étale if its naturality square is a pullback: $$ \begin{array}{ccc} A & \mapright{ι_A} & Im(A) \\ \mapdown{f} & \square & \mapdown{Im(f)} \\ B & \mapright{ι_B} & Im(B) \\ \end{array} $$ with induced naturality equation: $$ \eta_f(x) : Im(f(\iota_A(x))) = \iota_B(Im(f(x))). $$

ImApp (A B: U) (f: A -> B) : Im A -> Im B ImNaturality (A B: U) (f: A -> B) : (a: A) -> Path (Im B) ((ImUnit B) (f a)) ((ImApp A B f) (ImUnit A a))
isÉtaleMap (A B: U) (f: A -> B): U = isPullbackSq A iA B (Im B) x y w f h where iA : U = Im A iB : U = Im B x: iA -> iB = ImApp A B f y: B -> iB = ImUnit B w: A -> iA = ImUnit A c1: A -> iB = o A iA iB x w c2: A -> iB = o A B iB y f T2: U = (a:A) -> Path iB (c1 a) (c2 a) h: T2 = \(a : A) -> <i> ImNaturality A B f a @ -i
EtaleMap (A B: U): U = (f: A -> B) * isÉtaleMap A B f

Definition (Infinitesimal Close). Let $x,y: A$, then we have a type which could be read x is infinitesimally close to y and is given as: $$ x \sim y =_{def} ι_A (x) = ι_B (y). $$

isInfinitesimalClose (X: U) (a x': X): U = Path (Im X) (ImUnit X a) (ImUnit X x')


Definition (Formal Disk). Let $A$ be a type and $a:A$. The type $\mathbb{D}_a$ defined below in three equivalent ways is called the formal disk at a: i) $\mathbb{D}_a$ is the sum of all point infinitesimal close to a; $$ \mathbb{D}_a =_{def} \sum_{x:A} x \sim a $$ ii) $\mathbb{D}_a$ is a fiber of $ι_A$ at $ι_A(a)$; iii) $\mathbb{D}_a$ is defined as a pullback square: $$ \begin{array}{ccc} \mathbb{D}_a & \mapright{} & 1 \\ \mapdown{} & \square & \mapdown{* \mapsto ι_A(a)} \\ A & \mapright{ι_A} & Im(A) \\ \end{array} $$

formalDisc (X: U) (a: X): U = (x': X) * isInfinitesimalClose X a x'

Definition (Differential). If $f: A \rightarrow B$ is a type, there is a dependent function $$ df : \prod_{x:A} \mathbb{D}_x \rightarrow \mathbb{D}_{f(x)} $$ defined as $$ df_a =_{def} (x,ε) \mapsto (f(x),η^{−1}(x)•Im(f(ε))•η_f(x)) $$

differential (X Y: U) (f: X -> Y) (x: X) : formalDisc X x -> formalDisc Y (f x)

Definition (Formal Disk Bundle). Let $A$ be a type. The type $T_\infty(A)$ defined in one of the equivalent ways below is called the formal disk bundle of $A$: i) $T_\infty(A)$ is the sum over all formal disks in A: $$ T_\infty(A) =_{def} \sum_{x:A}\mathbb{D}_x $$ ii) $T_\infty(A)$ is defined by pullback square: $$ \begin{array}{ccc} T_\infty(A) & \mapright{} & A \\ \mapdown{} & \square & \mapdown{ι_A} \\ A & \mapright{ι_A} & Im(A) \\ \end{array} $$

formalDiscBundle (A: U): U = (a: A) * formalDisc A a

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

Theorem (Kock). The infinitesimal disk bundle construction is left adjoint to the jet comonad: $$ T_\infty \vdash Jet $$

Definition (Induced map). For a map $f : A \rightarrow B$ there is an induced map on the formal disk bundles, given as $$ T_\infty(A) =_{def} (a,ε) \mapsto (f(a),df_a(ε)) $$


Definition (Homogeneous structure). A type $A$ is homogeneous, if there are terms of the following types: i) $e:A$; ii) $t: \prod_{x:A} A = A$; iii) $p: \prod_{x:A}t_x(e) = x$.

homogeneous (A: U): U = (e: A) * (translationsFamily: (x: A) -> Path U A A) * ((x: A) -> Path A (transport (translationsFamily x) e) x)


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