{- 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 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) omega_ (A: pointed): nat -> pointed = split -- omega n A zero -> A succ x -> omegaSplit x where omegaSplit: nat -> pointed = split zero -> omega1 A succ x -> omega_ (omega_ A (succ x)) (succ x) -- 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)