{- 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=0) -> cz z, (i=1) -> cz (sucZ z)] zeroR : R = cz zeroZ glueR (z : Z) : Path R (cz z) (cz (sucZ z)) = 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 -> glueR (predZ zeroZ) @ -i succ z -> composition R zeroR (cz (inl z)) (cz (inl (succ z))) (vectNeg z) ( 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 -> compInv R zeroR (cz (inl z)) (vectNeg z) (cz (inl (succ z))) ( 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 ( Path R zeroR (glueR z @ i)) (vectR z) (vectR (sucZ z)) = substPathP (Path R zeroR (cz z)) (Path R zeroR (cz (sucZ z))) ( Path R zeroR (glueR z @ i)) (vectR z) (vectR (sucZ z)) (comp ( 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 ( 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 = 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) -> (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) = Path S1 x (composition S1 (f z) (f p.1) base ( 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 ( 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) = comp (<_> U) (lem @ i) [ (i = 0) -> (z : A) * (homoOverPath A p f q x z @ -j), (i = 1) -> 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