{-# OPTIONS --without-K #-}
module hott.level.closure.extra where

open import level
open import decidable
open import sum
open import level using (lsuc; ↑; lift)
open import equality.core
open import equality.calculus
open import function.core using (_∘_; const)
open import function.extensionality
open import function.isomorphism.core
open import function.isomorphism.lift
open import function.isomorphism.utils
open import sets.bool
open import sets.unit
open import sets.nat.core
open import sets.nat.ordering.leq.core
open import hott.level.core
open import hott.level.sets
open import hott.level.closure.core
open import hott.equivalence.core
  using (weak-equiv; _≈_)
open import hott.univalence
open import sets.empty
open import sets.unit

abstract
  -- Π preserves h-levels
  Π-level : ∀ {i j n} {X : Set i}{Y : X → Set j}
           → ((x : X) → h n (Y x))
           → h n ((x : X) → Y x)
  Π-level {n = 0} c = Π-contr c
  Π-level {n = suc n} {X = X}{Y} hn = λ f g →
    subst (h n) strong-funext (Π-level (λ x → hn x (f x) (g x)))

  -- Σ preserves h-levels
  Σ-level : ∀ {i j n} {X : Set i}{Y : X → Set j}
           → h n X → ((x : X) → h n (Y x))
           → h n (Σ X Y)
  Σ-level {n = 0}{X = X}{Y} (x₀ , cx) hy =
    (x₀ , proj₁ (hy x₀)) , λ { (x , y) → c x y }
    where
      c : (x : X)(y : Y x) → (x₀ , proj₁ (hy x₀)) ≡ (x , y)
      c x y = ap (λ x → (x , proj₁ (hy x))) (cx x)
            · ap (_,_ x) (proj₂ (hy x) y)
  Σ-level {n = suc n} hx hy = λ a b → iso-level Σ-split-iso
    (Σ-level (hx _ _) (λ p → hy (proj₁ b) _ _))

  -- × preserves h-levels
  ×-level : ∀ {i j n}{X : Set i}{Y : Set j}
           → h n X → h n Y → h n (X × Y)
  ×-level hx hy = Σ-level hx (λ _ → hy)

  -- ⊎ preserves h-levels
  ⊎-level : ∀ {i j n}{X : Set i}{Y : Set j}
           → 2 ≤ n → h n X → h n Y → h n (X ⊎ Y)
  ⊎-level {i}{j}{n} {X}{Y} p hx hy = iso-level lem
    (Σ-level (h! {p = decide p} bool-set) P-level)
    where
      P : Bool → Set (i ⊔ j)
      P true = ↑ j X
      P false = ↑ i Y

      P-level : (b : Bool) → h n (P b)
      P-level true = iso-level (lift-iso j X) hx
      P-level false = iso-level (lift-iso i Y) hy

      lem : Σ Bool P ≅ (X ⊎ Y)
      lem = iso f g H K
        where
          f : (Σ Bool P) → (X ⊎ Y)
          f (true , lift x) = inj₁ x
          f (false , lift y) = inj₂ y

          g : (X ⊎ Y) → (Σ Bool P)
          g (inj₁ x) = (true , lift x)
          g (inj₂ y) = (false , lift y)

          H : (x : Σ Bool P) → g (f x) ≡ x
          H (true , lift x) = refl
          H (false , lift y) = refl

          K : (x : X ⊎ Y) → f (g x) ≡ x
          K (inj₁ x) = refl
          K (inj₂ y) = refl

  Π-level-impl : ∀ {i j n} {X : Set i}{Y : X → Set j}
                → ((x : X) → h n (Y x))
                → h n ({x : X} → Y x)
  Π-level-impl {X = X}{Y} hY = iso-level impl-iso (Π-level hY)

  -- being contractible is a proposition
  contr-h1 : ∀ {i}(X : Set i) → h 1 (contr X)
  contr-h1 X = prop⇒h1 λ { (x₀ , c₀) (x₁ , c₁) →
      unapΣ (c₀ x₁ , contr⇒prop (lem (x₀ , c₀) x₁) _ _) }
    where
      lem : ∀ {i}{A : Set i} → contr A → (x : A) → contr ((x' : A) → x ≡ x')
      lem c x = Π-level (λ x' → h↑ c x x')

  -- being of h-level n is a proposition
  hn-h1 : ∀ {i} n (X : Set i) → h 1 (h n X)
  hn-h1 0 X = contr-h1 X
  hn-h1 (suc n) X = Π-level λ x → Π-level λ y → hn-h1 n (x ≡ y)

  -- being a weak equivalence is a proposition
  weak-equiv-h1 : ∀ {i j}{X : Set i}{Y : Set j}
                → (f : X → Y)
                → h 1 (weak-equiv f)
  weak-equiv-h1 f = Π-level λ y
                  → contr-h1 _

  equiv-level : ∀ {i j n}{X : Set i}{Y : Set j}
              → h n X → h n Y
              → h n (X ≈ Y)
  equiv-level {n = 0} hX hY = Σ-level (Π-level (λ _ → hY)) λ f
    → (λ y → Σ-level hX λ x → h↑ hY _ _)
    , (λ w → h1⇒prop (weak-equiv-h1 f) _ _)
  equiv-level {n = suc n } hX hY
    = Σ-level (Π-level λ _ → hY) λ f
    → h! (weak-equiv-h1 f)

  ⊎-h1 : ∀ {i j}{A : Set i}{B : Set j}
       → h 1 A → h 1 B → ¬ (A × B)
       → h 1 (A ⊎ B)
  ⊎-h1 {A = A}{B = B} hA hB u = prop⇒h1 ⊎-prop
    where
      ⊎-prop : prop (A ⊎ B)
      ⊎-prop (inj₁ a) (inj₁ a') = ap inj₁ (h1⇒prop hA a a')
      ⊎-prop (inj₁ a) (inj₂ b') = ⊥-elim (u (a , b'))
      ⊎-prop (inj₂ b) (inj₁ a') = ⊥-elim (u (a' , b))
      ⊎-prop (inj₂ b) (inj₂ b') = ap inj₂ (h1⇒prop hB b b')

  inj-level : ∀ {i j n}{A : Set i}{B : Set j}
             → (f : A → B)
             → h (suc n) A → h n (injective f)
  inj-level f hA
    = Π-level-impl λ x
    → Π-level-impl λ x'
    → Π-level λ p
    → hA x x'

  ↣-level : ∀ {i j n}{A : Set i}{B : Set j}
           → h (suc n) A → h n B → h n (A ↣ B)
  ↣-level hA hB
    = Σ-level (Π-level λ _ → hB) λ f
    → inj-level f hA

  ¬-h1 : ∀ {i}{X : Set i} → h 1 (¬ X)
  ¬-h1 = Π-level λ _ → ⊥-prop

  type-level : ∀ {i n} → h (suc n) (Type i n)
  type-level {i}{n} (X , hX) (Y , hY) = iso-level uni-iso' (equiv-level hX hY)
    where
      uni-iso' : (X ≈ Y) ≅ ((X , hX) ≡ (Y , hY))
      uni-iso' = begin
          (X ≈ Y)
        ≅⟨ sym≅ uni-iso ⟩
          (X ≡ Y)
        ≅⟨ sym≅ ×-right-unit ⟩
          ((X ≡ Y) × ⊤)
        ≅⟨ ( Σ-ap-iso refl≅ λ q → sym≅ (contr-⊤-iso (hn-h1 n Y _ _)) ) ⟩
          ( Σ (X ≡ Y) λ q → subst (h n) q hX ≡ hY )
        ≅⟨ Σ-split-iso ⟩
          ((X , hX) ≡ (Y , hY))
        ∎
        where open ≅-Reasoning