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

\func famUniverse.{u} {fam : Family.{u}} : ReflUniverse \cowith
  | Universe => universe
  | localization A => \new Localization {
    | S' {
      | S => LData {famHat} A
      | local j => inP \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 IsEquiv (inv (path (\lam i g d => rec.map g id id (\lam x => idpe (F j x)) d @ i)))
                               (IsEquiv.trans (Embedding.diag-equiv (Embedding.fromIsEquiv (Z.local j))) (pushout_pullback-equiv (F j)))
        }}
  }
  \where {
    \open PushoutData

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

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

    \data LData.{u} {fam : Family.{u}} (A : \Type u)
      | 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.{u} {fam : Family.{u}} {A : \Type u} {Z : Local.{u}} (h : A -> Z) (d : LData A) : Z \elim d
      | alpha a => h a
      | ext {j} f y => IsEquiv.ret (Z.local j) (\lam x => dataExt h (f x)) y
      | isExt {j} f x i => (IsEquiv.f_ret (Z.local j) {\lam x => dataExt h (f x)} i) x

    \func dataExt-unique.{u} {fam : Family.{u}} {A : \Type u} {Z : Local.{u}} (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 => IsEquiv.ret (pmapIsEquiv (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 => pmapIsEquiv (Z.local j) {H1 `o` ext f} {H2 `o` ext f}
             | q => path (\lam i => IsEquiv.ret e (path (\lam i' x => p x i')) i (F j x))
             | s : q = p x => path (\lam k => path (\lam i => IsEquiv.f_ret e k i x))
        \in Cube2.map _ _ _ _ s i

    \lemma alpha-equiv.{u} {fam : Family.{u}} {A : \Type u} {Z : Local.{u}} : IsEquiv {LData A -> Z} {A -> Z} (-o alpha)
      => inP \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.{u} {fam : Family.{u}} (k : J `Or` J) : \Type u \elim k
      | inl j => X j
      | inr j => PushoutData (F j) (F j)

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

    \func FHat.{u} {fam : Family.{u}} (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.{u} {fam : Family.{u}}
      => \new Family (J `Or` J) DHat CHat FHat

    \lemma pushout_pullback-equiv {X Y Z : \Type} (f : X -> Y)
      : IsEquiv {\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)))
      => inP \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.{u} {J : \Type u} (X : J -> \Type u) : Modality \cowith
  | ReflUniverse => famUniverse {\new famUniverse.Family J X (\lam _ => \Sigma) (\lam _ _ => ())}
  | isModality A B => \new Local {
    | local j => inP $ 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 => IsEquiv.toQEquiv $ (B (f ())).local j}
        (\Sigma (f : \Sigma -> A) (X j -> B (f ())))       {sigma-left $ IsEquiv.toQEquiv (A.local 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.{u} {J : \Type u} {X : J -> \Type u} (Z : \Type u) : (nullFamUniverse X).isLocal Z = (\Pi (j : J) -> IsEquiv {Z} {X j -> Z} (\lam z _ => z))
      => path \lam i => \Pi (j : J) -> IsEquiv {QEquiv_= (unit-func Z) i} {X j -> Z} (\lam t _ => coe2 (QEquiv_= (unit-func Z)) i t right)
  }

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