\import Algebra.Meta
\import Data.Or
\import Equiv
\import Equiv.Path
\import Equiv.Sigma
\import Function
\import Homotopy.Cube
\import Homotopy.Localization.Modality
\import Homotopy.Localization.Universe
\import Homotopy.Pushout
\import Paths

\func famUniverse {fam : Family} : ReflUniverse \cowith
  | Universe => universe
  | localization A => \new Localization {
    | S' {
      | S => LData {famHat} A
      | local j =>
          \new QEquiv {
            | ret => ext {famHat} {A} {inl j}
            | ret_f g =>
              \have p s => path (isExt {famHat} {A} {inr j} (rec (ext {famHat} {A} {inl j} (g `o` F j)) g (\lam x => path (isExt {famHat} {A} {inl j} (g `o` F j) x))) s)
              \in path (\lam i y => (inv (p (pinl y)) *> p (pinr y)) @ i)
            | f_sec f => path (\lam i x => isExt {famHat} {A} {inl j} f x i)
          }
    }
    | inL => alpha {famHat}
    | local-univ Z => alpha-equiv {famHat} {A} {\new Local {universe {famHat}} Z
        \case \elim __ \with {
          | inl j => local {Z} j
          | inr j => transport (Equiv __) (inv (path (\lam i g d => rec.map g id id (\lam x => idpe (F j x)) d @ i)))
                               (transEquiv (Embedding.diag-equiv (ESEquiv.fromEquiv (local {Z} j))) (pushout_pullback-equiv (F j)))
        }}
  }
  \where {
    \open PushoutData

    \class Family
      | J : \Type
      | X : J -> \Type
      | Y : J -> \Type
      | F : \Pi (j : J) -> X j -> Y j

    \instance universe {fam : Family} : Universe \cowith
      | isLocal Z => \Pi (j : J) -> Equiv {Y j -> Z} {X j -> Z} (`o F j)

    \data LData {fam : Family} (A : \Type)
      | alpha A
      | ext {j : J} (X j -> LData A) (Y j)
      | isExt {j : J} (f : X j -> LData A) (x : X j) : ext f (F j x) = f x

    \func dataExt {fam : Family} {A : \Type} {Z : Local} (h : A -> Z) (d : LData A) : Z \elim d
      | alpha a => h a
      | ext {j} f y => sec {Z.local j} (\lam x => dataExt h (f x)) y
      | isExt {j} f x i => (f_sec {Z.local j} (\lam x => dataExt h (f x)) @ i) x

    \func dataExt-unique {fam : Family} {A : \Type} {Z : Local} (H1 H2 : LData A -> Z) (K : \Pi (a : A) -> H1 (alpha a) = H2 (alpha a)) (d : LData A) : H1 d = H2 d \elim d
      | alpha a => K a
      | ext {j} f y =>
        \have p x => path (\lam i => H1 (isExt f x i)) <* dataExt-unique H1 H2 K (f x) *> inv (path (\lam i => H2 (isExt f x i)))
        \in path (\lam i => (sec {pmapEquiv (Z.local j) {H1 `o` ext f} {H2 `o` ext f}} (path (\lam i' x => p x @ i')) @ i) y)
      | isExt {j} f x i =>
        \let | p x => path (\lam i => H1 (isExt f x i)) <* dataExt-unique H1 H2 K (f x) *> inv (path (\lam i => H2 (isExt f x i)))
             | e : Equiv {H1 `o` ext f = H2 `o` ext f} => pmapEquiv (Z.local j)
             | q => path (\lam i => (e.sec (path (\lam i' x => p x @ i')) @ i) (F j x))
             | s : q = p x => path (\lam k => path (\lam i => (e.f_sec (path (\lam i' x => p x @ i')) @ k @ i) x))
        \in Cube2.map _ _ _ _ s i

    \lemma alpha-equiv {fam : Family} {A : \Type} {Z : Local} : Equiv {LData A -> Z} {A -> Z} (-o alpha) =>
      \new QEquiv {
        | ret => dataExt
        | ret_f h => path (\lam i d => dataExt-unique (dataExt (h `o` alpha)) h (\lam _ => idp) d @ i)
        | f_sec _ => idp
      }

    \func DHat {fam : Family} (k : J `Or` J) : \hType \elim k
      | inl j => X j
      | inr j => PushoutData (F j) (F j)

    \func CHat {fam : Family} (k : J `Or` J) : \Type \elim k
      | inl j => Y j
      | inr j => Y j

    \func FHat {fam : Family} (k : J `Or` J) (d : DHat k) : CHat k \elim k
      | inl j => F j d
      | inr j => rec id id (\lam _ => idp) d

    \func famHat {fam : Family} => \new Family (J `Or` J) DHat CHat FHat

    \lemma pushout_pullback-equiv {X Y Z : \Type} (f : X -> Y)
      : Equiv {\Sigma (g1 g2 : Y -> Z) (g1 `o` f = g2 `o` f)}
              {PushoutData f f -> Z}
              (\lam t => rec t. t. (\lam x => path ((t. @ __) x)))
      => \new QEquiv {
        | ret m => (m `o` pinl, m `o` pinr, path (\lam i x => m (pglue x i)))
        | ret_f t => idp
        | f_sec m => path (\lam i d => (\case \elim d \return rec (m `o` pinl) (m `o` pinr) (\lam x => path (\lam i => m (pglue x i))) d = m d \with {
          | pinl y => idp
          | pinr y => idp
          | pglue x i => idp
        }) @ i)
      }
  }

\func nullFamUniverse {J : \Type} (X : J -> \Type) : Modality \cowith
  | ReflUniverse => famUniverse {\new famUniverse.Family J X (\lam _ => \Sigma) (\lam _ _ => ())}
  | isModality A B => \new Local {
    | local j => equation
        (\Sigma -> \Sigma (a : A) (B a))                   {\new QEquiv { | B => \Sigma (f : \Sigma -> A) (\Sigma -> B (f ())) | f g => (\lam _ => (g ())., \lam _ => (g ()).) | ret p _ => (p. (), p. ()) | ret_f g => idp | f_sec p => idp }}
        (\Sigma (f : \Sigma -> A) (\Sigma -> B (f ())))    {sigma-right {\Sigma -> A} (\lam f => local {B (f ())} j)}
        (\Sigma (f : \Sigma -> A) (X j -> B (f ())))       {sigma-left (local {A} j)}
        (\Sigma (f : X j -> A) (\Pi (x : X j) -> B (f x))) {\new QEquiv { | B => X j -> \Sigma (a : A) (B a) | f p x => (p. x, p. x) | ret g => ((g __)., (g __).) | ret_f p => idp | f_sec g => idp }}
        (X j -> \Sigma (a : A) (B a))
  }
  \where {
    \lemma localDesc (Z : \Type) : isLocal {nullFamUniverse X} Z = (\Pi (j : J) -> Equiv {Z} {X j -> Z} (\lam z _ => z))
      => path (\lam i => \Pi (j : J) -> Equiv {equiv= (unit-func Z) @ i} {X j -> Z} (\lam t _ => coe2 (equiv= (unit-func Z) @) i t right))
  }

\func nullTypeUniverse (M : \Type) : Modality => nullFamUniverse {\Sigma} (\lam _ => M)
  \where {
    \lemma localDesc (M Z : \Type) : isLocal {nullTypeUniverse M} Z = Equiv {Z} {M -> Z} (\lam z _ => z)
      => nullFamUniverse.localDesc Z *> equiv= (unit-func (Equiv {Z} {M -> Z} (\lam z _ => z)))
  }