{- | 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 HLevel
\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 \noclassifying {A : \Type} {B : \Type (\suc \lp)} (f : A -> B) (R : B -> B -> \Type) (ret : \Pi (b b' : B) -> R b b' -> b = b') {
      \func MImageAppr (n : Nat) : \Sigma (X : \hType) (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) : Surjection dom-map =>
        seqColimit-surj seq (\lam n => \new Surjection {
          | isSurjMap y => \case \elim y \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 isSurjMap {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 {A B : \Type} (S : A -> B -> \Type) => 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-to-= (r b) @ i)

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

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

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

    \lemma cod-map-emb : Embedding cod-map
      => MData.cod-map-emb (\lam {F} b => idEquiv {F b}) (\lam {F} =>
          \have p b : Equiv-to-= (idEquiv {F b}) = idp => univalence.ret_f idp
          \in path (\lam i => path (\lam j b => p b @ i @ j)))
  }