{- | The construction of the image of a map from the paper
 -   Egbert Rijke, The join construction, https://arxiv.org/pdf/1701.07538.pdf
 -}

\import Data.SeqColimit
\import Equiv
\import Equiv.Univalence
\import Function
\import Logic.Unique
\import Homotopy.Fibration
\import Homotopy.Pushout
\import Logic
\import Paths
\import Paths.Meta

\func MJoin {A B : \Type} (R : A -> B -> \Type) => PushoutData {\Sigma (x : A) (y : B) (R x y)} __. __.
  \where
    \class MData.{u} \noclassifying {A : \Type u} {B : \Type (\suc u)} (f : A -> B) (R : B -> B -> \Type u) (ret : \Pi (b b' : B) -> R b b' -> b = b') {
      \func MImageAppr (n : Nat) : \Sigma (X : \Type u) (X -> B) \elim n
        |  => (A,f)
        | suc n =>
          \let (X,g) => MImageAppr n
          \in (MJoin (\lam a x => R (f a) (g x)), PushoutData.rec f g (\lam q => ret (f q.) (g q.) q.))

      \func MImage => SeqColimit seq

      \func seq : Seq \cowith
        | A n => (MImageAppr n).
        | f x => pinr x

      \func dom-map (a : A) : MImage => inSC {seq} {} a

      \lemma dom-map-surj (refl : \Pi {b : B} -> R b b) : IsSurj dom-map
        => seqColimit-surj seq \lam n => \case \elim __ \with {
          | pinl a => inP \case \elim n \with {
            |  => (a, inv (path (pglue ((a,a,refl) : \Sigma (a : A) (a' : A) (R (f a) (f a'))))))
            | suc n => (pinl a, inv (path (pglue ((a, pinl a, refl) : \Sigma (a : A) (x : (MImageAppr (suc n)).) (R (f a) ((MImageAppr (suc n)). x))))))
          }
          | pinr x => inP (x,idp)
        }

      \func cod-map (x : MImage) : B \elim x
        | inSC {n} x => (MImageAppr n). x
        | quotSC {n} x => idp

      \lemma cod-map-emb (refl : \Pi {b : B} -> R b b) (refl-idp : \Pi {b : B} -> ret b b refl = idp) : Embedding cod-map =>
        Embedding.fibers cod-map (\lam b => isContr'=>isProp (\lam (r : Fib cod-map b) => \case dom-map-surj refl r. \with {
          | inP r' => rewriteI (pmap cod-map r'. *> r.) (fibers-contr refl refl-idp r'.)
        }))
        \where
          \lemma fibers-contr (refl : \Pi {b : B} -> R b b) (refl-idp : \Pi {b : B} -> ret b b refl = idp) (a : A) : Contr (Fib cod-map (f a)) =>
            \let | P x => cod-map x = f a
                 | sec {b b' : B} (q : b = b') => transport (R b) q refl
                 | sec-ret {b b' : B} (q : b = b') => Jl (\lam b'' q' => ret b b'' (sec q') = q') refl-idp q
            \in rewriteI (SeqColimit.flattening P)
                         (constantMaps SeqColimit.flattening.total.seq (\lam n => ((pinl a, idp), \lam p =>
                             inv (ext (path (pglue ((a, p., sec (inv p.)) : \Sigma (a : A) (x : (MImageAppr n).) (R (f a) ((MImageAppr n). x)))),
                                       transport_path-left (ret (f a) ((MImageAppr n). p.) (sec (inv p.))) idp *> pmap inv (sec-ret (inv p.)) *> inv_inv p.)))))
    }

\func YImage.{u} {A B : \Type u} (S : A -> B -> \Type u) => data.MImage
  \where {
    \open MJoin

    \instance data : MData S \cowith
      | R F G => \Pi (b : B) -> Equiv (F b) (G b)
      | ret F G r => path (\lam i b => Equiv_= (r b) i)

    \func dom-map (a : A) : YImage S
      => MData.dom-map a

    \lemma dom-map-surj : IsSurj dom-map
      => MData.dom-map-surj \lam {F} b => mkEquiv (inP idEquiv)

    \func cod-map (y : YImage S) (b : B)
      => MData.cod-map y b

    \lemma cod-map-emb : Embedding cod-map
      => MData.cod-map-emb (\lam {F} b => mkEquiv (inP idEquiv)) \lam {F} =>
          \have p b : Equiv_= (mkEquiv (inP (idEquiv {F b}))) = idp => typeUnivalence.ret_f idp
          \in path \lam i => path \lam j b => p b i j
  }