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