{- The modality of shape infinitesimal in cohesive infinity topos. - \Im modality type. Copyright (c) Groupoid Infinity, 2014-2018. HoTT 7.7 Modalities https://ncatlab.org/schreiber/show/thesis+Wellen https://arxiv.org/pdf/1806.05966.pdf -} module infinitesimal where import path import equiv import trunc -- Infinitesimal modality, represents infinitesimal shape constructions -- Formation Im : U -> U = undefined -- Introduction ImUnit (A: U) : A -> Im A = undefined isCoreduced (A:U): U = isEquiv A (Im A) (ImUnit A) ImCoreduced (A:U): isCoreduced (Im A) = undefined ImRecursion (A B: U) (c: isCoreduced B) (f: A -> B) : Im A -> B = undefined ImComputeRecursion (A B: U) (c: isCoreduced B) (f: A -> B) (a: A) : PathP ( B) ((ImRecursion A B c f) (ImUnit A a)) (f a) = undefined ImApp (A B: U) (f: A -> B) : Im A -> Im B = ImRecursion A (Im B) (ImCoreduced B) (o A B (Im B) (ImUnit B) f) ImNaturality (A B: U) (f: A -> B) : (a: A) -> Path (Im B) ((ImUnit B) (f a)) ((ImApp A B f) (ImUnit A a)) = undefined -- Elimination 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 -- Beta 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