\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.1 t.2 (\lam x => path ((t.3 @ __) 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 ()).1, \lam _ => (g ()).2) | ret p _ => (p.1 (), p.2 ()) | 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.1 x, p.2 x) | ret g => ((g __).1, (g __).2) | 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)))
}
`