# INFINITESIMAL MODALITY

*shape modality* if
i)

```
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

*formally étale*
if its naturality square is a pullback:

```
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
```

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

# FORMAL DISK BUNDLE

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

```
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)
```

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

# MANIFOLDS

```
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.