{- Real Cohesive Homotopy Type Theory: - Flat, Shape, Crisp modalities. Copyright (c) Groupoid Infinity, 2016-2018. -} module real where import s1 helix : S1 -> U = split { base -> Z ; loop @ i -> sucPathZ @ i } -- Homotopy Reals data R = cz (x: Z) | sz (z: Z) [(i=0) -> cz z, (i=1) -> cz (sucZ z)] RtoHelix: R -> U = split cz x -> helix base sz z p @ i -> helix (loop {S1} @ i) -- Flat Modality data flat (A: U) = con (x: flat A) flatInd (A: U) (C: flat A -> U) (f: (u: flat A) -> C (con u)) : (x: flat A) -> C x = split con x -> f x -- Shape Modality (Fundamental $\infty$-groupoid) data shape (A: U) = sig' (_: A) | kap (_: R -> shape A) | kap' (_: R -> shape A) shapeRec (A B: U) (f: A -> B) (k: (R -> B) -> B) (k': (R -> B) -> B) (p1': (g: R -> B) (x: R) -> Path B (g x) (k g)) (p2': (x: B) -> Path B x (k' (\(_:R) -> x))) : shape A -> B = split sig' a -> f a kap g -> k (\(x:R) -> shapeRec A B f k k' p1' p2' (g x)) kap' g -> k' (\(x:R) -> shapeRec A B f k k' p1' p2' (g x)) -- Discrete Types IsDiscrete (A: U) : U = (f: A -> (R -> A)) * isEquiv A (R -> A) f