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