{- 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 -- Formal Disk Bundle isInfinitesimalClose (X: U) (a x': X): U = Path (Im X) (ImUnit X a) (ImUnit X x') formalDisc (X: U) (a: X): U = (x': X) * isInfinitesimalClose X a x' unitDisc (X: U) (x: Im X): U = (x': X) * Path (Im X) x (ImUnit X x') starDisc (X: U) (x: X): formalDisc X x = (x, refl (Im X) (ImUnit X x)) differential (X Y: U) (f: X -> Y) (x: X) : formalDisc X x -> formalDisc Y (f x) = undefined formalDiscBundle (A: U): U = (a: A) * formalDisc A a -- T_\infty(A) := \Sigma_{a:A}\mathbb{D}_a lemma45 (A B C: U) (f: A -> B) (g: B -> C) (x: A) : Path (formalDisc A x -> formalDisc C ((o A B C g f) x)) (differential A C (o A B C g f) x) (o (formalDisc A x) (formalDisc B (f x)) (formalDisc C ((o A B C g f) x)) (differential B C g (f x)) (differential A B f x)) = undefined preservesInifinitesimalProximity (X Y: U) (x x': X) (f: X -> Y) : isInfinitesimalClose X x x' -> isInfinitesimalClose Y (f x) (f x') = undefined