{- 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 (<i> A) a b
refl (A: U) (a: A): Path A a a = <i> 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) = <i> (p @ i,<j> 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) = <i> 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) = <i>(p@i,<j>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 (<i> (PathP (<j> 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) = <i> (p @ i,sq1 @ i)
  where
    rem0 : Path A (g y) x0 = <i> hcomp A (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> <k> g y ]
    rem1 : Path A (g y) x1 = <i> hcomp A (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> <k> g y ]
    p : Path A x0 x1 = <i> hcomp A (g y) [ (i = 0) -> rem0, (i = 1) -> rem1 ]
    fill0 : Square A (g y) (g (f x0)) (g y) x0
                     (<i> g (p0 @ i)) rem0 (<i> g y) (t x0)  =
      <i j> hcomp A (g (p0 @ i)) [ (i = 1) -> <k> t x0 @ j /\ k
                                      , (i = 0) -> <k> g y
                                      , (j = 0) -> <k> g (p0 @ i) ]

    fill1 : Square A (g y) (g (f x1)) (g y) x1
                     (<i> g (p1 @ i)) rem1 (<i> g y) (t x1) =
      <i j> hcomp A (g (p1 @ i)) [ (i = 1) -> <k> t x1 @ j /\ k
                                      , (i = 0) -> <k> g y
                                      , (j = 0) -> <k> g (p1 @ i) ]

    fill2 : Square A (g y) (g y) x0 x1
                     (<k> g y) p rem0 rem1 =
      <i j> hcomp A (g y) [ (i = 0) -> <k> rem0 @ j /\ k
                               , (i = 1) -> <k> rem1 @ j /\ k
                               , (j = 0) -> <k> g y ]

    sq : Square A (g y) (g y) (g (f x0)) (g (f x1))
                  (<i> g y) (<i> g (f (p @ i)))
                  (<j> g (p0 @ j)) (<j> g (p1 @ j)) =
      <i j> hcomp A (fill2 @ i @ j) [ (i = 0) -> <k> fill0 @ j @ -k
                                         , (i = 1) -> <k> fill1 @ j @ -k
                                         , (j = 0) -> <k> g y
                                         , (j = 1) -> <k> t (p @ i) @ -k ]

    sq1 : Square B y y (f x0) (f x1)
                   (<k>y) (<i> f (p @ i)) p0 p1 =
      <i j> 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,<i>s y@-i),\ (z:fiber A B f y) ->
    lemIso A B f g s t y (g y) z.1 (<i>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 =
       <i> 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> [ (i=0) -> base
                   , (i=1) -> base]

loopS1 : U = Path S1 base base
loop1 : loopS1 = <i> loop{S1} @ i

data susp (A : U) = north
                  | south
                  | merid (a : A) <i> [ (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 =
  <i j> hcomp A a [ (i = 0) -> <k> p @ (j \/ - k),
                    (i = 1) -> <k> p @ (j /\ k),
                    (j = 0) -> <k> p @ (i \/ - k),
                    (j = 1) -> <k> 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 (<i> P (p @ i)) b0 b1 =
  <i> pP (p @ i) (comp (<j> P (p @ i/\ j)) b0 [ (i=0) -> <_> b0])
                 (comp (<j> 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 =
  <i> (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 =
  <i> hcomp A (p @ i) [ (i = 1) -> q, (i=0) -> <j> 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 = <i> \ (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) -> <i>p@i x
       G (p:T1) : T0 = <i>\ (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) -> <i> \ (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) (<i>idPi A B f g@-i) rem1

propSet (A : U) (h : isProp A) : isSet A =
 \(a b : A) (p q : Path A a b) ->
   <j i> 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 (<i> 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) -> <i> \(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-><i>false;true-><i>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 =
  <i> 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) (<j> \ (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))