{-# OPTIONS --without-K #-}
module hott.truncation.core where

open import sum
open import equality
open import function.core
open import function.fibration
open import function.extensionality
open import function.isomorphism
open import sets.nat.core
open import hott.equivalence
open import hott.level.core
open import hott.level.closure

module _ {i j i' j'}{A : Set i}{A' : Set i'}
         {B : A → Set j}{B' : A' → Set j'}
         (f : A → A')
         (g : (a : A) → B a → B' (f a)) where
  private
    E E' : Set _
    E = Σ A B
    E' = Σ A' B'

    p : E → A
    p = proj₁

    p' : E' → A'
    p' = proj₁

    t : E → E'
    t (a , b) = (f a , g a b)

  module _ (f-equiv : weak-equiv f)
           (t-equiv : weak-equiv t) where

    private
      φ : A ≅ A'
      φ = ≈⇒≅ (f , f-equiv)

      τ : E ≅ E'
      τ = ≈⇒≅ (t , t-equiv)

      lem : (a : A)(e : E) → (p e ≡ a) ≅ (p' (t e) ≡ f a)
      lem a e = iso≡ φ

    fib-equiv : (a : A) → B a ≅ B' (f a)
    fib-equiv a = sym≅ (fib-iso a) ·≅ Σ-ap-iso τ (lem a) ·≅ fib-iso (f a)

postulate
  Trunc : ∀ {i} → ℕ → Set i → Set i
  Trunc-level : ∀ {i} n {X : Set i} → h n (Trunc n X)
  [_] : ∀ {i n} {X : Set i} → X → Trunc n X

Trunc-ext : ∀ {i j} n (X : Set i)(Y : Set j)
          → (Trunc n X → Y) → X → Y
Trunc-ext n X Y f x = f [ x ]

postulate
  Trunc-univ : ∀ {i j} n (X : Set i)(Y : Set j) → h n Y
             → weak-equiv (Trunc-ext n X Y)

Trunc-elim-iso : ∀ {i j} n (X : Set i)(Y : Set j) → h n Y
               → (Trunc n X → Y) ≅ (X → Y)
Trunc-elim-iso n X Y hY = ≈⇒≅ (Trunc-ext n X Y , Trunc-univ n X Y hY)

Trunc-elim : ∀ {i j} n (X : Set i)(Y : Set j) → h n Y
           → (X → Y) → (Trunc n X → Y)
Trunc-elim n X Y hY = invert (Trunc-elim-iso n X Y hY)

Trunc-elim-β : ∀ {i j} n (X : Set i)(Y : Set j)(hY : h n Y)
             → (f : X → Y)(x : X)
             → Trunc-elim n X Y hY f [ x ] ≡ f x
Trunc-elim-β n X Y hY f x = funext-inv (_≅_.iso₂ (Trunc-elim-iso n X Y hY) f) x

module _ {i j} n {X : Set i} (Y : Trunc n X → Set j)
         (hY : (x : Trunc n X) → h n (Y x)) where

  private
    Z : Set _
    Z = Σ (Trunc n X) Y

    hZ : h n Z
    hZ = Σ-level (Trunc-level n) hY

    Sec₂ : ∀ {k}{A : Set k} → (A → Trunc n X) → Set _
    Sec₂ {A = A} r = (x : A) → Y (r x)

    Sec : ∀ {k} → Set k → Set _
    Sec A = Σ (A → Trunc n X) Sec₂

    τ : Sec (Trunc n X) ≅ Sec X
    τ = sym≅ ΠΣ-swap-iso ·≅ Trunc-elim-iso n X Z hZ ·≅ ΠΣ-swap-iso

    ψ : (r : Trunc n X → Trunc n X)
      → (Sec₂ r) ≅ Sec₂ (r ∘ [_])
    ψ = fib-equiv {A = Trunc n X → Trunc n X}{A' = X → Trunc n X}{B = Sec₂} {B' = Sec₂}
        (Trunc-ext n X (Trunc n X)) (λ r g x → g [ x ])
        (Trunc-univ n X (Trunc n X) (Trunc-level n))
        (proj₂ (≅⇒≈ τ))

  Trunc-dep-iso : Sec₂ (λ x → x) ≅ Sec₂ [_]
  Trunc-dep-iso = ψ (λ x → x)

  Trunc-dep-elim : ((x : X) → Y [ x ]) → (x : Trunc n X) → Y x
  Trunc-dep-elim = invert Trunc-dep-iso

  Trunc-dep-elim-β : (d : ((x : X) → Y [ x ]))
                   → (x : X) → Trunc-dep-elim d [ x ] ≡ d x
  Trunc-dep-elim-β d = funext-inv (_≅_.iso₂ Trunc-dep-iso d)