{- Pointed Types: - Pointed; - Loop Space; - Their Maps. Copyright (c) Groupoid Infinity, 2014-2018. HoTT 2.1 Types are higher groupoids HoTT 8.2 Connectedness of suspensions HoTT 8.4 Fiber sequences and the long exact sequence -} module pointed where import trunc import path import nat -- Definition 2.1.7 pointed: U = (A: U) * A ptSpace (A: U): U = (point: A) * unit point (A: pointed): A.1 = A.2 space (A: pointed): U = A.1 -- Definition 2.1.8 -- Loop Spaces omega1 (A: pointed): pointed = (Path (space A) (point A) (point A), refl A.1 (point A)) omega2 (A: pointed): pointed = omega1 (omega1 A) omega3 (A: pointed): pointed = omega2 (omega1 A) omega : nat -> pointed -> pointed = split zero -> idfun pointed succ n -> \(A: pointed) -> omega n (omega1 A) -- Definition 8.4.1 pmap (A B: pointed): U = (f: A.1 -> B.1) * (Path B.1 (f (point A)) (point B)) zmap (X Y: pointed): space X -> space Y = \ (x: space X) -> point Y omegaMap (A B: pointed) (f: pmap A B) : pmap (omega1 A) (omega1 B) = (space,prf) where space (p: (omega1 A).1) : (omega1 B).1 = kanOp B.1 (f.1 (point A)) (f.1 (p@i)) (point B) f.2 prf : Path (omega1 B).1 (space (point (omega1 A))) (point (omega1 B)) = kanOpRefl B.1 (f.1 (point A)) (point B) f.2 omegaMap2 (A B: pointed) (f: pmap A B): pmap (omega2 A) (omega2 B) = omegaMap (omega1 A) (omega1 B) (omegaMap A B f) omegaMap3 (A B: pointed) (f: pmap A B): pmap (omega3 A) (omega3 B) = omegaMap (omega2 A) (omega2 B) (omegaMap2 A B f) omegaMapRefl (A: pointed) (B: U) (h: A.1 -> B) (p: (omega1 A).1) : (omega1 (B, h (point A))).1 = h (p @ i) omegaMapRefl2 (A: pointed) (B: U) (h: A.1 -> B) (p: (omega2 A).1) : (omega2 (B, h (point A))).1 = h (p @ i @ j) omegaMapRefl3 (A: pointed) (B: U) (h: A.1 -> B) (p: (omega3 A).1) : (omega3 (B, h (point A))).1 = h (p @ i @ j @ k) -- The Wegde Sum : X \vee Y = X \times \{ y_0 \} \cup \{ x_0 \} \times Y data Wedge (A : pointed) (B : pointed) = winl (a : A.1) | winr (b : B.1) | wglue [ (x = 0) -> winl A.2 , (x = 1) -> winr B.2 ] -- The Smash Product : X \wedge Y = X \times Y / X \vee Y data Smash (A : pointed) (B : pointed) = spair (a : A.1) (b : B.1) | smash (a : A.1) (b : B.1) [(x=0) -> spair a B.2, (x=1) -> spair A.2 b] | smashpt [(x=0) -> smash {Smash A B} A.2 B.2 @ y, (x=1) -> spair A.2 B.2, (y=0) -> spair A.2 B.2, (y=1) -> spair A.2 B.2] data Join (A : U) (B : U) = joinl (a : A) | joinr (b : B) | join (a:A) (b:B) [(i=0) -> joinl a, (i=1) -> joinr b] SmashPt (A : pointed) (B : pointed) : pointed = (Smash A B, spair A.2 B.2) WedgePt (A : pointed) (B : pointed) : pointed = (Wedge A B, winl A.2) JoinPt (A : pointed) (B : pointed) : pointed = (Join A.1 B.1, joinl A.2)