# INFINITESIMAL

Bundle package contains axiom of infinitesimal comonadic shape modality Im.

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

```
Im : U -> U = undefined
ImUnit (A: U) : A -> Im A = undefined
```

```
isCoreduced (A:U): U = isEquiv A (Im A) (ImUnit A)
ImCoreduced (A:U): isCoreduced (Im A) = undefined
ImEquality (A B: U) (a: isCoreduced A) (b: isCoreduced B)
: isCoreduced (Path U A B) = undefined
ImRecursion (A B: U) (c: isCoreduced B) (f: A -> B) : Im A -> B = undefined
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 = undefined
ImComputeRecursion (A B: U) (c: isCoreduced B) (f: A->B) (a:A)
: Path B ((ImRecursion A B c f) (ImUnit A a)) (f a) = undefined
ImComputeInduction (A:U)(B:Im A->U) (c:(a:Im A)->isCoreduced(B a)) (f:(a:A)->B(ImUnit A a))(a:A)
: Path (B (ImUnit A a)) (f a) ((ImInduction A B c f) (ImUnit A a)) = undefined
```