{-# OPTIONS --without-K --rewriting #-}

open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.connected-maps
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equivalences
open import foundation.fibers-of-maps
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.functoriality-truncation
open import foundation.homotopies
open import foundation.identity-types
open import foundation.images
open import foundation.locally-small-types
open import foundation.propositional-truncations
open import foundation.slice
open import foundation.small-types
open import foundation.surjective-maps
open import foundation.transport-along-identifications
open import foundation.truncated-types
open import foundation.truncation-levels
  renaming (truncation-level-minus-two-ℕ to minus-two;
    truncation-level-minus-one-ℕ to minus-one)
open import foundation.truncated-maps
open import foundation.truncations
open import foundation.truncation-images-of-maps
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.uniqueness-image
open import foundation.universal-property-image
open import foundation.universe-levels

open import rewriting
open import notation

module image-factorisation where

  module _ {i j}
           {Domain : UU i} {Codomain : UU j}
           (_ : is-locally-small i Codomain)
           (f : Domain → Codomain) where

    postulate Image : UU i

    postulate image-inclusion : Image ↪ Codomain

    postulate image-quotient : Domain ↠ Image

    postulate image-β : ∀ x → (pr1 image-inclusion (image-quotient 〈 x 〉)) ↦ f x

    {-# REWRITE image-β #-}

    -- The small image postulated here is equivalent to the HoTT-book image
    is-image-image-inclusion : is-image f image-inclusion (pr1 image-quotient , (λ x → refl))
    is-image-image-inclusion =
      is-image-is-surjective
          (f)
          (image-inclusion)
          (pr1 image-quotient , λ x → refl)
          (pr2 image-quotient)

    equiv-im-Image : im f ≃ Image
    equiv-im-Image =
      equiv-equiv-slice-uniqueness-im
        (f)
        (image-inclusion)
        (pr1 image-quotient , λ x → refl)
        (is-image-image-inclusion)

    equiv-Image-im : Image ≃ im f
    equiv-Image-im = inv-equiv equiv-im-Image

    -- Characterisation of the fibers of image-inclusion
    equiv-fiber-Image-im : (y : Codomain)
                       → fiber (map-emb image-inclusion) y
                       ≃ type-trunc-Prop (fiber f y)
    equiv-fiber-Image-im y =
      equivalence-reasoning
        fiber (map-emb image-inclusion) y
      ≃ fiber (inclusion-im f) y           by (inv-equiv (map-equiv (equiv-fam-equiv-equiv-slice
                                                       (inclusion-im f)
                                                       (map-emb image-inclusion))
                                                       (equiv-slice-uniqueness-im
                                                         (f)
                                                         (image-inclusion)
                                                         (pr1 image-quotient , λ x → refl)
                                                         (is-image-image-inclusion))
                                                       (y)))
      ≃ type-trunc-Prop (fiber f y)        by (equiv-fiber-pr1 (type-trunc-Prop ∘ fiber f) y)


  -- Using the assumptions above we can construct a small (n-2)-image
  -- given that the domain is small and the codomain is n-small

  is-[_]-small : ℕ → (i : Level)
               → {j : Level} (A : UU j)
               → UU (lsuc i ⊔ j)
  is-[ zero-ℕ ]-small i A = is-small i A
  is-[ succ-ℕ n ]-small i A = (x y : A) → is-[ n ]-small i (x == y)

  -- A type that is n-small is also (n+1)-small
  is-succ-ℕ-n-small-is-n-small : {i j : Level}
                           → {A : UU j} {n : ℕ}
                           → is-[ n ]-small i A
                           → is-[ succ-ℕ n ]-small i A
  is-succ-ℕ-n-small-is-n-small {n = zero-ℕ} p = is-locally-small-is-small p
  is-succ-ℕ-n-small-is-n-small {n = succ-ℕ n} p x y =
    is-succ-ℕ-n-small-is-n-small {n = n} (p x y)

  -- A type that is locally small is (n+1)-small for any n
  is-[succ-ℕ_]-small-is-locally-small : {i j : Level}
                                      → {A : UU j} (n : ℕ)
                                      → is-locally-small i A
                                      → is-[ succ-ℕ n ]-small i A
  is-[succ-ℕ zero-ℕ ]-small-is-locally-small p = p
  is-[succ-ℕ succ-ℕ n ]-small-is-locally-small p =
    is-succ-ℕ-n-small-is-n-small (is-[succ-ℕ n ]-small-is-locally-small p)

  is-small-trunc-im : (i : Level) {j : Level} (n : ℕ) {A : UU i} {B : UU j} (f : A → B)
                    → is-[ n ]-small i B
                    → is-small i (trunc-im (minus-two n) f)
  is-small-trunc-im i zero-ℕ f p = is-small-equiv _ (equiv-pr1 (λ _ → is-trunc-type-trunc)) p
  is-small-trunc-im i (succ-ℕ n) {A} f p = (X , e)
    where
      is-surjective-unit-trunc-im : is-surjective (unit-trunc-im (minus-one n) f)
      is-surjective-unit-trunc-im =
        is-surjective-is-connected-map (minus-two n)
          (is-connected-map-unit-trunc-im (minus-one n) f)

      is-locally-small-trunc-im : is-locally-small i (trunc-im (minus-one n) f)
      is-locally-small-trunc-im t t' =
        apply-dependent-universal-property-surj-is-surjective
          (λ ((a , a') : A × A) → (unit-trunc-im (minus-one n) f a , unit-trunc-im (minus-one n) f a'))
          (is-surjective-map-prod is-surjective-unit-trunc-im is-surjective-unit-trunc-im)
          (λ (s , s') → is-small-Prop i (s == s'))
          (λ (a , a') →
            is-small-equiv _
              (extensionality-trunc-im (minus-two n) f a a')
              (is-small-trunc-im i n (ap f {a} {a'}) (p (f a) (f a'))))
          (t , t')

      X : UU i
      X = Image is-locally-small-trunc-im (unit-trunc-im (minus-one n) f)

      e : trunc-im (minus-one n) f ≃ X
      e =
        equiv-im-Image is-locally-small-trunc-im (unit-trunc-im (minus-one n) f) ∘e
        inv-equiv
          (equiv-equiv-slice-uniqueness-im
            (unit-trunc-im (minus-one n) f)
            (emb-equiv id-equiv)
            (unit-trunc-im (minus-one n) f , refl-htpy)
            (is-image-is-surjective _
              (emb-equiv id-equiv)
              (unit-trunc-im (minus-one n) f , refl-htpy)
              is-surjective-unit-trunc-im))

  module _ {i j}
           {Domain : UU i} {Codomain : UU j}
           {n : ℕ}
           (p : is-[ n ]-small i Codomain)
           (f : Domain → Codomain) where

    abstract
      trunc-Image : UU i
      trunc-Image = pr1 (is-small-trunc-im i n f p)

      equiv-trunc-im-trunc-Image : trunc-im (minus-two n) f ≃ trunc-Image
      equiv-trunc-im-trunc-Image = pr2 (is-small-trunc-im i n f p)

      trunc-image-inclusion : trunc-map (minus-two n) trunc-Image Codomain
      pr1 trunc-image-inclusion =
        projection-trunc-im (minus-two n) f ∘
        map-inv-equiv equiv-trunc-im-trunc-Image
      pr2 trunc-image-inclusion =
        is-trunc-map-comp (minus-two n)
          (projection-trunc-im (minus-two n) f)
          (map-inv-equiv equiv-trunc-im-trunc-Image)
          (is-trunc-map-projection-trunc-im (minus-two n) f)
          (is-trunc-map-is-equiv (minus-two n) (is-equiv-map-inv-equiv equiv-trunc-im-trunc-Image))

      trunc-image-quotient : connected-map (minus-two n) Domain trunc-Image
      pr1 trunc-image-quotient =
        map-equiv equiv-trunc-im-trunc-Image ∘
        unit-trunc-im (minus-two n) f
      pr2 trunc-image-quotient =
        is-connected-map-comp (minus-two n)
          (is-connected-map-is-equiv (is-equiv-map-equiv equiv-trunc-im-trunc-Image))
          (is-connected-map-unit-trunc-im (minus-two n) f)

      trunc-image-β : ∀ x → (trunc-image-inclusion 〈 trunc-image-quotient 〈 x 〉 〉) == f x
      trunc-image-β x =
        ap (projection-trunc-im (minus-two n) f)
           (is-retraction-map-inv-equiv equiv-trunc-im-trunc-Image (unit-trunc-im (minus-two n) f x))

      equiv-fiber-trunc-Image-im : (y : Codomain)
                               → fiber (map-trunc-map trunc-image-inclusion) y
                               ≃ type-trunc (minus-two n) (fiber f y)
      equiv-fiber-trunc-Image-im y =
        equivalence-reasoning
          fiber (map-trunc-map trunc-image-inclusion) y

            ≃ Σ (fiber (map-trunc-map trunc-image-inclusion) y)
                (λ t → type-trunc (minus-two n)
                  (fiber (map-connected-map trunc-image-quotient) (pr1 t)))        by inv-equiv (equiv-pr1 λ t → pr2 trunc-image-quotient (pr1 t))

            ≃ type-trunc (minus-two n)
                (Σ (fiber (map-trunc-map trunc-image-inclusion) y)
                   (λ t → type-trunc (minus-two n)
                     (fiber (map-connected-map trunc-image-quotient) (pr1 t))))    by equiv-unit-trunc
                                                                                      (_ , is-trunc-Σ
                                                                                        (pr2 trunc-image-inclusion y)
                                                                                        (λ t → is-trunc-type-trunc))
            ≃ type-trunc (minus-two n)
                (Σ (fiber (map-trunc-map trunc-image-inclusion) y)
                   (λ t → fiber (map-connected-map trunc-image-quotient) (pr1 t))) by inv-equiv-trunc-Σ (minus-two n)

            ≃ type-trunc (minus-two n)
                (fiber (pr1 trunc-image-inclusion ∘ pr1 trunc-image-quotient) y)   by equiv-trunc (minus-two n) (inv-compute-fiber-comp _ _ y)

            ≃ type-trunc (minus-two n) (fiber f y)                                 by equiv-trunc (minus-two n)
                                                                                      (equiv-tot (λ x →
                                                                                        equiv-concat (inv (trunc-image-β x)) y))


  -- The image inclusion is also n+k-truncated
  module _ {i j} {Domain : UU i} {Codomain : UU j} where

    is-trunc-image-inclusion-add-ℕ : {n : ℕ} (k : ℕ)
                                   → (p : is-[ n ]-small i Codomain)
                                   → (f : Domain → Codomain)
                                   → is-trunc-map (minus-two (add-ℕ n k)) (map-trunc-map (trunc-image-inclusion p f))
    is-trunc-image-inclusion-add-ℕ zero-ℕ p f = is-trunc-map-map-trunc-map (trunc-image-inclusion p f)
    is-trunc-image-inclusion-add-ℕ (succ-ℕ k) p f =
      is-trunc-map-succ-is-trunc-map _ (is-trunc-image-inclusion-add-ℕ k p f)

    module _ {n : ℕ}(k : ℕ)
      (p : is-[ n ]-small i Codomain)
      (f : Domain → Codomain) where

      trunc-image-inclusion-add-ℕ : trunc-map (minus-two (add-ℕ n k)) (trunc-Image p f) Codomain
      pr1 trunc-image-inclusion-add-ℕ = map-trunc-map (trunc-image-inclusion p f)
      pr2 trunc-image-inclusion-add-ℕ = is-trunc-image-inclusion-add-ℕ k p f

      trunc-image-inclusion-add-ℕ' : trunc-map (minus-two (add-ℕ' n k)) (trunc-Image p f) Codomain
      pr1 trunc-image-inclusion-add-ℕ' = map-trunc-map (trunc-image-inclusion p f)
      pr2 trunc-image-inclusion-add-ℕ' =
        tr (λ l → is-trunc-map (minus-two l) (map-trunc-map (trunc-image-inclusion p f)))
           (commutative-add-ℕ n k)
           (is-trunc-image-inclusion-add-ℕ k p f)

    trunc-image-inclusion-eq-add-ℕ : {n : ℕ}(k m : ℕ)
                                   → (m == add-ℕ n k)
                                   → (p : is-[ n ]-small i Codomain)
                                   → (f : Domain → Codomain)
                                   → trunc-map (minus-two m) (trunc-Image p f) Codomain
    pr1 (trunc-image-inclusion-eq-add-ℕ {n} k m α p f) = map-trunc-map (trunc-image-inclusion p f)
    pr2 (trunc-image-inclusion-eq-add-ℕ {n} k .(add-ℕ n k) refl p f) =
      is-trunc-image-inclusion-add-ℕ k p f

    trunc-image-inclusion-eq-add-ℕ' : {n : ℕ}(k m : ℕ)
                                   → (m == add-ℕ' n k)
                                   → (p : is-[ n ]-small i Codomain)
                                   → (f : Domain → Codomain)
                                   → trunc-map (minus-two m) (trunc-Image p f) Codomain
    pr1 (trunc-image-inclusion-eq-add-ℕ' {n} k m α p f) = map-trunc-map (trunc-image-inclusion p f)
    pr2 (trunc-image-inclusion-eq-add-ℕ' {n} k .(add-ℕ' n k) refl p f) =
      is-trunc-map-map-trunc-map (trunc-image-inclusion-add-ℕ' k p f)