\import Equiv
\import Equiv.Sigma
\import Equiv.Univalence
\import HLevel
\import Homotopy.Fibration
\import Homotopy.Join
\import Homotopy.Localization.Accessible
\import Homotopy.Localization.Universe
\import Homotopy.Pushout
\import Logic
\import Paths
\import Paths.Meta

\open Localization

-- | A type {X} is connected if, for every local type Z, the constant map (\Sigma -> Z) -> (X -> Z) is an equivalence
\func isConnectedType {U : Universe} (X : \hType) => \Pi (Z : Local) -> isLocal {nullTypeUniverse X} Z

-- | If a type {X} is connected, then its localization is contractible
\lemma isConnected=>contr {U : ReflUniverse} (X : \hType) (c : isConnectedType X) : Contr (LType X) =>
  \have c' : Equiv (\lam z _ => z) => propExt.dir (nullTypeUniverse.localDesc X (LType X)) (c (LType X))
  \in \new Contr {
    | center => c'.sec lEta
    | contraction => remove_inL (\lam _ => c'.sec lEta) (\lam x => x) (\lam a => path (\lam i => (c'.f_sec lEta @ i) a))
  }

-- | If the localization of a type {X} is contractible, then {X} is connected
\lemma contr=>isConnected {U : ReflUniverse} (X : \hType) (c : Contr (LType X)) : isConnectedType X
  => \lam Z => propExt.conv (nullTypeUniverse.localDesc X Z) (\new QEquiv {
    | ret g => lift g c.center
    | ret_f z => lift.const z c.center
    | f_sec g => path (\lam i x => (pmap (lift g) (c.contraction (inL x)) *> lift-prop g x) @ i)
  })

\class Connected {U : Universe} (X : \hType) {
  | connected : isConnectedType X

  \lemma equiv (Z : Local {U}) : Equiv {Z} {X -> Z} (\lam z _ => z) => propExt.dir (nullTypeUniverse.localDesc X Z) (connected Z)
}

-- | Theorem 6.8, Egbert Rijke, The join construction, https://arxiv.org/pdf/1701.07538.pdf
\lemma connected_join (X Y M N : \hType)
                      (X-conn : isConnectedType {nullTypeUniverse M} X)
                      (Y-conn : isConnectedType {nullTypeUniverse N} Y)
  : isConnectedType {nullTypeUniverse (Join M N)} (Join X Y)
  => \lam Z => connected_local_join-right Z Y X N Y-conn (connected_local_join-left X Z M N X-conn (local {Z}))
  \where {
    -- | Lemma 6.4
    \lemma local_join (A A' B : \hType) : (\Pi (f : A' -> B) -> isLocal {nullTypeUniverse A} (\Sigma (b : B) (\Pi (a : A') -> f a = b)))
                                       = isLocal {nullTypeUniverse (Join A A')} B
      => \let | C (f : A' -> B) => \Sigma (b : B) (\Pi (a : A') -> b = f a)
              | F (p : \Sigma (f : A' -> B) (C f)) : \Sigma (f : A' -> B) (A -> C f) => (p.1, \lam _ => p.2)
              | eq1 => transEquiv (symQEquiv (contr-right (\lam b => lsigma (\lam _ => b))))
                                  (\new QEquiv {\Sigma (b : B) (\Sigma (f : A' -> B) ((\lam _ => b) = f))} {\Sigma (f : A' -> B) (C f)} {
                                    | f p => (p.2.1, (p.1, \lam a => path ((p.2.2 @ __) a)))
                                    | ret p => (p.2.1, (p.1, path (\lam i a => p.2.2 a @ i)))
                                    | ret_f => idpe
                                    | f_sec => idpe
                                  })
              | eq2 => transEquiv (PushoutData.rec.equiv B)
                                  (\new QEquiv {\Sigma (f : A -> B) (g : A' -> B) (\Pi (q : \Sigma A A') -> f q.1 = g q.2)} {\Sigma (f : A' -> B) (A -> C f)} {
                                    | f p => (p.2, \lam a => (p.1 a, \lam a' => p.3 (a,a')))
                                    | ret p => ((p.2 __).1, p.1, \lam q => (p.2 q.1).2 q.2)
                                    | ret_f => idpe
                                    | f_sec => idpe
                                  })
         \in (\Pi (f : A' -> B) -> isLocal {nullTypeUniverse A} (\Sigma (b : B) (\Pi (a : A') -> f a = b))) ==< path (\lam i => \Pi (f : A' -> B) -> isLocal {nullTypeUniverse A} (\Sigma (b : B) (\Pi (a : A') -> path-sym (f a) b @ i))) >==
             (\Pi (f : A' -> B) -> isLocal {nullTypeUniverse A} (C f))                                      ==< path (\lam i => \Pi (f : A' -> B) -> nullTypeUniverse.localDesc A (C f) @ i) >==
             (\Pi (f : A' -> B) -> Equiv {C f} {A -> C f} (\lam c _ => c))                                  ==< totalEquiv (\lam f c _ => c) >==
             Equiv F                                                                                        ==< inv (TwoOutOfThree.parallelEquiv (\lam b _ => b) F eq1 eq2 (\lam _ => idp)) >==
             {- The left and right maps are equivalences,
                so the top one is an equivalence iff the bottom one is.
                            \lam b _ => b
                     B -----------------------> Join A A' -> B
                     |                               |
                 eq1 |                               | eq2
                     v                               v
                \Sigma (f : A' -> B) (C f) ---> \Sigma (f : A' -> B) (A -> C f)
                                            F   -}
             Equiv {B} {Join A A' -> B} (\lam b _ => b)                                                     ==< inv (nullTypeUniverse.localDesc (Join A A') B) >==
             isLocal {nullTypeUniverse (Join A A')} B                                                       `qed

    -- | Lemma 6.5
    \lemma connected_local_join-left (X Y M N : \hType)
                                     (X-conn : isConnectedType {nullTypeUniverse M} X)
                                     (Y-local : isLocal {nullTypeUniverse (Join M N)} Y)
      : isLocal {nullTypeUniverse (Join X N)} Y
      => propExt.dir (local_join X N Y) (\lam f => X-conn (\new Local { | S => _ | local => propExt.conv (local_join M N Y) Y-local f }))

    \lemma connected_local_join-right (X Y M N : \hType)
                                      (Y-conn : isConnectedType {nullTypeUniverse N} Y)
                                      (X-local : isLocal {nullTypeUniverse (Join M N)} X)
      : isLocal {nullTypeUniverse (Join M Y)} X
      => rewriteI (Equiv-to-= (Join-sym Y M))
                  (connected_local_join-left Y X N M Y-conn (rewriteI (Equiv-to-= (Join-sym M N)) X-local))
  }

\func isConnectedMap {U : Universe} {A B : \hType} (f : A -> B) => \Pi (b : B) -> isConnectedType (Fib f b)