{- Fiber Bundle: https://groupoid.space/mltt/types/bundle/
   - Fiber Bundle;
   - Trivial Fiber Bundle, Trivial = Pi;
   - Local F-Bundle (4 definitions).
   Copyright (c) Groupoid Infinity, 2014-2018. -}

module bundle where
import iso
import infinitesimal
import pullback
import trunc

-- Fiber Bundle

-- A fiber bundle p : E -> B is required to be locally trivial,
-- which might be witnessed by a pullback square like this:

-- V × F ------> E
--     |_|       |
-- v*p |  (pb)   | p
--     |         |
--     v         v
--     V ---v--> B

-- NOTE: there is twisted hidden structure in p
-- U = neighborhood in base B
-- fibers locally behave like a products, but could be twisted

--           h
--           |
-- p-inv (V) -> V * F
--        |   /
--    p --|  /-- pi1
--        v /
--        V
--
-- pr_1 o h = p

-- F_B  -> E -> B -- fiber bundle (F_B,E,p,B),
-- F: B -> U      -- fiber, ex. Vector Space, Section Space, Dependent Product
-- E              -- total topological space
-- B              -- base space
-- h: F -> E      -- homeomorphism
-- p:      E -> B -- surjective projection map
-- p^-1:   B -> E -- section (y: B) = (x: E) * p (x) = y
-- E=(y:B)*p^-1 y -- total space
-- p^-1 = F       -- fiber is iso F_B
-- T. E = B * F_B -- fiber bundle called trivial if total space is a cartesian product

Family (B: U): U = B -> U
Fibration (B: U): U = (X: U) * (X -> B)

-- Trivial Fiber Bundle (F,B*F,pi1,B) equals Dependent Family F:B->U
--
-- Agda Syntax:
-- https://paolocapriotti.com/blog/2013/02/20/families-and-fibrations/
--
--  F y = fiber (total B F) B (trivial B F) y    (A)
--      = (z: E) * Path B z.1 y                     
--      = (z: B) * (k: F z) * Path B z y         (B)
--      = (x y: B) * (_: Path B x y) * (F y)        
--      = (_: isContr B) * (F y)                 (C)
--      = F y                                    (D)

fiber (A B: U) (f: A -> B) (y: B)
  : U
  = (x: A) * Path B (f x) y

encode (B: U) (F: B -> U) (y: B)
  : fiber (Sigma B F) B (pi1 B F) y -> F y
  = \ (x: fiber (Sigma B F) B (pi1 B F) y)
    -> subst B F x.1.1 y x.2 x.1.2

decode (B: U) (F: B -> U) (y: B)
  : F y -> fiber (Sigma B F) B (pi1 B F) y
  = \ (x: F y) -> ((y,x),refl B y)


lem2 (B: U) (F: B -> U) (y: B) (x: F y)
  : Path (F y) (comp (<i>F (refl B y @ i)) x []) x
  = <j> comp (<i>F (refl B y @ j/\i)) x [(j=1) -> <k>x]

lem3 (B: U) (F: B -> U) (y: B) (x: fiber (Sigma B F) B (pi1 B F) y)
  : Path (fiber (Sigma B F) B (pi1 B F) y) ((y,encode B F y x),refl B y) x
  = <i> ((x.2 @ -i,comp (<j> F (x.2 @ -i /\ j))
        x.1.2 [(i=1) -> <_> x.1.2 ]),<j> x.2 @ -i \/ j)

TrivialEqualsPi (B: U) (F: B -> U) (y: B)
  : Path U (fiber (Sigma B F) B (pi1 B F) y) (F y)
  = isoPath T A f g s t where
    T: U = fiber (Sigma B F) B (pi1 B F) y
    A: U = F y
    f: T -> A = encode B F y
    g: A -> T = decode B F y
    s (x: A): Path A (f (g x)) x = lem2 B F y x
    t (x: T): Path T (g (f x)) x = lem3 B F y x

-- Local F-Bundle

-- Definition (1) Dependent
isFBundle1 (B: U) (p: B -> U) (F: U): U
  = (_: (b: B) -> isContr (Path U (p b) F))
  * ((x: Sigma B p) -> B)

-- Definition (2) Dependent
isFBundle2 (B: U) (p: B -> U) (F: U): U
  = (V: U)
  * (v: surjective V B)
  * ((x: V) -> Path U (p (v.1 x)) F)

-- Definition (3) Non-Dependent
im1 (A B: U) (f: A -> B): U = (b: B) * propTrunc ((a:A) * Path B (f a) b)
BAut (F: U): U = im1 unit U (\(x: unit) -> F)
unitIm1 (A B: U) (f: A -> B): im1 A B f -> B = \(x: im1 A B f) -> x.1
unitBAut (F: U): BAut F -> U = unitIm1 unit U (\(x: unit) -> F)
isFBundle3 (E B: U) (p: E -> B) (F: U): U
  = (X: B -> BAut F)
  * (classify B (BAut F) (\(b: B) -> fiber E B p b) (unitBAut F) X) where
  classify (A' A: U) (E': A' -> U) (E: A -> U) (f: A' -> A): U
    = (x: A') -> Path U (E'(x)) (E(f(x)))

-- Definition (4) Non-Dependent
isFBundle4 (E B: U) (p: E -> B) (F: U): U
  = (V: U)
  * (v: surjective V B)
  * (v': prod V F -> E)
  * pullbackSq (prod V F) E V B p v.1 v' (\(x: prod V F) -> x.1)

-- Theorem 4.3.7
unifamOverBAut (F: U): U = (x: BAut F) * U
FBundle (E B: U) (p: E -> B) (F: U) (x: isFBundle3 E B p F) (b: B)
  : pullbackSq E B (unifamOverBAut F) (BAut F)
    x.1 (\(x: unifamOverBAut F) -> x.1)
    p (\(y: E) -> (x.1 (p y),F))
  = undefined