{- Real Cohesive Homotopy Type Theory:
   - Flat, Shape, Crisp modalities.
   Copyright (c) Groupoid Infinity, 2016-2018. -}

module real where
import homotopy
import pullback

-- Homotopy Reals
data R
  = cz (x: Z)
  | sz (z: Z) <i> [(i=0) -> cz z, (i=1) -> cz (sucZ z)]

zeroR : R = cz zeroZ

glueR (z : Z) : Path R (cz z) (cz (sucZ z)) =
  <i> sz{R} z @ i

vectPos : (x : nat) -> Path R zeroR (cz (inr x)) = split
  zero -> <_> zeroR
  succ z -> composition R zeroR (cz (inr z)) (cz (inr (succ z))) (vectPos z) (glueR (inr z))

vectNeg : (x : nat) -> Path R zeroR (cz (inl x)) = split
  zero -> <i> glueR (predZ zeroZ) @ -i
  succ z -> composition R zeroR (cz (inl z)) (cz (inl (succ z)))
                                (vectNeg z) (<i> glueR (inl (succ z)) @ -i)

vectR : (x : Z) -> Path R zeroR (cz x) = split
  inl a -> vectNeg a
  inr b -> vectPos b

vectNegComp : (z : nat) ->
  Path (Path R zeroR (cz (sucZ (inl z))))
       (composition R zeroR (cz (inl z)) (cz (sucZ (inl z)))
                            (vectR (inl z)) (glueR (inl z)))
       (vectR (sucZ (inl z))) = split
  zero -> compInvPath R (cz (predZ zeroZ)) zeroR (glueR (predZ zeroZ))
  succ z -> <i> compInv R zeroR (cz (inl z)) (vectNeg z) (cz (inl (succ z))) (<j> glueR (inl (succ z)) @ -j) @ -i

vectComp : (z : Z) ->
  Path (Path R zeroR (cz (sucZ z)))
       (composition R zeroR (cz z) (cz (sucZ z)) (vectR z) (glueR z))
       (vectR (sucZ z)) = split
  inl a -> vectNegComp a
  inr b -> <_> vectR (inr (succ b))

vectOverTransport (z : Z) : PathP (<i> Path R zeroR (glueR z @ i)) (vectR z) (vectR (sucZ z)) =
  substPathP (Path R zeroR (cz z)) (Path R zeroR (cz (sucZ z)))
    (<i> Path R zeroR (glueR z @ i)) (vectR z) (vectR (sucZ z))
    (comp (<j> Path (Path R zeroR (cz (sucZ z)))
                    (composition R zeroR (cz z) (cz (sucZ z)) (vectR z) (glueR z))
                    (vectComp z @ j))
          (substToComp R zeroR (cz z) (cz (sucZ z)) (glueR z) (vectR z)) [])

zeroPath : (x : R) -> Path R zeroR x = split
  cz x -> vectR x
  sz z @ i -> vectOverTransport z @ i

contrR : isContr R = (zeroR, zeroPath)

distR (x y : R) : Path R x y =
  composition R x zeroR y (<i> zeroPath x @ -i) (zeroPath y)

RtoHelix: R -> U = split
  cz x -> helix base
  sz z @ i -> helix (loop {S1} @ i)

cis : R -> S1 = split
  cz x -> base
  sz z @ i -> loop{S1} @ i

helixOverCis (x : R) : Path U (helix (cis x)) Z =
  <i> helix (cis (distR x zeroR @ i))

ttPath : (x : unit) -> Path unit tt x = split
  tt -> <_> tt

contrUnitPath (A : U) (p : isContr A) : Path U A unit
  = isoPath A unit (\(_ : A) -> tt) (\(_ : unit) -> p.1) ttPath p.2

unitProdPath (A : U) : Path U (prod unit A) A
  = isoPath (prod unit A) A (\(p : prod unit A) -> p.2) (\(x : A) -> (tt, x))
    (\(x : A) -> <_> x) (\(x : prod unit A) -> <i> (ttPath x.1 @ i, x.2))

homoOverPath (A : U) (p : isContr A) (f : A -> S1) (q : Path S1 (f p.1) base)
  (x : S1) (z : A) : Path U (Path S1 x (f z)) (Path S1 x base)
  = <i> Path S1 x (composition S1 (f z) (f p.1) base (<j> f (p.2 z @ -j)) q @ i)

pathInvEquiv (A : U) (a b : A) : Path U (Path A a b) (Path A b a)
  = isoPath (Path A a b) (Path A b a) (inv A a b) (inv A b a)
      (\(p : Path A b a) -> <_> p) (\(p : Path A a b) -> <_> p)

contrProd (A B : U) (p : isContr A) : Path U (prod A B) B
  = composition U (prod A B) (prod unit B) B
      (<i> prod (contrUnitPath A p @ i) B) (unitProdPath B)

fibOfHomo (A : U) (p : isContr A) (f : A -> S1) (q : Path S1 (f p.1) base)
  (x : S1) : Path U (fiber A S1 f x) (helix x)
  = <i> comp (<_> U) (lem @ i)
             [ (i = 0) -> <j> (z : A) * (homoOverPath A p f q x z @ -j),
               (i = 1) -> <j> helixFamily x @ -j ]
  where
    lem : Path U (prod A (Path S1 x base)) (Path S1 base x)
      = composition U (prod A (Path S1 x base)) (Path S1 x base) (Path S1 base x)
          (contrProd A (Path S1 x base) p) (pathInvEquiv S1 x base)

kerOfHomo (A : U) (p : isContr A) (f : A -> S1) (q : Path S1 (f p.1) base) :
  Path U (fiber A S1 f base) Z
  = fibOfHomo A p f q base

Euler : Path U (fiber R S1 cis base) Z
  = kerOfHomo R contrR cis (<_> base)

-- 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