{- 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 (<i> 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