{- The Hopf Fibration: - (self-containing) for hcomptrans. Copyright (c) Groupoid Infinity, 2014-2018 HoTT 8.5 The Hopf fibration -} module hopf where prod (A B: U): U = (_: A) * B idfun (A: U) (a: A): A = a Pi (A: U) (B: A -> U): U = (x: A) -> B(x) Path (A: U) (a b: A): U = PathP ( A) a b refl (A: U) (a: A): Path A a a = a singl (A: U) (a: A): U = (x: A) * Path A a x eta (A: U) (a: A): singl A a = (a,refl A a) contr (A: U) (a b: A) (p: Path A a b): Path (singl A a) (eta A a) (b,p) = (p @ i, p @ i/\j) isContr (A : U) : U = (x : A) * ((y : A) -> Path A x y) fiber (A B : U) (f : A -> B) (y : B) : U = (x : A) * Path B y (f x) isEquiv (A B : U) (f : A -> B) : U = (y : B) -> isContr (fiber A B f y) equiv (A B : U) : U = (f : A -> B) * isEquiv A B f isContrSingl (A:U) (a:A): isContr (singl A a) = ((a,refl A a),\ (z:singl A a) -> contr A a z.1 z.2) idEquiv (A:U): equiv A A = (\ (x:A) -> x, isContrSingl A) ap (A B: U) (f: A -> B) (a b: A) (p: Path A a b): Path B (f a) (f b) = f (p@i) subst (A: U) (P: A -> U) (a b: A) (p: Path A a b) (e: P a): P b = transport (ap A U P a b p) e contrSingl (A: U) (a b: A) (p: Path A a b): Path ((x: A) * Path A a x) (a,<_>a) (b,p) = (p@i,p@i/\j) idIsEquiv (A : U) : isEquiv A A (idfun A) = \(a : A) -> ((a,<_>a),\(z : fiber A A (idfun A) a) -> contrSingl A a z.1 z.2) Square (A : U) (a0 a1 b0 b1 : A) (u : Path A a0 a1) (v : Path A b0 b1) (r0 : Path A a0 b0) (r1 : Path A a1 b1) : U = PathP ( (PathP ( A) (u @ i) (v @ i))) r0 r1 data N = Z | S (n: N) -- n-Groupoid n_grpd (A: U) (n: N): U = (a b: A) -> rec A a b n where rec (A: U) (a b: A) : (k: N) -> U = split { Z -> Path A a b ; S n -> n_grpd (Path A a b) n } isContr (A: U): U = (x: A) * ((y: A) -> Path A x y) isProp (A: U): U = n_grpd A Z isSet (A: U): U = n_grpd A (S Z) isGroupoid (A: U): U = n_grpd A (S (S Z)) ------------- lemIso (A B : U) (f : A -> B) (g : B -> A) (s : (y : B) -> Path B (f (g y)) y) (t : (x : A) -> Path A (g (f x)) x) (y : B) (x0 x1 : A) (p0 : Path B y (f x0)) (p1 : Path B y (f x1)) : Path (fiber A B f y) (x0,p0) (x1,p1) = (p @ i,sq1 @ i) where rem0 : Path A (g y) x0 = hcomp A (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> g y ] rem1 : Path A (g y) x1 = hcomp A (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> g y ] p : Path A x0 x1 = hcomp A (g y) [ (i = 0) -> rem0, (i = 1) -> rem1 ] fill0 : Square A (g y) (g (f x0)) (g y) x0 ( g (p0 @ i)) rem0 ( g y) (t x0) = hcomp A (g (p0 @ i)) [ (i = 1) -> t x0 @ j /\ k , (i = 0) -> g y , (j = 0) -> g (p0 @ i) ] fill1 : Square A (g y) (g (f x1)) (g y) x1 ( g (p1 @ i)) rem1 ( g y) (t x1) = hcomp A (g (p1 @ i)) [ (i = 1) -> t x1 @ j /\ k , (i = 0) -> g y , (j = 0) -> g (p1 @ i) ] fill2 : Square A (g y) (g y) x0 x1 ( g y) p rem0 rem1 = hcomp A (g y) [ (i = 0) -> rem0 @ j /\ k , (i = 1) -> rem1 @ j /\ k , (j = 0) -> g y ] sq : Square A (g y) (g y) (g (f x0)) (g (f x1)) ( g y) ( g (f (p @ i))) ( g (p0 @ j)) ( g (p1 @ j)) = hcomp A (fill2 @ i @ j) [ (i = 0) -> fill0 @ j @ -k , (i = 1) -> fill1 @ j @ -k , (j = 0) -> g y , (j = 1) -> t (p @ i) @ -k ] sq1 : Square B y y (f x0) (f x1) (y) ( f (p @ i)) p0 p1 = hcomp B (f (sq @ i @j)) [ (i = 0) -> s (p0 @ j) , (i = 1) -> s (p1 @ j) , (j = 1) -> s (f (p @ i)) , (j = 0) -> s y ] gradLemma (A B : U) (f : A -> B) (g : B -> A) (s : (y : B) -> Path B (f (g y)) y) (t : (x : A) -> Path A (g (f x)) x) : isEquiv A B f = \(y:B) -> ((g y,s y@-i),\ (z:fiber A B f y) -> lemIso A B f g s t y (g y) z.1 (s y@-i) z.2) isoPath (A B : U) (f : A -> B) (g : B -> A) (s : (y : B) -> Path B (f (g y)) y) (t : (x : A) -> Path A (g (f x)) x) : Path U A B = Glue B [ (i = 0) -> (A,f,gradLemma A B f g s t) , (i = 1) -> (B,idfun B,idIsEquiv B) ] -------------- data S1 = base | loop [ (i=0) -> base , (i=1) -> base] loopS1 : U = Path S1 base base loop1 : loopS1 = loop{S1} @ i data susp (A : U) = north | south | merid (a : A) [ (i=0) -> north , (i=1) -> south ] constSquare (A : U) (a : A) (p : Path A a a) : Square A a a a a p p p p = hcomp A a [ (i = 0) -> p @ (j \/ - k), (i = 1) -> p @ (j /\ k), (j = 0) -> p @ (i \/ - k), (j = 1) -> p @ (i /\ k)] lemPropF (A : U) (P : A -> U) (pP : (x : A) -> isProp (P x)) (a0 a1 :A) (p : Path A a0 a1) (b0 : P a0) (b1 : P a1) : PathP ( P (p @ i)) b0 b1 = pP (p @ i) (comp ( P (p @ i/\ j)) b0 [ (i=0) -> <_> b0]) (comp ( P (p @ i\/ -j)) b1 [ (i=1) -> <_> b1]) @ i lemSig (A : U) (B : A -> U) (pB : (x : A) -> isProp (B x)) (u v : (x:A) * B x) (p : Path A u.1 v.1) : Path ((x:A) * B x) u v = (p@i,(lemPropF A B pB u.1 v.1 p u.2 v.2)@i) propSig (A : U) (B : A -> U) (pA : isProp A) (pB : (x : A) -> isProp (B x)) (t u : (x:A) * B x) : Path ((x:A) * B x) t u = lemSig A B pB t u (pA t.1 u.1) compPath (A : U) (a b c : A) (p : Path A a b) (q : Path A b c) : Path A a c = hcomp A (p @ i) [ (i = 1) -> q, (i=0) -> a ] propPi (A : U) (B : A -> U) (h : (x : A) -> isProp (B x)) (f0 f1 : (x : A) -> B x) : Path ((x : A) -> B x) f0 f1 = \ (x:A) -> (h x (f0 x) (f1 x)) @ i idPi (A:U) (B:A->U) (f g : Pi A B) : Path U (Path (Pi A B) f g) ((x:A) -> Path (B x) (f x) (g x)) = isoPath (Path (Pi A B) f g) ((x:A) -> Path (B x) (f x) (g x)) F G S T where T0 : U = Path (Pi A B) f g T1 : U = (x:A) -> Path (B x) (f x) (g x) F (p:T0) : T1 = \ (x:A) -> p@i x G (p:T1) : T0 = \ (x:A) -> p x @ i S (p:T1) : Path T1 (F (G p)) p = refl T1 p T (p:T0) : Path T0 (G (F p)) p = refl T0 p setPi (A:U) (B:A -> U) (h:(x:A) -> isSet (B x)) (f g: Pi A B) : isProp (Path (Pi A B) f g) = rem where T : U = (x:A) -> Path (B x) (f x) (g x) rem1 : isProp T = \ (p q : T) -> \ (x:A) -> h x (f x) (g x) (p x) (q x)@i rem : isProp (Path (Pi A B) f g) = subst U isProp T (Path (Pi A B) f g) (idPi A B f g@-i) rem1 propSet (A : U) (h : isProp A) : isSet A = \(a b : A) (p q : Path A a b) -> hcomp A a [ (i=0) -> h a a , (i=1) -> h a b , (j=0) -> h a (p @ i) , (j=1) -> h a (q @ i)] lemProp (A : U) (h : A -> isProp A) : isProp A = \(a : A) -> h a a propIsContr (A : U) : isProp (isContr A) = lemProp (isContr A) rem where rem (t : isContr A) : isProp (isContr A) = propSig A T pA pB where T (x : A) : U = (y : A) -> Path A x y pA (x y : A) : Path A x y = compPath A x t.1 y ( t.2 x @ -i) (t.2 y) pB (x : A) : isProp (T x) = propPi A (\ (y : A) -> Path A x y) (propSet A pA x) propIsEquiv (A B : U) (f : A -> B) : isProp (isEquiv A B f) = \(u0 u1 : isEquiv A B f) -> \(y : B) -> propIsContr (fiber A B f y) (u0 y) (u1 y) @ i equivPath (A B : U) (v w : equiv A B) (p : Path (A -> B) v.1 w.1) : Path (equiv A B) v w = lemSig (A -> B) (isEquiv A B) (propIsEquiv A B) v w p data bool = false | true negBool : bool -> bool = split { false -> true ; true -> false } negBoolK : (b : bool) -> Path bool (negBool (negBool b)) b = split { false->false;true->true } negBoolEquiv : equiv bool bool = (negBool,gradLemma bool bool negBool negBool negBoolK negBoolK) S2 : U = susp S1 S3 : U = susp S2 ua (A B : U) (e : equiv A B) : Path U A B = Glue B [ (i = 0) -> (A,e), (i = 1) -> (B,idEquiv B) ] opaque propIsEquiv -- 1. Real moebius : S1 -> U = split base -> bool loop @ i -> ua bool bool negBoolEquiv @ i TH0 : U = (c : S1) * moebius c -- 2. Complex rot: (x : S1) -> Path S1 x x = split base -> loop1 loop @ i -> constSquare S1 base loop1 @ i mu : S1 -> equiv S1 S1 = split base -> idEquiv S1 loop @ i -> equivPath S1 S1 (idEquiv S1) (idEquiv S1) ( \ (x: S1) -> rot x @ j) @ i H1 : S2 -> U = split { north -> S1 ; south -> S1 ; merid x @ i -> ua S1 S1 (mu x) @ i } TH1 : U = (c : S2) * H1 c -- 3. Quaternionic -- 4. Octanionic -- more classical representation of H-space H_space: U = (A: U) * (e: A) * (mu: A -> A -> A) * ((a:A) -> prod (Path A (mu e a) a) (Path A (mu a e) a))